From c06d8682cda4885424d4c937bb3210e67c6eb22e Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Tue, 30 Sep 2025 10:26:36 +1300
Subject: [PATCH 1/3] Fix abc crash when aiger_props is empty

Includes test reproducer from #338, modified to also test `abc --keep-going pdr`.
---
 sbysrc/sby_engine_abc.py    |  4 ++--
 tests/unsorted/no_props.sby | 21 +++++++++++++++++++++
 2 files changed, 23 insertions(+), 2 deletions(-)
 create mode 100644 tests/unsorted/no_props.sby

diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index d8e0189..5bcb66f 100644
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -203,7 +203,7 @@ def run(mode, task, engine_idx, engine):
         match = re.match(r"^Proved output +([0-9]+) in frame +-?[0-9]+", line)
         if match:
             output = int(match[1])
-            prop = aiger_props[output]
+            prop = aiger_props[output] if aiger_props else None
             if prop:
                 prop.status = "PASS"
                 task.summary.add_event(
@@ -232,7 +232,7 @@ def run(mode, task, engine_idx, engine):
                 disproved_count = int(match[3])
                 undecided_count = int(match[4])
                 if (
-                    all_count != len(aiger_props) or
+                    (aiger_props and all_count != len(aiger_props)) or
                     all_count != proved_count + disproved_count + undecided_count or
                     disproved_count != len(disproved) or
                     proved_count != len(proved)
diff --git a/tests/unsorted/no_props.sby b/tests/unsorted/no_props.sby
new file mode 100644
index 0000000..afeeeb2
--- /dev/null
+++ b/tests/unsorted/no_props.sby
@@ -0,0 +1,21 @@
+[tasks]
+abc
+abc_keepgoing
+
+[options]
+mode prove
+
+[engines]
+abc: abc pdr
+abc_keepgoing: abc --keep-going pdr
+
+[script]
+read -sv test.sv
+prep -top top
+
+[file test.sv]
+module top(input i, output o);
+
+assign o = ~i;
+
+endmodule

From db782815f2c79b8fe5d2bd39d3948aaec0b66397 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Tue, 30 Sep 2025 10:31:40 +1300
Subject: [PATCH 2/3] More tests without properties

Used `sby --autotune` to find other engines which fail (though there aren't any other exceptions that I could find).
Parse errors from `abc bmc3` and `abc sim3` instead of returning UNKNOWN.
---
 sbysrc/sby_engine_abc.py    |  3 +++
 tests/unsorted/no_props.sby | 19 ++++++++++++++++---
 2 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 5bcb66f..42dbd0a 100644
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -246,6 +246,9 @@ def run(mode, task, engine_idx, engine):
                 else:
                     proc_status = "FAIL"
 
+        match = re.match("Error: (Does not work|Only works) for (sequential|combinational) networks.", line)
+        if match: proc_status = "ERROR"
+
         return line
 
     def exit_callback(retcode):
diff --git a/tests/unsorted/no_props.sby b/tests/unsorted/no_props.sby
index afeeeb2..6fce5e8 100644
--- a/tests/unsorted/no_props.sby
+++ b/tests/unsorted/no_props.sby
@@ -1,13 +1,26 @@
 [tasks]
-abc
-abc_keepgoing
+abc prove
+abc_keepgoing prove
+
+# "Error: Does not work for combinational networks."
+abc_bmc3 bmc error
+# "Error: Only works for sequential networks."
+abc_sim3 bmc error
+# "Property index 0 is greater than the number of properties in file model/design_btor_single.btor (0)"
+btor_pono bmc error
 
 [options]
-mode prove
+prove: mode prove
+bmc: mode bmc
+cover: mode cover
+error: expect ERROR
 
 [engines]
 abc: abc pdr
 abc_keepgoing: abc --keep-going pdr
+btor_pono: btor pono
+abc_bmc3: abc bmc3
+abc_sim3: abc sim3
 
 [script]
 read -sv test.sv

From d8e276983e90272aa275c692dfa498cb43cf83c3 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Tue, 30 Sep 2025 11:22:13 +1300
Subject: [PATCH 3/3] no_props.sby: Add btor_cover placeholder

The test infrastructure doesn't like when the `cover` tag is used but there is no task that uses it (because it thinks it is a task rather than a tag).
---
 tests/unsorted/no_props.sby | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tests/unsorted/no_props.sby b/tests/unsorted/no_props.sby
index 6fce5e8..f05fc3a 100644
--- a/tests/unsorted/no_props.sby
+++ b/tests/unsorted/no_props.sby
@@ -1,6 +1,7 @@
 [tasks]
 abc prove
 abc_keepgoing prove
+btor_cover cover
 
 # "Error: Does not work for combinational networks."
 abc_bmc3 bmc error
@@ -19,6 +20,7 @@ error: expect ERROR
 abc: abc pdr
 abc_keepgoing: abc --keep-going pdr
 btor_pono: btor pono
+btor_cover: btor btormc
 abc_bmc3: abc bmc3
 abc_sim3: abc sim3