Check model only when sat (#1694)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d3489b301a33fd51f08340ee6aacef247f319b43..8450307dbf7a2325495fda6282b462f75e4dce5b 100644 (file)
--- 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.