Fix apparent bug...

[satcheck.git] / constgen.cc

diff --git a/constgen.cc b/constgen.cc
index 82042af420bedfdd4b7b29c084f64aeeb33c081d..ff72bf0b7720848b9620d6ed3dee0a3f47c42d67 100644 (file)
--- a/constgen.cc
+++ b/constgen.cc
@@ -347,7 +347,8 @@ void ConstGen::printRecord(EPRecord *record, int file) {
                doPrint(record,file);
 
                if (record->getType()==LOOPENTER) {
-                       workstack->push_back(record->getNextRecord());
+                       if (record->getNextRecord()!=NULL)
+                               workstack->push_back(record->getNextRecord());
                        workstack->push_back(record->getChildRecord());
                        return;
                }
@@ -982,7 +983,8 @@ bool ConstGen::orderThread(EPRecord *first, EPRecord *second) {
                EPRecord *join=(*joinvec)[i];
                ExecPoint *jp=join->getEP();
                if (jp->get_tid()==thr2 &&
-                               jp->compare(ep2)==CR_AFTER)
+                               jp->compare(ep2)==CR_AFTER &&
+                               join->getJoinThread() == thr1)
                        return true;
        }
        return false;
@@ -1490,19 +1492,20 @@ void ConstGen::computeYieldCond(EPRecord *record) {
        ExecPoint *yieldep=record->getEP();
        EPRecord *prevyield=NULL;
        ExecPoint *prevyieldep=NULL;
-       
+
        for(int i=(int)(yieldlist->size()-1);i>=0;i--) {
                EPRecord *tmpyield=(*yieldlist)[i];
                ExecPoint *tmpep=tmpyield->getEP();
-               //Do we have a previous yield operation
-               if (yieldep->compare(tmpep)==CR_BEFORE) {
+               //Do we have a previous yield operation from the same thread
+               if (tmpep->get_tid()==yieldep->get_tid() &&
+                               yieldep->compare(tmpep)==CR_BEFORE) {
                        //Yes
                        prevyield=tmpyield;
                        prevyieldep=prevyield->getEP();
                        break;
                }
        }
-       
+
        yieldlist->push_back(record);
 
        ModelVector<Constraint *> * novel_branches=new ModelVector<Constraint *>();
@@ -1510,6 +1513,11 @@ void ConstGen::computeYieldCond(EPRecord *record) {
        while(sri->hasNext()) {
                EPRecord * unexploredbranch=sri->next();
                ExecPoint * branchep=unexploredbranch->getEP();
+               if (branchep->get_tid()!=yieldep->get_tid()) {
+                       //wrong thread
+                       continue;
+               }
+
                if (yieldep->compare(branchep)!=CR_BEFORE) {
                        //Branch does not occur before yield, so skip
                        continue;
@@ -1519,9 +1527,8 @@ void ConstGen::computeYieldCond(EPRecord *record) {
                if (prevyield != NULL &&
                                prevyieldep->compare(branchep)==CR_BEFORE) {
                        //Branch occurs before previous yield, so we can safely skip this branch
-                                               continue;
+                       continue;
                }
-
                //This is a branch that could prevent this yield from being executed
                BranchRecord *br=branchtable->get(unexploredbranch);
                Constraint * novel_branch=br->getNewBranch();
@@ -1757,6 +1764,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();
@@ -1970,7 +1978,8 @@ void ConstGen::traverseRecord(EPRecord *record, bool initial) {
                        processRecord(record);
                }
                if (record->getType()==LOOPENTER) {
-                       workstack->push_back(record->getNextRecord());
+                       if (record->getNextRecord()!=NULL)
+                               workstack->push_back(record->getNextRecord());
                        workstack->push_back(record->getChildRecord());
                        return;
                }