ftsrg
Some solvers failing XstsTest
XstsTest on the current master branch runs flawlessly with native legacy Z3 and smtinterpol:2.5-1256. However, the following table highlights issues with some of the available solvers:
| Solver | Failing tests | Reason |
|---|---|---|
| JavaSMT:SMTINTERPOL | 1,7,10,14,15,19,20,22,29,30,31,35,40,43,45,46,48,68, | interpolation can only be done over previously asserted formulas. |
| JavaSMT:SMTINTERPOL | 49,51, | Identifier '+' can not be used, because it is a simple operator. Use FormulaManager#isValidName to check your identifier before using it. |
| JavaSMT:SMTINTERPOL | 52,53,54,55,56,57,67, | Initialized arrays are not supported. |
| JavaSMT:PRINCESS | 1,7,10,13,14,15,16,18,19,20,22,29,30,31,35,40,43,45,46,48,68, | interpolation can only be done over previously asserted formulas. |
| JavaSMT:PRINCESS | 4, | value already present: UF (And) |
| JavaSMT:PRINCESS | 12,49,68, | value already present: UF (GeqZero) |
| JavaSMT:PRINCESS | 51, | next on empty iterator |
| JavaSMT:PRINCESS | 52,53,54,55,56,57,67, | Initialized arrays are not supported. |
| cvc5:1.0.8 | 1,3,4,5,10,16,17,18,19,20,21,22,23,24,25,35,42, | No response in iteration 1 |
| cvc5:1.0.8 | 13,14,15,45,51,54,70, | Possibly cant solve - stopped manually |
| cvc5:1.0.8 | 69, | Could not parse solver output: (error "Array theory solver does not yet support write-chains connecting two different constant arrays") |
| mathsat:5.6.10 | 52, | Possibly cant solve - stopped manually |
| mathsat:5.6.10 | 55,56,57,58,59,60, | Arrays with Bool as argument are not supported |
| princess:2023-06-19 | 7,10,13,14,15,22,38,43,46,48,49,51,56,61,71, | Indexing mismatch on declaration |
| z3:4.12.2 | 1,4,72, | Infinite loop |
| z3:4.12.2 | 13,14,15,22,43,52,53, | Possibly cant solve - stopped manually |
Please note the following:
- "Infinite loop" and "Possibly cant solve" issues might be the same
- Testing cvc5 required removing a lot of tests, so the larger numbers might be misaligned
- Some of these might be known limitations of the solver, but I collected every fail
To the Could not parse solver output: (error "Array theory solver does not yet support write-chains connecting two different constant arrays") error of cvc5:1.0.8: https://github.com/cvc5/cvc5/issues/3065
We should try with a newer version of cvc5
cvc5:1.0.8: A dummy assertion has to be added to A in case of interpolation
cvc5:1.0.8: A dummy assertion has to be added to A in case of interpolation
1.1.0 and 1.1.2 did not return any interpolant for the same simple example either, so a dummy assertion is most likely needed for newer versions as well
mathsat:5.6.10: Arrays with bools as key or value type are simply not supported.
(declare-fun _arr$0_0 () (Array Int Bool))
(error "Arrays with Bool as argument are not supported")
cvc5 1.1.0 and 1.0.9: It seems that pop does not remove declare-fun-s. The following doesn't work with 1.0.9 and 1.1.0, but works with newer or older versions:
(set-option :produce-models true)
(set-logic ALL)
(set-option :print-success true)
(push 1)
(declare-fun _x$0_0 () Int)
(assert (= _x$0_0 0))
(check-sat)
(pop 1)
(push 1)
(declare-fun _x$0_0 () Int)
(error "Cannot bind _x$0_0 to symbol of type Int, maybe the symbol has already been defined?")
cvc5:1.1.1+: The installer had to be modified to unzip the binary.
SmtLibSolverTest and SmtLibItpSolverTest work on Windows (after removing the OS assertions). The uninstall after the tests fails because it lacks permissions to delete the installed solver.
princess:2023-06-19: the HashMap had to be replaced with an IdentityHashMap, like in the case of SmtInterpol.
@RipplB: interpolation was fixed in https://github.com/ftsrg/theta/commit/49de2559. I cannot reproduce the bug with either SMTINTERPOL or PRINCESS.
However, the underlying issue is documented in https://github.com/sosy-lab/java-smt/issues/381, when it gets solved, we should remove our workaround.
for the rest of the table, I strongly think the proposed soution to https://github.com/ftsrg/theta/issues/270 is what we're after here as well. After you fix that issue, please re-test XstsTest with the different solvers again, and update the table so we can resume debugging!
Closing as fixed. Will probably re-visit smt solver issues with @as3810t.