riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Add a bit of flexibilty re trace length when processing aiger witnesses in smtbmc.py 

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
This commit is contained in:
Claire Xenia Wolf 2022-02-11 17:24:49 +01:00
parent fc7d78f071
commit 30eb7f8665
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
backends/smt2/smtbmc.py
View File

@ -583,7 +583,10 @@ if aimfile is not None:
if not got_topt: if not got_topt:
skip_steps = max(skip_steps, step) skip_steps = max(skip_steps, step)
num_steps = max(num_steps, step+1) # some solvers optimize the properties so that they fail one cycle early,
# thus we check the properties in the cycle the aiger witness ends, and
# if that doesn't work, we check the cycle after that as well.
num_steps = max(num_steps, step+2)
step += 1 step += 1
if btorwitfile is not None: if btorwitfile is not None: