Prefer the first tracefile for each failing assertion

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 18cfb092e5a273740860761a2c064baa63ef754f..4ec365de18b00927eaecd08b65b706328b4b471d 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -210,7 +210,8 @@ def run(mode, task, engine_idx, engine):
         match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line)
         if match and last_prop:
             for p in last_prop:
-                p.tracefile = match[1]
+                if not p.tracefile:
+                    p.tracefile = match[1]
             last_prop = []
             return line
 

diff --git a/tests/keepgoing_multi_step.check.py b/tests/keepgoing_multi_step.check.py
index 0b7d49ebb17c7204df65136cd38979c7cd2a036a..78c713f2b956513b03a53b8ec2f50565d58427cb 100644 (file)
--- a/tests/keepgoing_multi_step.check.py
+++ b/tests/keepgoing_multi_step.check.py
@@ -25,3 +25,5 @@ for task in ["keepgoing_multi_step_bmc", "keepgoing_multi_step_prove"]:
     assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % step_3_7, log_per_trace[3], re.M)
     assert re.search(r"Assert failed in test: %s \(.*\)$" % step_7, log_per_trace[3], re.M)
 
+    pattern = f"Property ASSERT in test at {assert_0} failed. Trace file: engine_0/trace0.vcd"
+    assert re.search(pattern, open(f"{task}/{task}.xml").read())