diff --git a/src/btor2/witness.rs b/src/btor2/witness.rs
index 03365d4..16e5771 100644
--- a/src/btor2/witness.rs
+++ b/src/btor2/witness.rs
@@ -5,7 +5,7 @@
 use crate::btor2::parse::tokenize_line;
 use crate::ir;
 use crate::ir::{SignalKind, TypeCheck};
-use crate::mc::{State, Value, Witness};
+use crate::mc::{Value, ValueStore, Witness};
 use std::io::{BufRead, Write};
 
 enum ParserState {
@@ -28,7 +28,7 @@ pub fn parse_witnesses(input: &mut impl BufRead, parse_max: usize) -> Result<Vec
     let mut state = ParserState::Start;
     let mut out = Vec::with_capacity(1);
     let mut wit = Witness::default();
-    let mut inputs = State::default();
+    let mut inputs = ValueStore::default();
 
     let finish_witness = |out: &mut Vec<Witness>, wit: &mut Witness| {
         out.push(std::mem::replace(wit, Witness::default()));
@@ -43,8 +43,9 @@ pub fn parse_witnesses(input: &mut impl BufRead, parse_max: usize) -> Result<Vec
         assert_eq!(at as usize, wit.inputs.len());
         ParserState::ParsingInputsAt(at)
     };
-    let finish_inputs = |wit: &mut Witness, inputs: &mut State| {
-        wit.inputs.push(std::mem::replace(inputs, State::default()));
+    let finish_inputs = |wit: &mut Witness, inputs: &mut ValueStore| {
+        wit.inputs
+            .push(std::mem::replace(inputs, ValueStore::default()));
     };
     let start_state = |line: &str| {
         let at = u64::from_str_radix(&line[1..], 10).unwrap();
diff --git a/src/mc/mod.rs b/src/mc/mod.rs
index 64e961c..d1602a6 100644
--- a/src/mc/mod.rs
+++ b/src/mc/mod.rs
@@ -1,10 +1,12 @@
 // Copyright 2023 The Regents of the University of California
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <laeufer@berkeley.edu>
+mod sim;
 mod smt;
 mod state;
 
+pub use sim::Simulator;
 pub use smt::{
     ModelCheckResult, SmtModelChecker, SmtModelCheckerOptions, SmtSolverCmd, BITWUZLA_CMD,
 };
-pub use state::{State, Value, ValueRef, Witness};
+pub use state::{Value, ValueRef, ValueStore, Witness};
diff --git a/src/mc/sim.rs b/src/mc/sim.rs
new file mode 100644
index 0000000..89db6d2
--- /dev/null
+++ b/src/mc/sim.rs
@@ -0,0 +1,21 @@
+// Copyright 2023 The Regents of the University of California
+// released under BSD 3-Clause License
+// author: Kevin Laeufer <laeufer@berkeley.edu>
+
+use crate::ir::*;
+use crate::mc::ValueStore;
+
+/// Interpreter based simulator for a transition system.
+pub struct Simulator<'a> {
+    ctx: &'a Context,
+    sys: &'a TransitionSystem,
+    state: ValueStore,
+}
+
+impl<'a> Simulator<'a> {
+    pub fn new(ctx: &'a Context, sys: &'a TransitionSystem) -> Self {
+        let types = sys.states().map(|s| s.symbol.get_type(ctx));
+        let state = ValueStore::new(types);
+        Self { ctx, sys, state }
+    }
+}
diff --git a/src/mc/smt.rs b/src/mc/smt.rs
index e622e4d..03c286d 100644
--- a/src/mc/smt.rs
+++ b/src/mc/smt.rs
@@ -7,7 +7,7 @@ use crate::ir::{Expr, ExprRef, GetNode, SignalInfo, SignalKind, Type, TypeCheck}
 use std::borrow::Cow;
 
 use crate::ir::SignalKind::Input;
-use crate::mc::{State, Value, Witness};
+use crate::mc::{Value, ValueStore, Witness};
 use easy_smt as smt;
 
 #[derive(Debug, Clone, Copy)]
@@ -160,7 +160,7 @@ impl SmtModelChecker {
         // collect all inputs
         let inputs = sys.get_signals(|s| s.kind == SignalKind::Input);
         for k in 0..=k_max {
-            let mut input_values = State::default();
+            let mut input_values = ValueStore::default();
             for (input_idx, (input, _)) in inputs.iter().enumerate() {
                 let sym_at = enc.get_at(smt_ctx, *input, k);
                 let value = get_smt_value(smt_ctx, sym_at)?;
diff --git a/src/mc/state.rs b/src/mc/state.rs
index e0f144b..626b251 100644
--- a/src/mc/state.rs
+++ b/src/mc/state.rs
@@ -10,9 +10,9 @@ use num_traits::{Num, Zero};
 #[derive(Debug, Default)]
 pub struct Witness {
     /// The starting state. Contains an optional value for each state.
-    pub init: State,
+    pub init: ValueStore,
     /// The inputs over time. Each entry contains an optional value for each input.
-    pub inputs: Vec<State>,
+    pub inputs: Vec<ValueStore>,
     /// Index of all safety properties (bad state predicates) that are violated by this witness.
     pub failed_safety: Vec<u32>,
 }
@@ -47,9 +47,9 @@ fn smt_tpe_to_storage_tpe(tpe: Type) -> StorageType {
     }
 }
 
-/// Represents concrete values which can be updated, but state cannot be added once created.
+/// Represents concrete values which can be updated.
 #[derive(Debug)]
-pub struct State {
+pub struct ValueStore {
     meta: Vec<Option<StorageMetaData>>,
     longs: Vec<u64>,
     bigs: Vec<BigUint>,
@@ -57,9 +57,9 @@ pub struct State {
     //arrays: Vec<ArrayValue>,
 }
 
-impl Default for State {
+impl Default for ValueStore {
     fn default() -> Self {
-        State {
+        ValueStore {
             meta: Vec::default(),
             longs: Vec::default(),
             bigs: Vec::default(),
@@ -67,9 +67,9 @@ impl Default for State {
     }
 }
 
-impl State {
+impl ValueStore {
     pub fn new(types: impl Iterator<Item = Type>) -> Self {
-        let mut state = State::default();
+        let mut state = ValueStore::default();
         let mut long_count = 0;
         let mut big_count = 0;
         for tpe in types {
@@ -165,24 +165,24 @@ impl State {
         self.meta.is_empty()
     }
 
-    pub fn iter(&self) -> StateIter<'_> {
-        StateIter::new(&self)
+    pub fn iter(&self) -> ValueStoreIter<'_> {
+        ValueStoreIter::new(&self)
     }
 }
 
-pub struct StateIter<'a> {
-    state: &'a State,
+pub struct ValueStoreIter<'a> {
+    state: &'a ValueStore,
     underlying: std::slice::Iter<'a, Option<StorageMetaData>>,
 }
 
-impl<'a> StateIter<'a> {
-    fn new(state: &'a State) -> Self {
+impl<'a> ValueStoreIter<'a> {
+    fn new(state: &'a ValueStore) -> Self {
         let underlying = state.meta.iter();
         Self { state, underlying }
     }
 }
 
-impl<'a> Iterator for StateIter<'a> {
+impl<'a> Iterator for ValueStoreIter<'a> {
     type Item = Option<ValueRef<'a>>;
 
     fn next(&mut self) -> Option<Self::Item> {