1 files changed, 4 insertions, 0 deletions
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 31882cd4..25a874cd 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -18,6 +18,7 @@
 #include "ExecutionState.h"
 #include "UserSearcher.h"
 
+#include "klee/ADT/RNG.h"
 #include "klee/Core/Interpreter.h"
 #include "klee/Expr/ArrayCache.h"
 #include "klee/Expr/ArrayExprOptimizer.h"
@@ -111,6 +112,9 @@ public:
     Unhandled
   };
 
+  /// The random number generator.
+  RNG theRNG;
+
 private:
   static const char *TerminateReasonNames[];