diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-17 16:39:48 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-17 16:39:48 +0000 |
| commit | 1417d43cca9eae841cef84d7bc5d245d235daaa1 (patch) | |
| tree | 2cfc3e8220b9401ae40677bc9706617cacf1c97f /src/theory/model.cpp | |
| parent | 249c19d48e6a69ca4b083cae701d51d4ff54cfc5 (diff) | |
minor fix for models, added simple cliques option for uf strong solver
Diffstat (limited to 'src/theory/model.cpp')
| -rw-r--r-- | src/theory/model.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index c4fc0310c..42654b74c 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -432,6 +432,7 @@ Node DefaultModel::getInterpretedValue( TNode n ){ n = d_equalityEngine.getRepresentative( n ); if( d_reps.find( n )==d_reps.end() ){ d_reps[n] = ret; + d_rep_set.add( 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 |