Halt execution at yield with -Y to simplify SAT formula

[satcheck.git] / mcexecution.cc

diff --git a/mcexecution.cc b/mcexecution.cc
index 59ea44aeb34d6b091b004c8e9f55385c67862bbf..65df7ce8218a6f74d2d416f2316ae7742204809c 100644 (file)
--- 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();
 void MCExecution::threadYield() {
        getOrCreateCurrRecord(YIELD, NULL, 0, 0, 8, false);
        currexecpoint->incrementTop();

+       if (model->params.noexecyields) {
+               threadFinish();
+       }

 }
 
 /** @brief Thread yield. */
 }
 
 /** @brief Thread yield. */