Reset input language for ExprMiner subsolver

Currently, the subsolver created by the `ExprMiner` copies all the
options from the main solver, including the input language. When
synthesizing rewrites and checking them with the subsolver, this is
problematic because the default decision engine used by SyGuS is
`--decision=internal` but we want `--decision=justification` for solving
string queries for example. This commit changes the `ExprMiner` to set
the input language of the subsolver to `smt2`, s.t.
`SmtEngine::setDefaults()` chooses the correct decision engine.

1 files changed, 1 insertions, 0 deletions

diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 67aa8688c..ddf377508 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -91,6 +91,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);
     }