From fbf887ef14272a13bf1413704d080e8496321338 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 16 Sep 2012 00:49:04 +0000 Subject: [PATCH] store values returned by get-value in TheoryModel::d_reps if necessary, fixes bug 382. --- src/theory/model.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) 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) -- 2.30.2