From: Tim King <taking@cs.nyu.edu>
Date: Tue, 13 Nov 2012 21:48:33 +0000 (+0000)
Subject: SmtEngine::checkModel() should only be called if the result is sat or unknown because... 
X-Git-Tag: cvc5-1.0.0~7605
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9e70f04c40674ef5f00b7d07a8529bafe9ff2dfc;p=cvc5.git

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.
---

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;