From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 4 Feb 2013 18:52:45 +0000 (-0500)
Subject: Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492... 
X-Git-Tag: cvc5-1.0.0~7391^2~20
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=55e24949a3464947d098eeeb627049b04a4af4a3;p=cvc5.git

Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492 and resolves previous issue for bug 486.
(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 713587be2..bbc51c9e0 100644
--- 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;
   }