From 9e70f04c40674ef5f00b7d07a8529bafe9ff2dfc Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 13 Nov 2012 21:48:33 +0000 Subject: [PATCH] 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. --- src/smt/smt_engine.cpp | 14 ++++++++++---- 1 file 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; -- 2.30.2