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

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 62327e4dc6aee92795f042a67cfa36158ab12173..c4fc0310c08bf88cdb239c14cc4275d9fa4f72f0 100644 (file)
--- 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)