Skip to content

Commit 16fdcb2

Browse files
CVC5: Set option "--arrays-exp" to enable support for array constants
1 parent be4a08d commit 16fdcb2

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java

+4
Original file line numberDiff line numberDiff line change
@@ -99,6 +99,10 @@ protected void setSolverOptions(
9999
// Set Strings option to enable all String features (such as lessOrEquals)
100100
pSolver.setOption("strings-exp", "true");
101101

102+
// Enable experimental array features
103+
// Needed when array constants (= with default element) are used
104+
pSolver.setOption("arrays-exp", "true");
105+
102106
// Enable more complete quantifier solving (for more info see CVC5QuantifiedFormulaManager)
103107
pSolver.setOption("full-saturate-quant", "true");
104108
}

0 commit comments

Comments
 (0)