From 08079a435ba6136de2a329b35d39b500be825673 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 30 Jan 2017 11:39:48 +0100
Subject: [PATCH] Fix "abc bmc3" engine for small state spaces
---
sbysrc/sby_bmc.py | 3 +++
1 file changed, 3 insertions(+)
diff --git a/sbysrc/sby_bmc.py b/sbysrc/sby_bmc.py
index a0f3d7b..1c146f7 100644
--- 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"