Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492...

(cherry picked from *part* of commit e54c0f73712b25f1d6d49a3817c923eea077da81)

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 713587be267ef959d5291527042503015d45ee22..bbc51c9e0c9cf7b847f39a48b308f1f5e92aa6f6 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -395,6 +395,9 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n)
 
 void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cache)
 {
+  if (n.getKind()==FORALL || n.getKind()==EXISTS) {
+    return;
+  }
   if (cache.find(n) != cache.end()) {
     return;
   }