diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-26 00:45:38 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-03-25 22:45:38 -0700 |
| commit | f7e0adeae28bae50632edef3ed2325df67a7ee7a (patch) | |
| tree | f0cea0c373a4dc901dbed3e46530fdc827187b90 /src/smt | |
| parent | c03e15c1b4ef6ec62209f2a4906cce5843e80c46 (diff) | |
Check model only when sat (#1694)
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. |