update SMTChecker tests with Z3 4.11.2 #13740
Conversation
| "1988", "2066", "2833", "3356", | ||
| "3893", "3996", "4010", "4458", "4802", | ||
| "4902", "5272", "5622", "5798", "7128", "7400", | ||
| "4902", "5272", "5622", "5798", "5840", "7128", "7400", |
There was a problem hiding this comment.
These 2 error IDs were SMT errors when the solver couldn't prove something, which surprisingly doesn't happen anymore with the new z3! It's a nice development. We should anyway add some more complex tests that cause that in a future PR.
| m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::All(); | ||
| else if (choice == "none") | ||
| auto const& choice = m_reader.stringSetting("SMTSolvers", "z3"); | ||
| if (choice == "none") |
There was a problem hiding this comment.
This was changed to reflect the new behavior of "z3 is default now".
leonardoalt
force-pushed
the
z3_4_11_2_tests
branch
from
6c058b4 to
c37a62b
Compare
leonardoalt
force-pushed
the
z3_4_11_2_tests
branch
from
8c688da to
d660f0c
Compare
| @@ -5,8 +5,8 @@ Warning: Return value of low-level calls not used. | |||
| | ^^^^^^^^^^^ | |||
|
|
|||
| Info: Contract invariant(s) for model_checker_invariants_all/input.sol:test: | |||
| ((x <= 0) || true) | |||
| (!(x >= 1) || true) | |||
There was a problem hiding this comment.
Just curious, why this change? (x <= 0) and !(x >= 1) are equal, right?
There was a problem hiding this comment.
Yea, invariant and counterexample outputs are very nondeterministic, so the solver will choose an answer at its own discretion. As long as the results are correct you may get anything
| @@ -34,7 +34,7 @@ else | |||
| BUILD_DIR="$1" | |||
| fi | |||
|
|
|||
| # solbuildpackpusher/solidity-buildpack-deps:emscripten-13 | |||
| # solbuildpackpusher/solidity-buildpack-deps:emscripten-14 | |||
There was a problem hiding this comment.
There's a bug here. The hash below has not been updated. Looks like the nightly build in solc-bin has been failing since Friday due to this:
-- Found Z3: /emsdk/upstream/emscripten/cache/sysroot/usr/lib/cmake/z3/Z3Config.cmake (found version "4.11.0.0")
CMake Error at CMakeLists.txt:84 (message):
SMTChecker tests require Z3 4.11.2 for all tests to pass.
Build with -DSTRICT_Z3_VERSION=OFF if you want to use a different version.
You can also use -DUSE_Z3=OFF to build without Z3. In both cases use
--no-smt when running tests.
-- Configuring incomplete, errors occurred!
Pinging @r0qs.
There was a problem hiding this comment.
True! Made a PR #13757
No description provided.