diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-16 18:28:03 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-17 17:21:26 -0400 |
| commit | 004bcc12f592991db93ffd92cfb5925940c80980 (patch) | |
| tree | 1bb1db6b03f80b4833a681622f211b6bfaa911b9 /src/smt/smt_engine.cpp | |
| parent | cffc449795c777217c6412998c7900ad80c389e8 (diff) | |
Fix bug 516; include some bug testcases.
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b72f52092..2cddc29cf 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3541,6 +3541,12 @@ void SmtEngine::checkModel(bool hardFailure) { Debug("boolean-terms") << "++ got " << n << endl; Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl; + if(Theory::theoryOf(n) != THEORY_REWRITERULES) { + // In case it's a quantifier (or contains one), look up its value before + // simplifying, or the quantifier might be irreparably altered. + n = m->getValue(n); + } + // Simplify the result. n = d_private->simplify(n); Notice() << "SmtEngine::checkModel(): -- simplifies to " << n << endl; @@ -3562,6 +3568,7 @@ void SmtEngine::checkModel(bool hardFailure) { // but don't show up in our substitution map above. n = m->getValue(n); Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n << endl; + AlwaysAssert(n.isConst() || n.getKind() == kind::LAMBDA); // The result should be == true. if(n != NodeManager::currentNM()->mkConst(true)) { |