correct termination reason from timer_thread

vprover · Jan 7, 2025 · ec0d8cf · ec0d8cf
1 parent 1dc0e45
commit ec0d8cf
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/Lib/Timer.cpp b/Lib/Timer.cpp
@@ -115,6 +115,8 @@ static std::chrono::time_point<std::chrono::steady_clock> START_TIME;
   unsigned limit = env.options->timeLimitInDeciseconds();
   while(true) {
     if(limit && Timer::elapsedDeciseconds() >= limit) {
+      // in principle could have a race on terminationReason, seems unlikely/harmless in practice
+      env.statistics->terminationReason = Shell::Statistics::TIME_LIMIT;
       limitReached(TIME_LIMIT);
     }
 
@@ -123,7 +125,7 @@ static std::chrono::time_point<std::chrono::steady_clock> START_TIME;
       Timer::updateInstructionCount();
       if (env.options->instructionLimit() && LAST_INSTRUCTION_COUNT_READ >= MEGA*(long long)env.options->instructionLimit()) {
         // in principle could have a race on terminationReason, seems unlikely/harmless in practice
-        env.statistics->terminationReason = Shell::Statistics::TIME_LIMIT;
+        env.statistics->terminationReason = Shell::Statistics::INSTUCTION_LIMIT;
         limitReached(INSTRUCTION_LIMIT);
       }
     }

diff --git a/Shell/Statistics.hpp b/Shell/Statistics.hpp
@@ -294,6 +294,8 @@ class Statistics {
     UNKNOWN,
     /** time limit reached */
     TIME_LIMIT,
+    /** instruction limit reached */
+    INSTRUCTION_LIMIT,
     /** memory limit reached */
     MEMORY_LIMIT,
     /** activation limit reached */
@@ -314,6 +316,8 @@ class Statistics {
         return out << "UNKNOWN";
       case TIME_LIMIT:
         return out << "TIME_LIMIT";
+      case INSTRUCTION_LIMIT:
+        return out << "INSTRUCTION_LIMIT";
       case MEMORY_LIMIT:
         return out << "MEMORY_LIMIT";
       case ACTIVATION_LIMIT: