Fix for fuzzer-found model bug

2 files changed, 40 insertions, 21 deletions

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 826e729fc..3880aaad9 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -210,7 +210,7 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
 }
 
 /** add term */
-void TheoryModel::addTerm( Node n ){
+void TheoryModel::addTerm(TNode n ){
   Assert(d_equalityEngine.hasTerm(n));
   //must collect UF terms
   if (n.getKind()==APPLY_UF) {
@@ -223,7 +223,7 @@ void TheoryModel::addTerm( Node n ){
 }
 
 /** assert equality */
-void TheoryModel::assertEquality( Node a, Node b, bool polarity ){
+void TheoryModel::assertEquality(TNode a, TNode b, bool polarity ){
   if (a == b && polarity) {
     return;
   }
@@ -233,7 +233,7 @@ void TheoryModel::assertEquality( Node a, Node b, bool polarity ){
 }
 
 /** assert predicate */
-void TheoryModel::assertPredicate( Node a, bool polarity ){
+void TheoryModel::assertPredicate(TNode a, bool polarity ){
   if ((a == d_true && polarity) ||
       (a == d_false && (!polarity))) {
     return;
@@ -263,6 +263,8 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>*
       predFalse = ee->areEqual(eqc, d_false);
     }
     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
+    bool first = true;
+    Node rep;
     for (; !eqc_i.isFinished(); ++eqc_i) {
       if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) {
         continue;
@@ -274,28 +276,43 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>*
         else if (predFalse) {
           assertPredicate(*eqc_i, false);
         }
-        else if (eqc != (*eqc_i)) {
-          Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << eqc << "));" << endl;
-          d_equalityEngine.mergePredicates(*eqc_i, eqc, Node::null());
-          Assert(d_equalityEngine.consistent());
+        else {
+          if (first) {
+            rep = (*eqc_i);
+            first = false;
+          }
+          else {
+            Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl;
+            d_equalityEngine.mergePredicates(*eqc_i, rep, Node::null());
+            Assert(d_equalityEngine.consistent());
+          }
         }
       } else {
-        assertEquality(*eqc_i, eqc, true);
+        if (first) {
+          rep = (*eqc_i);
+          first = false;
+        }
+        else {
+          assertEquality(*eqc_i, rep, true);
+        }
       }
     }
   }
 }
 
-void TheoryModel::assertRepresentative( Node n ){
+void TheoryModel::assertRepresentative(TNode n )
+{
   Trace("model-builder-reps") << "Assert rep : " << n << std::endl;
   d_reps[ n ] = n;
 }
 
-bool TheoryModel::hasTerm( Node a ){
+bool TheoryModel::hasTerm(TNode a)
+{
   return d_equalityEngine.hasTerm( a );
 }
 
-Node TheoryModel::getRepresentative( Node a ){
+Node TheoryModel::getRepresentative(TNode a)
+{
   if( d_equalityEngine.hasTerm( a ) ){
     Node r = d_equalityEngine.getRepresentative( a );
     if( d_reps.find( r )!=d_reps.end() ){
@@ -308,7 +325,8 @@ Node TheoryModel::getRepresentative( Node a ){
   }
 }
 
-bool TheoryModel::areEqual( Node a, Node b ){
+bool TheoryModel::areEqual(TNode a, TNode b)
+{
   if( a==b ){
     return true;
   }else if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
@@ -318,7 +336,8 @@ bool TheoryModel::areEqual( Node a, Node b ){
   }
 }
 
-bool TheoryModel::areDisequal( Node a, Node b ){
+bool TheoryModel::areDisequal(TNode a, TNode b)
+{
   if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
     return d_equalityEngine.areDisequal( a, b, false );
   }else{
diff --git a/src/theory/model.h b/src/theory/model.h
index 7ccbe2fc3..e283ee183 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -90,11 +90,11 @@ public:
     *   such as contraining the interpretation of uninterpretted functions,
     *   and adding n to the equality engine of this model
     */
-  virtual void addTerm( Node n );
+  virtual void addTerm(TNode n);
   /** assert equality holds in the model */
-  void assertEquality( Node a, Node b, bool polarity );
+  void assertEquality(TNode a, TNode b, bool polarity);
   /** assert predicate holds in the model */
-  void assertPredicate( Node a, bool polarity );
+  void assertPredicate(TNode a, bool polarity);
   /** assert all equalities/predicates in equality engine hold in the model */
   void assertEqualityEngine(const eq::EqualityEngine* ee, std::set<Node>* termSet = NULL);
   /** assert representative
@@ -103,13 +103,13 @@ public:
     *  case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... )
     *  functions where fullModel = true.
     */
-  void assertRepresentative( Node n );
+  void assertRepresentative(TNode n);
 public:
   /** general queries */
-  bool hasTerm( Node a );
-  Node getRepresentative( Node a );
-  bool areEqual( Node a, Node b );
-  bool areDisequal( Node a, Node b );
+  bool hasTerm(TNode a);
+  Node getRepresentative(TNode a);
+  bool areEqual(TNode a, TNode b);
+  bool areDisequal(TNode a, TNode b);
 public:
   /** get value function for Exprs. */
   Expr getValue( Expr expr ) const;