1 files changed, 61 insertions, 38 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 65762a50b..034ca30e2 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -193,13 +193,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
 
   if (opts.smt.solveIntAsBV > 0)
   {
-    // not compatible with incremental
-    if (opts.base.incrementalSolving)
-    {
-      throw OptionException(
-          "solving integers as bitvectors is currently not supported "
-          "when solving incrementally.");
-    }
     // Int to BV currently always eliminates arithmetic completely (or otherwise
     // fails). Thus, it is safe to eliminate arithmetic. Also, bit-vectors
     // are required.
@@ -253,17 +246,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
 
   if (opts.smt.ackermann)
   {
-    if (opts.base.incrementalSolving)
-    {
-      throw OptionException(
-          "Incremental Ackermannization is currently not supported.");
-    }
-
-    if (logic.isQuantified())
-    {
-      throw LogicException("Cannot use Ackermannization on quantified formula");
-    }
-
     if (logic.isTheoryEnabled(THEORY_UF))
     {
       logic = logic.getUnlockedCopy();
@@ -394,25 +376,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
     opts.smt.produceAssertions = true;
   }
 
-  if (opts.bv.bvAssertInput && opts.smt.produceProofs)
-  {
-    Notice() << "Disabling bv-assert-input since it is incompatible with proofs."
-             << std::endl;
-    opts.bv.bvAssertInput = false;
-  }
-
-  // If proofs are required and the user did not specify a specific BV solver,
-  // we make sure to use the proof producing BITBLAST_INTERNAL solver.
-  if (opts.smt.produceProofs
-      && opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL
-      && !opts.bv.bvSolverWasSetByUser
-      && opts.bv.bvSatSolver == options::SatSolverMode::MINISAT)
-  {
-    Notice() << "Forcing internal bit-vector solver due to proof production."
-             << std::endl;
-    opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
-  }
-
   if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
   {
     /**
@@ -513,6 +476,18 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
 
   // widen the logic
   widenLogic(logic, opts);
+
+  // check if we have any options that are not supported with quantified logics
+  if (logic.isQuantified())
+  {
+    std::stringstream reasonNoQuant;
+    if (incompatibleWithQuantifiers(opts, reasonNoQuant))
+    {
+      std::stringstream ss;
+      ss << reasonNoQuant.str() << " not supported in quantified logics.";
+      throw OptionException(ss.str());
+    }
+  }
 }
 
 void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
@@ -895,7 +870,7 @@ bool SetDefaults::usesSygus(const Options& opts) const
   return false;
 }
 
-bool SetDefaults::incompatibleWithProofs(const Options& opts,
+bool SetDefaults::incompatibleWithProofs(Options& opts,
                                          std::ostream& reason) const
 {
   if (opts.quantifiers.globalNegate)
@@ -912,6 +887,24 @@ bool SetDefaults::incompatibleWithProofs(const Options& opts,
     reason << "sygus";
     return true;
   }
+  // options that are automatically set to support proofs
+  if (opts.bv.bvAssertInput)
+  {
+    Notice()
+        << "Disabling bv-assert-input since it is incompatible with proofs."
+        << std::endl;
+    opts.bv.bvAssertInput = false;
+  }
+  // If proofs are required and the user did not specify a specific BV solver,
+  // we make sure to use the proof producing BITBLAST_INTERNAL solver.
+  if (opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL
+      && !opts.bv.bvSolverWasSetByUser
+      && opts.bv.bvSatSolver == options::SatSolverMode::MINISAT)
+  {
+    Notice() << "Forcing internal bit-vector solver due to proof production."
+             << std::endl;
+    opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
+  }
   return false;
 }
 
@@ -946,6 +939,11 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
                                               std::ostream& reason,
                                               std::ostream& suggest) const
 {
+  if (opts.smt.ackermann)
+  {
+    reason << "ackermann";
+    return true;
+  }
   if (opts.smt.unconstrainedSimp)
   {
     if (opts.smt.unconstrainedSimpWasSetByUser)
@@ -977,6 +975,11 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
              << std::endl;
     opts.quantifiers.sygusInference = false;
   }
+  if (opts.smt.solveIntAsBV > 0)
+  {
+    reason << "solveIntAsBV";
+    return true;
+  }
   return false;
 }
 
@@ -1134,6 +1137,26 @@ bool SetDefaults::safeUnsatCores(const Options& opts) const
   return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS;
 }
 
+bool SetDefaults::incompatibleWithQuantifiers(Options& opts,
+                                              std::ostream& reason) const
+{
+  if (opts.smt.ackermann)
+  {
+    reason << "ackermann";
+    return true;
+  }
+  if (opts.arith.nlRlvMode != options::NlRlvMode::NONE)
+  {
+    // Theory relevance is incompatible with CEGQI and SyQI, since there is no
+    // appropriate policy for the relevance of counterexample lemmas (when their
+    // guard is entailed to be false, the entire lemma is relevant, not just the
+    // guard). Hence, we throw an option exception if quantifiers are enabled.
+    reason << "--nl-ext-rlv";
+    return true;
+  }
+  return false;
+}
+
 void SetDefaults::widenLogic(LogicInfo& logic, Options& opts) const
 {
   bool needsUf = false;