Reset input language for ExprMiner subsolver (#2624)

3 files changed, 26 insertions, 2 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index e65d57770..f3baa8214 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1355,6 +1355,14 @@ header = "options/quantifiers_options.h"
   type       = "unsigned long"
   help       = "timeout (in milliseconds) for satisfiability checks in expression miners"
 
+[[option]]
+  name       = "sygusExprMinerCheckUseExport"
+  category   = "expert"
+  long       = "sygus-expr-miner-check-use-export"
+  type       = "bool"
+  default    = "true"
+  help       = "export expressions to a different ExprManager with different options for satisfiability checks in expression miners"
+
 # CEGQI applied to general quantified formulas
 
 [[option]]
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0a4859971..b1d6df852 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2182,6 +2182,22 @@ void SmtEngine::setDefaults() {
         << endl;
     options::bvLazyRewriteExtf.set(false);
   }
+
+  if (!options::sygusExprMinerCheckUseExport())
+  {
+    if (options::sygusExprMinerCheckTimeout.wasSetByUser())
+    {
+      throw OptionException(
+          "--sygus-expr-miner-check-timeout=N requires "
+          "--sygus-expr-miner-check-use-export");
+    }
+    if (options::sygusRewSynthInput())
+    {
+      throw OptionException(
+          "--sygus-rr-synth-input requires "
+          "--sygus-expr-miner-check-use-export");
+    }
+  }
 }
 
 void SmtEngine::setProblemExtended(bool value)
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 67aa8688c..16e59c119 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -77,8 +77,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
   // check is ground.
   Node squery = convertToSkolem(query);
   NodeManager* nm = NodeManager::currentNM();
-  if (options::sygusExprMinerCheckTimeout.wasSetByUser()
-      || options::sygusRewSynthInput())
+  if (options::sygusExprMinerCheckUseExport())
   {
     // To support a separate timeout for the subsolver, we need to create
     // a separate ExprManager with its own options. This requires that
@@ -91,6 +90,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
       checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true);
       checker->setLogic(smt::currentSmtEngine()->getLogicInfo());
       checker->setOption("sygus-rr-synth-input", false);
+      checker->setOption("input-language", "smt2");
       Expr equery = squery.toExpr().exportTo(&em, varMap);
       checker->assertFormula(equery);
     }