diff --git a/src/tsolvers/egraph/Egraph.h b/src/tsolvers/egraph/Egraph.h
index 50a480089..994b54a28 100644
--- a/src/tsolvers/egraph/Egraph.h
+++ b/src/tsolvers/egraph/Egraph.h
@@ -182,7 +182,7 @@ class Egraph : public TSolver {
     bool childDuplicatesClass(ERef parent, uint32_t childIndex);
 
     //***************************************************************************************************************
-    Map<PTRef, ERef, PTRefHash> negatedTermToERef;
+    Map<PTRef, ERef, PTRefHash> termToNegatedERef;
 
     ELAllocator forbid_allocator;
 
diff --git a/src/tsolvers/egraph/EgraphSolver.cc b/src/tsolvers/egraph/EgraphSolver.cc
index cde889613..ce8b0578d 100644
--- a/src/tsolvers/egraph/EgraphSolver.cc
+++ b/src/tsolvers/egraph/EgraphSolver.cc
@@ -270,7 +270,7 @@ void Egraph::declareTerm(PTRef tr) {
     if (logic.hasSortBool(tr) and not logic.isDisequality(tr) and PTRefERefPairVec.size() == 2) {
         auto [negated_tr, negated_er] = PTRefERefPairVec[1];
         assert(logic.isNot(negated_tr));
-        negatedTermToERef.insert(negated_tr, negated_er);
+        termToNegatedERef.insert(tr, negated_er);
         assert(PTRefERefPairVec[0].tr == logic.mkNot(PTRefERefPairVec[1].tr));
         assertNEq(PTRefERefPairVec[0].er, PTRefERefPairVec[1].er, Expl(Expl::Type::pol, PtAsgn_Undef, PTRefERefPairVec[0].tr));
     }
@@ -349,8 +349,8 @@ bool Egraph::addTrue(PTRef term) {
     assert(logic.hasSortBool(term));
     assert(not logic.isNot(term));
     bool res = assertEq(term, logic.getTerm_true(), PtAsgn(term, l_True));
-    if (res and negatedTermToERef.has(logic.mkNot(term))) {
-        res = assertEq(logic.mkNot(term), logic.getTerm_false(), PtAsgn(term, l_True));
+    if (res and termToNegatedERef.has(term)) {
+        res = assertEq(termToNegatedERef[term], termToERef(logic.getTerm_false()), PtAsgn(term, l_True));
     }
 #ifdef STATISTICS
     if (res == false)
@@ -366,8 +366,8 @@ bool Egraph::addFalse(PTRef term) {
     assert(logic.hasSortBool(term));
     assert(not logic.isNot(term));
     bool res = assertEq(term, logic.getTerm_false(), PtAsgn(term, l_False));
-    if (res and negatedTermToERef.has(logic.mkNot(term))) {
-        res = assertEq(logic.mkNot(term), logic.getTerm_true(), PtAsgn(term, l_False));
+    if (res and termToNegatedERef.has(term)) {
+        res = assertEq(termToNegatedERef[term], termToERef(logic.getTerm_true()), PtAsgn(term, l_False));
     }
 #ifdef STATISTICS
     if (res == false)