SmtEngine::checkModel() should only be called if the result is sat or unknown because of incompleteness. Other unknown results are not safe to build models for, timeout, interrupted, etc.

1 files changed, 10 insertions, 4 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 32557e7c8..ad6bad43e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2260,8 +2260,11 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
   Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl;
 
   // Check that SAT results generate a model correctly.
-  if(options::checkModels() && r.asSatisfiabilityResult() != Result::UNSAT) {
-    checkModel(/* hard failure iff */ ! r.isUnknown());
+  if(options::checkModels()){
+    if(r.asSatisfiabilityResult().isSat() == Result::SAT ||
+       (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){
+      checkModel(/* hard failure iff */ ! r.isUnknown());
+    }
   }
 
   return r;
@@ -2324,8 +2327,11 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
   Trace("smt") << "SMT query(" << e << ") ==> " << r << endl;
 
   // Check that SAT results generate a model correctly.
-  if(options::checkModels() && r.asSatisfiabilityResult() != Result::UNSAT) {
-    checkModel(/* hard failure iff */ ! r.isUnknown());
+  if(options::checkModels()){
+    if(r.asSatisfiabilityResult().isSat() == Result::SAT ||
+       (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){
+      checkModel(/* hard failure iff */ ! r.isUnknown());
+    }
   }
 
   return r;