(proof-new) Miscelleneous fixes from proof-new (#5714)

[cvc5.git] / src / theory / datatypes / theory_datatypes.cpp

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 01054372556be9f8fef1ccab94770545ea69ce40..7d5b555c23db4961c8a55bbfde990768a0d3efee 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1044,7 +1044,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
         {
           std::vector<Node> conf;
           conf.push_back(t);
-          conf.push_back(c.eqNode(t[0][0]));
+          conf.push_back(t[0][0].eqNode(c));
           Trace("dt-conflict")
               << "CONFLICT: Tester merge eq conflict : " << conf << std::endl;
           d_im.sendDtConflict(conf, InferId::TESTER_CONFLICT);