Skip to content

Commit

Permalink
Update sby_engine_abc.py
Browse files Browse the repository at this point in the history
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)`.
  • Loading branch information
KrystalDelusion authored Mar 11, 2024
1 parent c73cd3e commit 6c8b838
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion sbysrc/sby_engine_abc.py
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down

0 comments on commit 6c8b838

Please sign in to comment.