From 66f761a8c54b66b8e6b4667cfb54072ad76952e0 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 8 Aug 2022 15:33:47 +0200 Subject: smtbmc: Set step range for --yw and dont skip steps for --check-witness --- backends/smt2/smtbmc.py | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 3714e2918..5f05287de 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -482,7 +482,8 @@ if cexfile is not None: constr_assumes[step].append((cexfile, smtexpr)) if not got_topt: - skip_steps = max(skip_steps, step) + if not check_witness: + skip_steps = max(skip_steps, step) num_steps = max(num_steps, step+1) if aimfile is not None: @@ -615,7 +616,8 @@ if aimfile is not None: constr_assumes[step].append((cexfile, smtexpr)) if not got_topt: - skip_steps = max(skip_steps, step) + if not check_witness: + skip_steps = max(skip_steps, step) # 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. @@ -623,6 +625,11 @@ if aimfile is not None: step += 1 if inywfile is not None: + if not got_topt: + assume_skipped = 0 + skip_steps = 0 + num_steps = 0 + with open(inywfile, "r") as f: inyw = ReadWitness(f) @@ -717,6 +724,11 @@ if inywfile is not None: smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) constr_assumes[t].append((inywfile, smt_constr)) + if not got_topt: + if not check_witness: + skip_steps = max(skip_steps, t) + num_steps = max(num_steps, t+1) + if btorwitfile is not None: with open(btorwitfile, "r") as f: step = None -- cgit v1.2.3