Halt execution at yield with -Y to simplify SAT formula
authorbdemsky <bdemsky@uci.edu>
Wed, 21 Dec 2016 23:10:42 +0000 (15:10 -0800)
committerbdemsky <bdemsky@uci.edu>
Wed, 21 Dec 2016 23:10:42 +0000 (15:10 -0800)
constgen.cc
mcexecution.cc

index e7f8c2d..368cb68 100644 (file)
@@ -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;
                }
@@ -1975,7 +1976,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;
                }
index 59ea44a..65df7ce 100644 (file)
@@ -842,6 +842,9 @@ void MCExecution::threadFinish() {
 void MCExecution::threadYield() {
        getOrCreateCurrRecord(YIELD, NULL, 0, 0, 8, false);
        currexecpoint->incrementTop();
+       if (model->params.noexecyields) {
+               threadFinish();
+       }
 }
 
 /** @brief Thread yield. */