doDumpStates: incorrectly increments stats

doDumpStates calls stepInstruction and therefore indirectly increases time and
instruction statistics for all dangling (dumped) states. This patch removes the
call, but now the timing stats for the last executed state are lost, as
StatsTracker::stepInstruction isn't called anymore.

2 files changed, 13 insertions, 8 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 1ab82595..794b5980 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2577,15 +2577,11 @@ void Executor::checkMemoryUsage() {
 void Executor::doDumpStates() {
   if (!DumpStatesOnHalt || states.empty())
     return;
+
   klee_message("halting execution, dumping remaining states");
-  for (std::set<ExecutionState *>::iterator it = states.begin(),
-                                            ie = states.end();
-       it != ie; ++it) {
-    ExecutionState &state = **it;
-    stepInstruction(state); // keep stats rolling
-    terminateStateEarly(state, "Execution halting.");
-  }
-  updateStates(0);
+  for (const auto &state : states)
+    terminateStateEarly(*state, "Execution halting.");
+  updateStates(nullptr);
 }
 
 void Executor::run(ExecutionState &initialState) {
diff --git a/test/regression/2018-05-05-number-instructions-dumped-states.c b/test/regression/2018-05-05-number-instructions-dumped-states.c
new file mode 100644
index 00000000..5f2af61e
--- /dev/null
+++ b/test/regression/2018-05-05-number-instructions-dumped-states.c
@@ -0,0 +1,9 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -stop-after-n-instructions=1 --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s
+
+// CHECK: KLEE: done: total instructions = 1
+
+#include "klee/klee.h"
+
+int main(int argc, char * argv[]) {}