From b2b067757ef1187d640022a9b5ab54f98f0e2467 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Tue, 7 Jul 2026 12:50:02 +0200 Subject: [PATCH] don't call yosys-witness on (unsupported) justice witnesses --- sbysrc/sby_engine_aiger.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index ce9d169..c17f6bf 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -181,6 +181,9 @@ def aigsmt_exit_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_vc task.update_status(proc_status) task.summary.set_engine_status(engine_idx, proc_status) task.terminate() + if task.opt_mode == "live": + # we don't have any tools to process or visualize justice (lasso) witnesses + return if proc_status == "FAIL" and (not run_aigsmt or task.opt_aigsmt != "none"): aigsmt_trace_callback(task, engine_idx, proc_status, run_aigsmt=run_aigsmt, smtbmc_vcd=smtbmc_vcd, smtbmc_append=smtbmc_append, sim_append=sim_append)