From 96029400cbf661fb5303572923df3f0dc17164ee Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 20 Oct 2022 13:44:45 +0200 Subject: [PATCH] smtbmc: Do not assume skipped assertions when loading a witness trace This is not valid when the prefix of a trace already violates assertions. This can happen when the trace generating solver doesn't look for a minimal length counterexample. --- backends/smt2/smtbmc.py | 3 --- 1 file changed, 3 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 4c1f07229..cb21eb3aa 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -453,7 +453,6 @@ assert topmod in smt.modinfo if cexfile is not None: if not got_topt: - assume_skipped = 0 skip_steps = 0 num_steps = 0 @@ -499,7 +498,6 @@ if aimfile is not None: latch_map = dict() if not got_topt: - assume_skipped = 0 skip_steps = 0 num_steps = 0 @@ -633,7 +631,6 @@ if aimfile is not None: if inywfile is not None: if not got_topt: - assume_skipped = 0 skip_steps = 0 num_steps = 0