diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-03 16:17:24 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-03 16:17:24 -0600 |
| commit | f81c51ca8af1c38126336f0c31a33fba72614dc1 (patch) | |
| tree | 33cab3539b7ecc7b81dcb6890fd612e15d528e70 /src/theory/sep | |
| parent | 72986ccf378dcdbede11d93c70601fdcc5b438ed (diff) | |
Fix for collectModelInfo related to finite types + preregistration. Generalize previous fix for sets, minor changes to Datatypes.
Diffstat (limited to 'src/theory/sep')
| -rw-r--r-- | src/theory/sep/theory_sep.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 81afc0da2..4f31f10b5 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -201,8 +201,13 @@ void TheorySep::computeCareGraph() { void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ){ + set<Node> termSet; + + // Compute terms appearing in assertions and shared terms + computeRelevantTerms(termSet); + // Send the equality engine information to the model - m->assertEqualityEngine( &d_equalityEngine ); + m->assertEqualityEngine( &d_equalityEngine, &termSet ); } void TheorySep::postProcessModel( TheoryModel* m ){ |