From 15370ed784b596d905f88bc2bc47d94e4b521dc4 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Wed, 21 Dec 2016 15:10:42 -0800 Subject: [PATCH] Halt execution at yield with -Y to simplify SAT formula --- constgen.cc | 6 ++++-- mcexecution.cc | 3 +++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/constgen.cc b/constgen.cc index e7f8c2d..368cb68 100644 --- 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; } @@ -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; } diff --git a/mcexecution.cc b/mcexecution.cc index 59ea44a..65df7ce 100644 --- a/mcexecution.cc +++ b/mcexecution.cc @@ -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. */ -- 2.34.1