Activate an option for better quantifiers in CVC4
@@ -98,6 +98,8 @@ class CVC4TheoremProver extends AbstractProverWithAllSat<Void>
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() {
