From: Claire Xenia Wolf Date: Fri, 11 Feb 2022 16:24:49 +0000 (+0100) Subject: Add a bit of flexibilty re trace length when processing aiger witnesses in smtbmc.py X-Git-Tag: yosys-0.15~13^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=30eb7f8665bb54ee9e3e25e0508ec6201106ac79;p=yosys.git Add a bit of flexibilty re trace length when processing aiger witnesses in smtbmc.py Signed-off-by: Claire Xenia Wolf --- diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index e5cfcdc08..7e0d8f571 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -583,7 +583,10 @@ if aimfile is not None: if not got_topt: 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 if btorwitfile is not None: