for morgan to see the regression problems

1 files changed, 10 insertions, 0 deletions

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 7e5c01291..63eb301b6 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -738,6 +738,16 @@ void TheoryArithPrivate::addSharedTerm(TNode n){
 }
 
 Node TheoryArithPrivate::getModelValue(TNode var) {
+  /*try{
+    DeltaRational drv = getDeltaValue(term);
+    const Rational& delta = d_partialModel.getDelta();
+    Rational qmodel = drv.substituteDelta( delta );
+    return mkRationalNode( qmodel );
+  } catch (DeltaRationalException& dr) {
+    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;