From 6c8b838eb3c9cbc2f3452855fb6fda3362fefdb6 Mon Sep 17 00:00:00 2001 From: KrystalDelusion <93062060+KrystalDelusion@users.noreply.github.com> Date: Tue, 12 Mar 2024 10:48:26 +1300 Subject: [PATCH] Update sby_engine_abc.py ABC will sometimes return negative frame numbers when proving by convergence, e.g. ``` engine_0: Proved output 1 in frame -698905656 (converged). engine_0: Proved output 4 in frame -698905656 (converged). ``` This change fixes these properties being missed and causing the engine status to return UNKNOWN due to `proved_count != len(proved)`. --- sbysrc/sby_engine_abc.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 54ff1698..1fabe6fa 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -182,7 +182,7 @@ def output_callback(line): match = re.match(r"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line) if match: proc_status = "FAIL" - match = re.match(r"^Proved output +([0-9]+) in frame +[0-9]+", line) + match = re.match(r"^Proved output +([0-9]+) in frame +-?[0-9]+", line) if match: output = int(match[1]) prop = aiger_props[output]