diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-04 12:23:34 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-11-04 12:23:34 -0600 |
| commit | 9a2913c2f1a22ed43ed772467ec42ba2262bee17 (patch) | |
| tree | d8465f1a1deefc91397d2f426630c92b7a797133 /src/theory/theory_engine.cpp | |
| parent | 9854e505aeae1ac86ea75e98131dd8643349df60 (diff) | |
Make getSynthSolution return a Bool (#3306)
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0adb592f2..d73babdc0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -944,16 +944,14 @@ TheoryModel* TheoryEngine::getBuiltModel() return d_curr_model; } -void TheoryEngine::getSynthSolutions(std::map<Node, Node>& sol_map) +bool TheoryEngine::getSynthSolutions(std::map<Node, Node>& sol_map) { if (d_quantEngine) { - d_quantEngine->getSynthSolutions(sol_map); - } - else - { - Assert(false); + return d_quantEngine->getSynthSolutions(sol_map); } + // we are not in a quantified logic, there is no synthesis solution + return false; } bool TheoryEngine::presolve() { |