From b394fb6e65b7bc1ddaaecd7a916c354a1464cb5c Mon Sep 17 00:00:00 2001
From: sy2zhao <sy2zhao@edu.uwaterloo.ca>
Date: Wed, 16 Aug 2017 15:40:47 -0400
Subject: [PATCH] Fix MC_Equals to handle NODEP MCIDs.

---
 constgen.cc          |  1 +
 mcexecution.cc       |  9 +++++++++
 test/test_eq_nodep.c | 23 +++++++++++++++++++++++
 3 files changed, 33 insertions(+)
 create mode 100644 test/test_eq_nodep.c

diff --git a/constgen.cc b/constgen.cc
index 368cb68..27c17fb 100644
--- a/constgen.cc
+++ b/constgen.cc
@@ -1763,6 +1763,7 @@ void ConstGen::processEquals(EPRecord *record) {
 		Constraint *l2=getRetValueEncoding(r, constval);
 		Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
 		ADDCONSTRAINT(functionimplication2,"equalsimpl");
+        return;
 	}
 
 	IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
diff --git a/mcexecution.cc b/mcexecution.cc
index 65df7ce..d986f51 100644
--- a/mcexecution.cc
+++ b/mcexecution.cc
@@ -654,6 +654,15 @@ uint64_t MCExecution::equals(MCID op1, uint64_t val1, MCID op2, uint64_t val2, M
 		recordFunctionChange(record, 0);
 		recordFunctionChange(record, 1);
 	}
+
+	if(op1 == MCID_NODEP) {
+		record->getSet(VC_BASEINDEX + 0)->add(val1);
+	}
+
+	if(op2 == MCID_NODEP) {
+		record->getSet(VC_BASEINDEX + 1)->add(val2);
+	}
+
 	MCID eqmcid=getNextMCID();
 	ASSERT(EPList->size()==eqmcid);
 	EPList->push_back(epvalue);
diff --git a/test/test_eq_nodep.c b/test/test_eq_nodep.c
new file mode 100644
index 0000000..0efc1f7
--- /dev/null
+++ b/test/test_eq_nodep.c
@@ -0,0 +1,23 @@
+#include <threads.h>
+#include <inttypes.h>
+#include "libinterface.h"
+
+static int zero;
+
+int user_main(int argc, char **argv)
+{
+    store_32(&zero, 0);
+
+    int val = load_32(&zero);
+
+    int val2 = 0;
+    MCID _mval2 = MCID_NODEP;
+
+    /** this equality check contains one NODEP and should work. **/
+    if(val == val2)
+    {
+        return 1;
+    }
+
+    return 0;
+}
\ No newline at end of file
-- 
2.34.1