Fix apparent bug...

[satcheck.git] / mcexecution.cc

diff --git a/mcexecution.cc b/mcexecution.cc
index 59ea44aeb34d6b091b004c8e9f55385c67862bbf..d986f517ae751336a97434f06b2c329a9b5567b8 100644 (file)
--- 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);
@@ -842,6 +851,9 @@ void MCExecution::threadFinish() {
 void MCExecution::threadYield() {
        getOrCreateCurrRecord(YIELD, NULL, 0, 0, 8, false);
        currexecpoint->incrementTop();
+       if (model->params.noexecyields) {
+               threadFinish();
+       }
 }
 
 /** @brief Thread yield. */