From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 16 Sep 2012 00:49:04 +0000 (+0000)
Subject: store values returned by get-value in TheoryModel::d_reps if necessary, fixes bug... 
X-Git-Tag: cvc5-1.0.0~7807
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fbf887ef14272a13bf1413704d080e8496321338;p=cvc5.git

store values returned by get-value in TheoryModel::d_reps if necessary, fixes bug 382.
---

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 62327e4dc..c4fc0310c 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -425,10 +425,17 @@ Node DefaultModel::getInterpretedValue( TNode n ){
       }
     }
     if( !ret.isNull() ){
+      Node prev = n;
       //store the equality
       assertEquality( n, ret, true );
-      //this is dangerous since it may cause representatives to change
-      Assert( getRepresentative( ret )==ret );
+      //add it to the map of representatives
+      n = d_equalityEngine.getRepresentative( n );
+      if( d_reps.find( n )==d_reps.end() ){
+        d_reps[n] = ret;
+      }
+      //TODO: make sure that this doesn't affect the representatives in the equality engine
+      //  in other words, we need to be sure that all representatives of the equality engine
+      //  are still representatives after this function, or else d_reps should be modified.
       return ret;
     }else{
       //otherwise, just return itself (this usually should not happen)