From: Tim King <taking@cs.nyu.edu>
Date: Sat, 13 Jun 2015 21:14:46 +0000 (+0200)
Subject: Restricting TheoryArith to computeRelevantTerms.
X-Git-Tag: cvc5-1.0.0~6279
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=56827afd6b3ba99fd72b927f29e98d80dbd7c2ae;p=cvc5.git

Restricting TheoryArith to computeRelevantTerms.
---

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 786499bf0..616656408 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4180,6 +4180,9 @@ void TheoryArithPrivate::collectModelInfo( TheoryModel* m, bool fullModel ){
 
   Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;
 
+  std::set<Node> termSet;
+  d_containing.computeRelevantTerms(termSet);
+ 
 
   // Delta lasts at least the duration of the function call
   const Rational& delta = d_partialModel.getDelta();
@@ -4194,7 +4197,9 @@ void TheoryArithPrivate::collectModelInfo( TheoryModel* m, bool fullModel ){
     if(!isAuxiliaryVariable(v)){
       Node term = d_partialModel.asNode(v);
 
-      if(theoryOf(term) == THEORY_ARITH || shared.find(term) != shared.end()){
+      if((theoryOf(term) == THEORY_ARITH || shared.find(term) != shared.end())
+         && termSet.find(term) != termSet.end()){
+
         const DeltaRational& mod = d_partialModel.getAssignment(v);
         Rational qmodel = mod.substituteDelta(delta);