X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=mcexecution.cc;fp=mcexecution.cc;h=d986f517ae751336a97434f06b2c329a9b5567b8;hb=b394fb6e65b7bc1ddaaecd7a916c354a1464cb5c;hp=65df7ce8218a6f74d2d416f2316ae7742204809c;hpb=c8a74edea90ccd70bc7de522a2ffe0530d3d3793;p=satcheck.git

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);