Restricting TheoryArith to computeRelevantTerms.

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 786499bf0f10e874cba450dba92dfb75b336265b..61665640829c5d74feb8f7131b4a52247ea87fc3 100644 (file)
--- 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);