diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-08 17:42:50 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-08 17:42:57 +0100 |
| commit | e6150efc1ab45debb10e3ebf560432d8dae68790 (patch) | |
| tree | 7670c4b6b784285303da03ca9e27e8c4bcb5dcf1 /src/theory/theory_model.cpp | |
| parent | 5f4e66786b24d76bcd20cede25473ba326a2e381 (diff) | |
Fix bug with incremental+datatypes. Minor cleanup. Disable regression bug484, enable parsing_ringer.
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 33f6ca9c8..1c62717c8 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -372,6 +372,7 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>* void TheoryModel::assertRepresentative(TNode n ) { Trace("model-builder-reps") << "Assert rep : " << n << std::endl; + Trace("model-builder-reps") << "Rep eqc is : " << getRepresentative( n ) << std::endl; d_reps[ n ] = n; } @@ -684,7 +685,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if(t.isTuple() || t.isRecord()) { t = NodeManager::currentNM()->getDatatypeForTupleRecord(t); } - TypeNode tb = t.getBaseType(); + TypeNode tb = t.getBaseType(); if (!assignOne) { set<Node>* repSet = typeRepSet.getSet(tb); if (repSet != NULL && !repSet->empty()) { |