Abort execution if --only-output-states-covering-new is enabled but its dependency --output-istats is not

3 files changed, 8 insertions, 0 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 1e1a142b..f7c71e8d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -354,6 +354,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
 
   initializeSearchOptions();
 
+  if (OnlyOutputStatesCoveringNew && !StatsTracker::useIStats())
+    klee_error("To use --only-output-states-covering-new, you need to enable --output-istats.");
+
   if (DebugPrintInstructions.isSet(FILE_ALL) ||
       DebugPrintInstructions.isSet(FILE_COMPACT) ||
       DebugPrintInstructions.isSet(FILE_SRC)) {
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 83e1844f..d9ec35aa 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -110,6 +110,10 @@ bool StatsTracker::useStatistics() {
   return OutputStats || OutputIStats;
 }
 
+bool StatsTracker::useIStats() {
+  return OutputIStats;
+}
+
 namespace klee {
   class WriteIStatsTimer : public Executor::Timer {
     StatsTracker *statsTracker;
diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h
index 629a723d..23abac06 100644
--- a/lib/Core/StatsTracker.h
+++ b/lib/Core/StatsTracker.h
@@ -48,6 +48,7 @@ namespace klee {
 
   public:
     static bool useStatistics();
+    static bool useIStats();
 
   private:
     void updateStateStatistics(uint64_t addend);