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