diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-25 17:06:02 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-25 17:39:21 -0500 |
| commit | 6d71aac1070aa7b1a8575722f4022a04b57d5763 (patch) | |
| tree | e51de5c69f3837946b5fad3e8cb9b21ac81d3683 /src/smt | |
| parent | 195dffbb7468e814d3dc3226666688869c13ba3d (diff) | |
fix --check-model --finite-model-find when used together (related to bug 486)
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 77e43d518..66c7e4cbc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2443,7 +2443,7 @@ 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()){ + if(options::checkModels()) { if(r.asSatisfiabilityResult().isSat() == Result::SAT || (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){ checkModel(/* hard failure iff */ ! r.isUnknown()); @@ -2513,7 +2513,7 @@ 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()){ + if(options::checkModels()) { if(r.asSatisfiabilityResult().isSat() == Result::SAT || (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){ checkModel(/* hard failure iff */ ! r.isUnknown()); |