CVC5: set default logic ALL for CVC5.

While most features of CVC5 would also set logic ALL internally by default,
some features, such as separation logic, do not and require an explicit setting upfront.

Author: kfriedberger

src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java

@@ -29,7 +29,7 @@
 
 public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
-  private final boolean generateModels;
+  protected final boolean generateModels;
   private final boolean generateAllSat;
   protected final boolean generateUnsatCores;
   private final boolean generateUnsatCoresOverAssumptions;

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

@@ -50,6 +50,7 @@ abstract class CVC5AbstractProver<T> extends AbstractProverWithAllSat<T> {
   protected final Deque<PersistentMap<String, Term>> assertedTerms = new ArrayDeque<>();
 
   // TODO: does CVC5 support separation logic in incremental mode?
+  //  --> No, CVC5 aborts on addConstraint.
   protected final boolean incremental;
 
   protected CVC5AbstractProver(
@@ -84,15 +85,10 @@ protected void setSolverOptions(
       throw new AssertionError("Unexpected exception", e);
     }
 
-    if (incremental) {
-      pSolver.setOption("incremental", "true");
-    }
-    if (pOptions.contains(ProverOptions.GENERATE_MODELS)) {
-      pSolver.setOption("produce-models", "true");
-    }
-    if (pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE)) {
-      pSolver.setOption("produce-unsat-cores", "true");
-    }
+    pSolver.setOption("incremental", incremental ? "true" : "false");
+    pSolver.setOption("produce-models", generateModels ? "true" : "false");
+    pSolver.setOption("produce-unsat-cores", generateUnsatCores ? "true" : "false");
+
     pSolver.setOption("produce-assertions", "true");
     pSolver.setOption("dump-models", "true");
 
@@ -105,6 +101,15 @@ protected void setSolverOptions(
 
     // Enable more complete quantifier solving (for more info see CVC5QuantifiedFormulaManager)
     pSolver.setOption("full-saturate-quant", "true");
+
+    // if no logic is set in CVC5, select the broadest logic available: "ALL"
+    if (!solver.isLogicSet()) {
+      try {
+        solver.setLogic("ALL");
+      } catch (CVC5ApiException e) {
+        throw new AssertionError("Unexpected exception", e);
+      }
+    }
   }
 
   @Override