diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 6ce561b2d..96a26059d 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -76,7 +76,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, Assert (!query.isNull()); initializeSubsolver(checker); // also set the options - checker->setOption("sygus-rr-synth-input", false); + checker->setOption("sygus-rr-synth-input", "false"); checker->setOption("input-language", "smt2"); // Convert bound variables to skolems. This ensures the satisfiability // check is ground. diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 8b741b6d7..9b4a03473 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -237,9 +237,9 @@ bool SygusRepairConst::repairSolution(Node sygusBody, options::sygusRepairConstTimeout.wasSetByUser(), options::sygusRepairConstTimeout()); // renable options disabled by sygus - repcChecker->setOption("miniscope-quant", true); - repcChecker->setOption("miniscope-quant-fv", true); - repcChecker->setOption("quant-split", true); + repcChecker->setOption("miniscope-quant", "true"); + repcChecker->setOption("miniscope-quant-fv", "true"); + repcChecker->setOption("quant-split", "true"); repcChecker->assertFormula(fo_body); // check satisfiability Result r = repcChecker->checkSat(); |