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: cvc5/cvc5#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 49de2559. I cannot reproduce the bug with either SMTINTERPOL or PRINCESS.

[leventeBajczi]

However, the underlying issue is documented in sosy-lab/java-smt#381, when it gets solved, we should remove our workaround.

[leventeBajczi]

for the rest of the table, I strongly think the proposed soution to #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!