Open
Description
The proof in examples/openssl_aes
appears to have bit-rotted. I tried running it on Ubuntu 22.04 with the latest what4-solvers
solvers, and I used clang-12 to build the bitcode. The proof ran for a few hours before the kernel killed ABC on a machine with 24GB of RAM. SAW-0.9 has the same problem, so this doesn't appear to be a new issue. I'm not sure when the proof broke, or what caused the breakage (off the top of my head, it could be SAW changes, Clang changes, or ABC changes). I also tried changing the proof to use Z3 instead, but it still hung for a few hours before I called it "unlikely to terminate" and killed SAW.
To reproduce the problem, run make
in examples/openssl_aes
. This will build the bitcode and run the SAW proof.