diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d3489b301..8450307db 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4866,9 +4866,10 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, // Check that SAT results generate a model correctly. if(options::checkModels()) { - if(r.asSatisfiabilityResult().isSat() == Result::SAT || - (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){ - checkModel(/* hard failure iff */ ! r.isUnknown()); + // TODO (#1693) check model when unknown result? + if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + checkModel(); } } // Check that UNSAT results generate a proof correctly. |