Fix "abc bmc3" engine for small state spaces

diff --git a/sbysrc/sby_bmc.py b/sbysrc/sby_bmc.py
index a0f3d7b3ac9ff347dd9317a793150ae82d44a626..1c146f7f7991d4ea78eb7242cb3c11dd292562b0 100644 (file)
--- a/sbysrc/sby_bmc.py
+++ b/sbysrc/sby_bmc.py
@@ -94,6 +94,9 @@ def run_abc(job, engine_idx, engine):
         match = re.match(r"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line)
         if match: task_status = "FAIL"
 
+        match = re.match(r"^Stopping BMC because all 2\^[0-9]+ reachable states are visited.", line)
+        if match: task_status = "PASS"
+
         match = re.match(r"^No output asserted in [0-9]+ frames.", line)
         if match: task_status = "PASS"