diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 7558c094..7e155899 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -196,7 +196,7 @@ def output_callback(line):
         nonlocal procs_running
 
         if pending_sim:
-            sim_proc = sim_witness_trace(procname, task, engine_idx, pending_sim, append=sim_append)
+            sim_proc = sim_witness_trace(procname, task, engine_idx, pending_sim, append=sim_append, inductive=mode == "prove_induction")
             sim_proc.register_exit_callback(simple_exit_callback)
             procs_running += 1
             pending_sim = None
diff --git a/sbysrc/sby_sim.py b/sbysrc/sby_sim.py
index 0025ed8e..46584075 100644
--- a/sbysrc/sby_sim.py
+++ b/sbysrc/sby_sim.py
@@ -20,7 +20,7 @@
 from sby_core import SbyProc
 from sby_design import pretty_path
 
-def sim_witness_trace(prefix, task, engine_idx, witness_file, *, append, deps=()):
+def sim_witness_trace(prefix, task, engine_idx, witness_file, *, append, inductive=False, deps=()):
     trace_name = os.path.basename(witness_file)[:-3]
     formats = []
     tracefile = None
@@ -40,8 +40,11 @@ def sim_witness_trace(prefix, task, engine_idx, witness_file, *, append, deps=()
 
     with open(f"{task.workdir}/engine_{engine_idx}/{trace_name}.ys", "w") as f:
         print(f"# running in {task.workdir}/engine_{engine_idx}/", file=f)
-        print(f"read_rtlil ../model/design_prep.il", file=f)
-        print(f"sim -hdlname -summary {trace_name}.json -append {append} -r {trace_name}.yw {' '.join(formats)}", file=f)
+        print("read_rtlil ../model/design_prep.il", file=f)
+        sim_args = ""
+        if inductive:
+            sim_args += " -noinitstate"
+        print(f"sim -hdlname -summary {trace_name}.json -append {append}{sim_args} -r {trace_name}.yw {' '.join(formats)}", file=f)
 
     def exit_callback(retval):