fix the infinite issue

2 files changed, 7 insertions, 33 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 {
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1f0eee2e2..df55bcf83 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -860,7 +860,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 											//Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y, d_emptyString);
 											//Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, len_z_eq_zero, len_y_eq_zero);
 											
-											Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate();
+											//Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate();
 											//Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, 
 											//						NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]),
 											//						sk_y_len );
@@ -868,9 +868,9 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 											//Node x_eq_y_rest = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], 
 											//						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_x_rest ) );
 											
-											conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, z_neq_empty );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y
-											Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString);
-											conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc );
+											conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y
+											//Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString);
+											//conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc );
 
                                             
 											Node loop_x = normal_forms[other_n_index][other_index];