Update smtCheckerTests for z3 4.8.10 #10845
Conversation
leonardoalt
force-pushed
the
smt_z3_4-8-10
branch
from
6058954 to
b023a08
Compare
| wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.9/z3-4.8.9-x64-osx-10.14.6.zip | ||
| unzip z3-4.8.9-x64-osx-10.14.6.zip | ||
| rm -f z3-4.8.9-x64-osx-10.14.6.zip | ||
| cp z3-4.8.9-x64-osx-10.14.6/bin/libz3.a /usr/local/lib | ||
| cp z3-4.8.9-x64-osx-10.14.6/bin/z3 /usr/local/bin | ||
| cp z3-4.8.9-x64-osx-10.14.6/include/* /usr/local/include | ||
| rm -rf z3-4.8.9-x64-osx-10.14.6 | ||
| wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-osx-10.15.7.zip | ||
| unzip z3-4.8.10-x64-osx-10.15.7.zip | ||
| rm -f z3-4.8.10-x64-osx-10.15.7.zip | ||
| cp z3-4.8.10-x64-osx-10.15.7/bin/libz3.a /usr/local/lib | ||
| cp z3-4.8.10-x64-osx-10.15.7/bin/z3 /usr/local/bin | ||
| cp z3-4.8.10-x64-osx-10.15.7/include/* /usr/local/include | ||
| rm -rf z3-4.8.10-x64-osx-10.15.7 |
There was a problem hiding this comment.
This could really use a a variable or two :)
There was a problem hiding this comment.
true, I'll do that when I get the tests to pass
leonardoalt
force-pushed
the
smt_z3_4-8-10
branch
4 times, most recently
from
da08fa4 to
23f4da9
Compare
cameel
left a comment
cameel
left a comment
There was a problem hiding this comment.
They look the same and are assigned to the right images with correct versions.
| // let result := addmod(x, y, z) | ||
| // if 0 { } | ||
| // if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { if 1 { sstore(0, 9) } } | ||
| // if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) |
There was a problem hiding this comment.
This is bad and should not happen :(
There was a problem hiding this comment.
In the encoding, result = wrap(x + y) % z while the condition below is (x + y) % z. With the restrictions in this line, z3 should be able to determine that the condition is 1.
On the other hand, if we switch to an LP solver, it will probably not understand it anyway...
There was a problem hiding this comment.
We should at least add a comment in this test.
leonardoalt
force-pushed
the
smt_z3_4-8-10
branch
from
23f4da9 to
5d51626
Compare
test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addmod.yul
Outdated
Show resolved
Hide resolved
leonardoalt
force-pushed
the
smt_z3_4-8-10
branch
from
5d51626 to
40221a9
Compare
|
|
||
| // addmod is equal to mod of sum for small numbers | ||
| if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { | ||
| // z3 <4.8.10 was able to infer that the |
There was a problem hiding this comment.
Which was the only reason for this test file... ;)
There was a problem hiding this comment.
Yea.. well, we can keep it for reference
Waiting for #10844 to finish in order to update the Ubuntu and emscripten hashes here.
For now only
t_archlinuxandt_osxshould pass.