diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 372cc9b..f05b31d 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -449,6 +449,7 @@ class SbyTask:
                 print("dffunmap", file=f)
                 print("stat", file=f)
                 print("write_btor {}-i design_{m}.info design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f)
+                print("write_btor -s {}-i design_{m}_single.info design_{m}_single.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f)
 
             proc = SbyProc(
                 self,
diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py
index 15344d8..7985b32 100644
--- a/sbysrc/sby_engine_btor.py
+++ b/sbysrc/sby_engine_btor.py
@@ -46,7 +46,7 @@ def run(mode, task, engine_idx, engine):
     elif solver_args[0] == "pono":
         if random_seed:
             task.error("Setting the random seed is not available for the pono solver.")
-        solver_cmd = task.exe_paths["pono"] + f" -v 1 -e bmc -k {task.opt_depth - 1}"
+        solver_cmd = task.exe_paths["pono"] + f" --witness -v 1 -e bmc -k {task.opt_depth - 1}"
 
     else:
         task.error(f"Invalid solver command {solver_args[0]}.")
@@ -153,7 +153,7 @@ def run(mode, task, engine_idx, engine):
                     task,
                     f"engine_{engine_idx}_{common_state.produced_cex}",
                     task.model("btor"),
-                    "cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols --info model/design_btor.info model/design_btor.btor engine_{idx}/trace{i}.wit".format(dir=task.workdir, idx=engine_idx, i=suffix),
+                    "cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols --info model/design_btor{s}.info model/design_btor{s}.btor engine_{idx}/trace{i}.wit".format(dir=task.workdir, idx=engine_idx, i=suffix, s='_single' if solver_args[0] == 'pono' else ''),
                     logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
                 )
                 proc2.output_callback = output_callback2
@@ -216,7 +216,7 @@ def run(mode, task, engine_idx, engine):
     proc = SbyProc(
         task,
         f"engine_{engine_idx}", task.model("btor"),
-        f"cd {task.workdir}; {solver_cmd} model/design_btor.btor",
+        f"cd {task.workdir}; {solver_cmd} model/design_btor{'_single' if solver_args[0]=='pono' else ''}.btor",
         logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
     )
 
diff --git a/tests/multi_assert.sby b/tests/multi_assert.sby
new file mode 100644
index 0000000..818195f
--- /dev/null
+++ b/tests/multi_assert.sby
@@ -0,0 +1,24 @@
+[tasks]
+btormc
+pono
+
+[options]
+mode bmc
+depth 5
+expect fail
+
+[engines]
+btormc: btor btormc
+pono: btor pono
+
+[script]
+read_verilog -sv multi_assert.v
+prep -top test
+
+[file multi_assert.v]
+module test();
+always @* begin
+assert (1);
+assert (0);
+end
+endmodule