From 2cb3d671d649abd26311c3c934adef15f79a4965 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 7 Jul 2026 12:19:38 +0200 Subject: [PATCH] yosys-witness: give error on justice property, support only 'b' --- backends/smt2/witness.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py index 83416c695..8c7d455bd 100755 --- a/backends/smt2/witness.py +++ b/backends/smt2/witness.py @@ -192,8 +192,10 @@ def aiw2yw(input, mapfile, output, skip_x, present_only): header_lines = list(itertools.islice(input, 0, 2)) - if len(header_lines) == 2 and header_lines[1][0] in ".bcjf": + if len(header_lines) == 2 and header_lines[1][0] in ".bj": status = header_lines[0].strip() + if header_lines[1][0]=='j': + raise click.ClickException(f"{input_name}: justice property in AIGER witness not yet supported") if status == "0": raise click.ClickException(f"{input_name}: file contains no trace, the AIGER status is unsat") elif status == "2":