diff --git a/sbysrc/sby.py b/sbysrc/sby.py
index 63c9f33..1403658 100644
--- a/sbysrc/sby.py
+++ b/sbysrc/sby.py
@@ -65,6 +65,8 @@ parser.add_argument("--abc", metavar="<path_to_executable>",
         action=DictAction, dest="exe_paths")
 parser.add_argument("--smtbmc", metavar="<path_to_executable>",
         action=DictAction, dest="exe_paths")
+parser.add_argument("--witness", metavar="<path_to_executable>",
+        action=DictAction, dest="exe_paths")
 parser.add_argument("--suprove", metavar="<path_to_executable>",
         action=DictAction, dest="exe_paths")
 parser.add_argument("--aigbmc", metavar="<path_to_executable>",
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 38a31e3..48da97b 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -614,6 +614,7 @@ class SbyTask(SbyConfig):
             "yosys": os.getenv("YOSYS", yosys_program_prefix + "yosys"),
             "abc": os.getenv("ABC", yosys_program_prefix + "yosys-abc"),
             "smtbmc": os.getenv("SMTBMC", yosys_program_prefix + "yosys-smtbmc"),
+            "witness": os.getenv("WITNESS", yosys_program_prefix + "yosys-witness"),
             "suprove": os.getenv("SUPROVE", "suprove"),
             "aigbmc": os.getenv("AIGBMC", "aigbmc"),
             "avy": os.getenv("AVY", "avy"),
diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 7981b77..ace68a0 100644
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -90,19 +90,26 @@ def run(mode, task, engine_idx, engine):
 
         if proc_status == "FAIL" and task.opt_aigsmt != "none":
             trace_prefix = f"engine_{engine_idx}/trace"
-            dump_flags = f"--dump-vcd {trace_prefix}.vcd " if task.opt_vcd else ""
-            dump_flags += f"--dump-yw {trace_prefix}.yw --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc"
+
+            smtbmc_opts = []
+            smtbmc_opts += ["-s", task.opt_aigsmt]
+            if task.opt_tbtop is not None:
+                smtbmc_opts  += ["--vlogtb-top", task.opt_tbtop]
+            smtbmc_opts += ["--noprogress", f"--append {task.opt_append}"]
+            if task.opt_vcd:
+                smtbmc_opts += [f"--dump-vcd {trace_prefix}.vcd"]
+            smtbmc_opts += [f"--dump-yw {trace_prefix}.yw", f"--dump-vlogtb {trace_prefix}_tb.v", f"--dump-smtc {trace_prefix}.smtc"]
+
+            witness_proc = SbyProc(
+                task, f"engine_{engine_idx}", [],
+                f"cd {task.workdir}; {task.exe_paths['witness']} aiw2yw engine_{engine_idx}/trace.aiw model/design_aiger.ywa engine_{engine_idx}/trace.yw",
+            )
 
             proc2 = SbyProc(
                 task,
                 f"engine_{engine_idx}",
-                task.model("smt2"),
-                ("cd {}; {} -s {}{} --noprogress --append {} {dump_flags} --aig model/design_aiger.aim:engine_{i}/trace.aiw --aig-noheader model/design_smt2.smt2").format
-                            (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
-                            "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
-                            task.opt_append,
-                            dump_flags=dump_flags,
-                            i=engine_idx),
+                [*task.model("smt2"), witness_proc],
+                f"cd {task.workdir}; {task.exe_paths['smtbmc']} {' '.join(smtbmc_opts)} --yw engine_{engine_idx}/trace.yw model/design_smt2.smt2",
                 logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
             )
 
diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index e7f8029..293b0cb 100644
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -106,34 +106,32 @@ def run(mode, task, engine_idx, engine):
         if proc_status == "FAIL" and task.opt_aigsmt != "none":
             if produced_cex:
                 trace_prefix = f"engine_{engine_idx}/trace"
-                dump_flags = f"--dump-vcd {trace_prefix}.vcd " if task.opt_vcd else ""
-                dump_flags += f"--dump-yw {trace_prefix}.yw --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc"
 
+                smtbmc_opts = []
                 if mode == "live":
-                    proc2 = SbyProc(
-                        task,
-                        f"engine_{engine_idx}",
-                        task.model("smt2"),
-                        ("cd {}; {} -g -s {}{} --noprogress {dump_flags} --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
-                                    (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
-                                    "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
-                                    dump_flags=dump_flags,
-                                    i=engine_idx),
-                        logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
-                    )
-                else:
-                    proc2 = SbyProc(
-                        task,
-                        f"engine_{engine_idx}",
-                        task.model("smt2"),
-                        ("cd {}; {} -s {}{} --noprogress --append {} {dump_flags} --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
-                                    (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
-                                    "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
-                                    task.opt_append,
-                                    dump_flags=dump_flags,
-                                    i=engine_idx),
-                        logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
-                    )
+                    smtbmc_opts += ["-g"]
+                smtbmc_opts += ["-s", task.opt_aigsmt]
+                if task.opt_tbtop is not None:
+                    smtbmc_opts  += ["--vlogtb-top", task.opt_tbtop]
+                smtbmc_opts += ["--noprogress"]
+                if mode != "live":
+                    smtbmc_opts += [f"--append {task.opt_append}"]
+                if task.opt_vcd:
+                    smtbmc_opts += [f"--dump-vcd {trace_prefix}.vcd"]
+                smtbmc_opts += [f"--dump-yw {trace_prefix}.yw", f"--dump-vlogtb {trace_prefix}_tb.v", f"--dump-smtc {trace_prefix}.smtc"]
+
+                witness_proc = SbyProc(
+                    task, f"engine_{engine_idx}", [],
+                    f"cd {task.workdir}; {task.exe_paths['witness']} aiw2yw engine_{engine_idx}/trace.aiw model/design_aiger.ywa engine_{engine_idx}/trace.yw",
+                )
+
+                proc2 = SbyProc(
+                    task,
+                    f"engine_{engine_idx}",
+                    [*task.model("smt2"), witness_proc],
+                    f"cd {task.workdir}; {task.exe_paths['smtbmc']} {' '.join(smtbmc_opts)} --yw engine_{engine_idx}/trace.yw model/design_smt2.smt2",
+                    logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
+                )
 
                 proc2_status = None