Activate an option for better quantifiers in CVC4

baierd · baierd · commit 0ecc5e4172f0 · 2021-12-01T18:07:18.000+01:00
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java
@@ -98,6 +98,8 @@ private void setOptions(int randomSeed, Set<ProverOptions> pOptions) {
     smtEngine.setOption("random-seed", new SExpr(randomSeed));
     // Set Strings option to enable all String features (such as lessOrEquals)
     smtEngine.setOption("strings-exp", new SExpr(true));
+    // Enable more complete quantifier solving
+    smtEngine.setOption("full-saturate-quant", new SExpr(true));
   }
 
   protected void setOptionForIncremental() {

Original file line number	Diff line number	Diff line change
`@@ -98,6 +98,8 @@ private void setOptions(int randomSeed, Set<ProverOptions> pOptions) {`
`98`	`98`	`smtEngine.setOption("random-seed", new SExpr(randomSeed));`
`99`	`99`	`// Set Strings option to enable all String features (such as lessOrEquals)`
`100`	`100`	`smtEngine.setOption("strings-exp", new SExpr(true));`
	`101`	`+ // Enable more complete quantifier solving`
	`102`	`+ smtEngine.setOption("full-saturate-quant", new SExpr(true));`
`101`	`103`	`}`
`102`	`104`
`103`	`105`	`protected void setOptionForIncremental() {`