Issue with functional correctness, arrays, and enable_smt_array_memory_model.

[linesthatinterlace]

I recently discovered the enable_smt_array_memory_model routine, and thought it might be useful to help with an issue I was having with a project where symbolic simulation was taking a considerable length of time. It seems to fix the symbolic simulation issue in my larger project, and reaches "Checking proof obligations" However, I am then getting a persistent error with it- I've created a minimum working example which shows the issue. This is the error message (on a smaller, test file).

wrobson@SESHAT:~/pqc-verification/classic-mceliece/verification/test$ ./build.sh 
make: 'test.bc' is up to date.

[20:36:19.524] Loading file "/home/wrobson/pqc-verification/classic-mceliece/verification/test/test.saw"
[20:36:19.568] Verifying test_plus ...
[20:36:19.574] Simulating test_plus ...
[20:36:19.595] Checking proof obligations test_plus ...
[20:36:19.606] Stack trace:
"crucible_llvm_verify" (/home/wrobson/pqc-verification/classic-mceliece/verification/test/test.saw:30:17-30:37):
"z3" (/home/wrobson/pqc-verification/classic-mceliece/verification/test/test.saw:30:85-30:87):
could not create uninterpreted type for Array

I''ve uploaded the test files I'm using. test.zip

I would welcome some advice - is this a genuine bug? Do you have any advice for using enable_smt_array_memory_model? I can't find many examples that use it, and none that use llvm_points_to in the way that I'm using it here, so I wondered if that causes an issue - but if so I would quite like to understand why. Thanks.

[robdockins]

The issue here is that the SBV-based backends (which includes z3) don't have support for the Array type hooked up. We should probably look into doing this, I think SBV can do what we need.

In the meantime, you can complete this proof by using w4_unint_z3 [] or similar instead of z3 for the proof script.