openssl_aes example proof hangs

[bboston7]

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.

[sauclovian-g]

The examples should be getting built in the CI runs...

[RyanGlScott]

There is a test_examples test case that runs some of the examples under the top-level examples directory, but it is set up to only run a subset of the examples. Currrently, this does not include openssl_aes. I agree that it would be nice to test this example in the CI as well (provided that it can be done in a reasonable amount of time).

[mccleeary-galois]

There is a test_examples test case that runs some of the examples under the top-level examples directory, but it is set up to only run a subset of the examples. Currrently, this does not include openssl_aes. I agree that it would be nice to test this example in the CI as well (provided that it can be done in a reasonable amount of time).

If it doesn't run in a reasonable amount of time I still am an advocate of having a longer running CI for testing pre-release branches and the like.

[sauclovian-g]

That and/or we should make sure everything gets run at least once every six months or something.