diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-09 19:22:17 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-09 19:22:17 +0000 |
commit | 0db88552a98ce250db69746415b39bd7f7e9ea4f (patch) | |
tree | f48f71260dc2715c1e3e60600bbc2bb54ffbeb3b /src/theory/model.cpp | |
parent | 680d9e20d412afe24a23dcaf3a4e440bcf208fbe (diff) |
More fixes to model code
Diffstat (limited to 'src/theory/model.cpp')
-rw-r--r-- | src/theory/model.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index f218332ac..3d918277f 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -328,7 +328,7 @@ void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){ assertPredicate(*eqc_i, false); } else { - d_equalityEngine.addTerm(*eqc_i); + d_equalityEngine.mergePredicates(*eqc_i, eqc, Node::null()); } } else { assertEquality(*eqc_i, eqc, true); @@ -663,6 +663,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node retNode = NodeManager::currentNM()->mkNode( r.getKind(), children ); if (childrenConst) { retNode = Rewriter::rewrite(retNode); + Assert(retNode.getKind() == kind::APPLY_UF || retNode.isConst()); } } d_normalizedCache[r] = retNode; |