summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/smt_engine.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 073c2ebc5..dfd3c9fee 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4861,6 +4861,7 @@ void SmtEngine::checkSynthSolution()
SmtEngine solChecker(d_exprManager);
solChecker.setLogic(getLogicInfo());
setOption("check-synth-sol", SExpr("false"));
+ setOption("sygus-rec-fun", SExpr("false"));
Trace("check-synth-sol") << "Retrieving assertions\n";
// Build conjecture from original assertions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback