You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, all CI jobs which use Z3 4.8.11 will fail when running the expr-builder-smtlib2 test suite. Here is an example:
Test suite expr-builder-smtlib2: RUNNING...
SOLVER SELF-REPORTED VERSIONS::
Solver cvc4 -> This is CVC4 version 1.8
Solver yices -> Yices 2.6.4
Solver z3 -> Z3 version 4.8.11 - 64 bit
Tests
<snip>
Z3 string1: OK (unexpected: unicode and string escaping not supported for older Z3 versions; upgrade to at least 4.8.12) (0.02s)
(unexpected success: unicode and string escaping not supported for older Z3 versions; upgrade to at least 4.8.12)
Use -p '/Z3 string1/' to rerun this test only.
Z3 string2: OK (0.04s)
Z3 string3: OK (unexpected: unicode and string escaping not supported for older Z3 versions; upgrade to at least 4.8.12) (0.17s)
(unexpected success: unicode and string escaping not supported for older Z3 versions; upgrade to at least 4.8.12)
Use -p '/Z3 string3/' to rerun this test only.
Z3 string4: OK (unexpected: unicode and string escaping not supported for older Z3 versions; upgrade to at least 4.8.12) (1.19s)
(unexpected success: unicode and string escaping not supported for older Z3 versions; upgrade to at least 4.8.12)
Use -p '/Z3 string4/' to rerun this test only.
Z3 string5: OK (unexpected: unicode and string escaping not supported for older Z3 versions; upgrade to at least 4.8.12) (0.04s)
(unexpected success: unicode and string escaping not supported for older Z3 versions; upgrade to at least 4.8.12)
Use -p '/Z3 string5/' to rerun this test only.
<snip>
4 out of 70 tests failed (7.11s)
Test suite expr-builder-smtlib2: FAIL
#180 contains a fix for this issue, but it is currently being held up on other things. I think it would be worth isolating the change to only run these tests on Z3 4.8.12 or later for the sake of fixing the CI in the short term.
The text was updated successfully, but these errors were encountered:
Currently, all CI jobs which use Z3 4.8.11 will fail when running the
expr-builder-smtlib2
test suite. Here is an example:#180 contains a fix for this issue, but it is currently being held up on other things. I think it would be worth isolating the change to only run these tests on Z3 4.8.12 or later for the sake of fixing the CI in the short term.
The text was updated successfully, but these errors were encountered: