diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-13 21:48:33 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-13 21:48:33 +0000 |
commit | 9e70f04c40674ef5f00b7d07a8529bafe9ff2dfc (patch) | |
tree | b59377196037f51c735233bd2fa971f558cf4821 /src | |
parent | 795e5ba8a1138a371409ac9c8e9da78ce652bb94 (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 14 |
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; |