about summary refs log tree commit diff homepage
path: root/include
diff options
context:
space:
mode:
Diffstat (limited to 'include')
-rw-r--r--include/klee/ExecutionState.h6
1 files changed, 3 insertions, 3 deletions
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 6523c456..720488cc 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -122,6 +122,8 @@ public:
   // use on structure
   ExecutionState(const std::vector<ref<Expr> > &assumptions);
 
+  ExecutionState(const ExecutionState& state);
+
   ~ExecutionState();
   
   ExecutionState *branch();
@@ -129,9 +131,7 @@ public:
   void pushFrame(KInstIterator caller, KFunction *kf);
   void popFrame();
 
-  void addSymbolic(const MemoryObject *mo, const Array *array) { 
-    symbolics.push_back(std::make_pair(mo, array));
-  }
+  void addSymbolic(const MemoryObject *mo, const Array *array);
   void addConstraint(ref<Expr> e) { 
     constraints.addConstraint(e); 
   }