diff --git a/examples/bmc.rs b/examples/bmc.rs
index a375a0e..7a145ce 100644
--- a/examples/bmc.rs
+++ b/examples/bmc.rs
@@ -14,6 +14,8 @@ use libpatron::*;
 struct Args {
     #[arg(short, long)]
     verbose: bool,
+    #[arg(short, long)]
+    dump_smt: bool,
     #[arg(value_name = "BTOR2", index = 1)]
     filename: String,
 }
@@ -31,7 +33,7 @@ fn main() {
     let checker_opts = mc::SmtModelCheckerOptions {
         check_constraints: true,
         check_bad_states_individually: true,
-        save_smt_replay: false,
+        save_smt_replay: args.dump_smt,
     };
     let solver = mc::BITWUZLA_CMD;
     if args.verbose {
diff --git a/src/mc/smt.rs b/src/mc/smt.rs
index 3695c19..e622e4d 100644
--- a/src/mc/smt.rs
+++ b/src/mc/smt.rs
@@ -473,7 +473,7 @@ impl<'a> TransitionSystemEncoding for UnrollSmtEncoding<'a> {
     }
     fn get_at(&self, smt_ctx: &mut smt::Context, expr: ExprRef, k: u64) -> smt::SExpr {
         assert!(k <= self.current_step.unwrap_or(0));
-        self.get_local_expr_symbol_at(smt_ctx, expr, self.current_step.unwrap())
+        self.get_local_expr_symbol_at(smt_ctx, expr, k)
     }
 }