Fix apparent bug...

[satcheck.git] / constgen.cc

diff --git a/constgen.cc b/constgen.cc
index e7f8c2d68004928529c2441d2024b0fe7208d85d..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;
@@ -1762,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();
@@ -1975,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;
                }