More fixes to model code

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index f218332acb8fa4408f7e7e6387ebd93d9c65acfc..3d918277f755f82c3ee653002ec71f4b6675af8c 100644 (file)
--- 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;

diff --git a/src/theory/model.h b/src/theory/model.h
index a10d0a9ac9d14fe289241150ec8afa1b6185591f..3c6d8e116880660d7ad92d91ea27ff21b2892a4d 100644 (file)
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -207,10 +207,10 @@ private:
     }
     Node n = **te;
     while (s->find(n) != s->end()) {
+      ++(*te);
       if (te->isFinished()) {
         return Node();
       }
-      ++(*te);
       n = **te;
     }
     s->insert(n);

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 97dcbad86ab55d40f0fd05a9712aae11426959a6..5cf4a5f9fa4b6e6da8962ec28c53c7bd10aaecef 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -355,8 +355,6 @@ void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason) {
 
 void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) {
   Debug("equality") << d_name << "::eq::mergePredicats(" << p << "," << q << ")" << std::endl;
-  Assert(p.getKind() != kind::EQUAL, "Use assertEquality instead");
-  Assert(q.getKind() != kind::EQUAL, "Use assertEquality instead");
   assertEqualityInternal(p, q, reason);
   propagate();
 }