diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ac5563fb3..c40096e3f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1318,6 +1318,11 @@ void SmtEngine::setDefaults() { options::cbqiMidpoint.set(true); } } + else + { + // cannot use sygus repair constants + options::sygusRepairConst.set(false); + } if(options::forceLogicString.wasSetByUser()) { d_logic = LogicInfo(options::forceLogicString()); @@ -1485,7 +1490,8 @@ void SmtEngine::setDefaults() { // cases where we need produce models if (!options::produceModels() - && (options::produceAssignments() || options::sygusRewSynthCheck())) + && (options::produceAssignments() || options::sygusRewSynthCheck() + || options::sygusRepairConst())) { Notice() << "SmtEngine: turning on produce-models" << endl; setOption("produce-models", SExpr("true")); @@ -5378,6 +5384,11 @@ void SmtEngine::checkSynthSolution() map<Node, Node> sol_map; /* Get solutions and build auxiliary vectors for substituting */ d_theoryEngine->getSynthSolutions(sol_map); + if (sol_map.empty()) + { + Trace("check-synth-sol") << "No solution to check!\n"; + return; + } Trace("check-synth-sol") << "Got solution map:\n"; std::vector<Node> function_vars, function_sols; for (const auto& pair : sol_map) @@ -5462,8 +5473,8 @@ void SmtEngine::checkSynthSolution() else if (r.asSatisfiabilityResult().isSat()) { InternalError( - "SmtEngine::checkSynhtSol(): produced solution allows satisfiable " - "negated conjecture."); + "SmtEngine::checkSynthSolution(): produced solution leads to " + "satisfiable negated conjecture."); } solChecker.resetAssertions(); } |