SmtEngine::checkModel() should only be called if the result is sat or unknown because...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 32557e7c8d6c0433c27860bc9660473de4d2197c..ad6bad43e310ccbf0042b30b8d96b501943b89fc 100644 (file)
--- 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;