Some solvers failing XstsTest

[RipplB]

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

[mondokm]

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

[mondokm]

cvc5:1.0.8: A dummy assertion has to be added to A in case of interpolation

[szdan97]

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

[mondokm]

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")

[mondokm]

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.

[mondokm]

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.

[mondokm]

princess:2023-06-19: the HashMap had to be replaced with an IdentityHashMap, like in the case of SmtInterpol.

[leventeBajczi]

@RipplB: interpolation was fixed in https://github.com/ftsrg/theta/commit/49de2559. I cannot reproduce the bug with either SMTINTERPOL or PRINCESS.

[leventeBajczi]

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.

[leventeBajczi]

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!

[AdamZsofi]

@RipplB has there been progress with this?