Remove mergePredicates from EqualityEngine interface (#4305)

This function was equivalent to asserting an equality. Removing it for the sake of simplicity.

1 files changed, 4 insertions, 2 deletions

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index dae7261e5..e96bee410 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -483,8 +483,10 @@ bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee,
             first = false;
           }
           else {
-            Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl;
-            d_equalityEngine->mergePredicates(*eqc_i, rep, Node::null());
+            Node eq = (*eqc_i).eqNode(rep);
+            Trace("model-builder-assertions")
+                << "(assert " << eq << ");" << std::endl;
+            d_equalityEngine->assertEquality(eq, true, Node::null());
             if (!d_equalityEngine->consistent())
             {
               return false;