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

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index e5cfcdc08a4cbdeb4c6356622f53b8ed955530a2..7e0d8f5710aeb69e313e086803c8d5623ab90cd7 100644 (file)
--- 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: