fix the infinite issue

1 files changed, 3 insertions, 29 deletions

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 63eb301b6..9d13dccb7 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -737,8 +737,8 @@ void TheoryArithPrivate::addSharedTerm(TNode n){
   }
 }
 
-Node TheoryArithPrivate::getModelValue(TNode var) {
-  /*try{
+Node TheoryArithPrivate::getModelValue(TNode term) {
+  try{
     DeltaRational drv = getDeltaValue(term);
     const Rational& delta = d_partialModel.getDelta();
     Rational qmodel = drv.substituteDelta( delta );
@@ -747,33 +747,7 @@ Node TheoryArithPrivate::getModelValue(TNode var) {
     return Node::null();
   } catch (ModelException& me) {
     return Node::null();
-  }*/
-	//if( d_partialModel.hasNode( var ) ){
-	if( var.getKind()==kind::STRING_LENGTH ){
-		Trace("strings-temp") << "Get model value of " << var << std::endl;
-		/*
-		ArithVar v;
-		bool foundV = false;
-	    ArithVariables& avnm = d_partialModel;
-	    ArithVariables::var_iterator vi, vend;
-	    for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
-			if( avnm.asNode(*vi)==var ){
-				v = *vi;
-				foundV = true;
-				break;
-			}
-		}
-		if( foundV ){
-			*/
-		ArithVar v = d_partialModel.asArithVar( var );
-		DeltaRational drv = d_partialModel.getAssignment( v );
-		const Rational& delta = d_partialModel.getDelta();
-		Rational qmodel = drv.substituteDelta( delta );
-		Trace("strings-temp") << "Value is " << drv << ", after subs : " << qmodel << std::endl;
-		return mkRationalNode( qmodel );
-	}
-	//}
-	return var;
+  }
 }
 
 namespace attr {