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

Merge pull request #3197 from YosysHQ/claire/smtbmcfix 

Add a bit of flexibilty re AIG witness trace length to smtbmc.py
This commit is contained in:
Claire Xen 2022-02-22 15:26:22 +01:00 committed by GitHub
parent 286caa09bd 30eb7f8665
commit ac294ed419
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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: