Merge branch '1.0.x'

Conflicts:
	src/theory/quantifiers/theory_quantifiers.cpp

1 files changed, 7 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0f0012971..2ba1ae7a9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3338,6 +3338,7 @@ void SmtEngine::checkModel(bool hardFailure) {
       hash_map<Node, Node, NodeHashFunction> cache;
       n = d_private->expandDefinitions(n, cache);
     }
+    Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
 
     // Apply our model value substitutions.
     n = substitutions.apply(n);
@@ -3359,6 +3360,12 @@ void SmtEngine::checkModel(bool hardFailure) {
       continue;
     }
 
+    // As a last-ditch effort, ask model to simplify it.
+    // Presently, this is only an issue for quantifiers, which can have a value
+    // but don't show up in our substitution map above.
+    n = m->getValue(n);
+    Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n << endl;
+
     // The result should be == true.
     if(n != NodeManager::currentNM()->mkConst(true)) {
       Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"