crucible_llvm_verify using z3 results in "unknown parameter 'global_declarations'"

[dylanmc]

I'm going through the compositional proof of salsa, and ran into this problem:

... good stuff
*** Data.SBV: Unexpected non-success response from Z3:
***
***    Sent      : (set-option :global-declarations true)
***    Expected  : success
***    Received  : (error "line 2 column 33: unknown parameter 'global_declarations'
***                Legal parameters are:
***                  auto_config (bool) (default: true)
... more stuff

Looking in the sawscript, I see it uses z3 instead of abc as in the earlier examples. I then went back to the swap example and got the same error by replacing abc with z3 in the sawscript. Also happens whether I'm using the Linux apt-get version of z3 (4.4.1) or the latest from the Microsoft website (4.8.9).

(This is saw version 0.6 on an Ubuntu 18.04.5 64-bit VM)

[robdockins]

Z3 version 4.4.1 is too old, but 4.8.9 should work. Maybe you need to adjust the path settings to get SAW to pull in the newer Z3?

[dylanmc]

You're right - removing the apt-get version of z3 did the trick. Thanks!