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:37:52 -0500 |
| commit | f837652f6d3a64e31238443b632cc1b7b1b4c804 (patch) | |
| tree | 3df747efeac1b0671f0efffa1a3a9c090efbb5a2 /src/smt | |
| parent | fd29170106da3401dd183b479c84984a16ddcc41 (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()); |