From b725bfed0c986777f239f362596b096c8cc05326 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Wed, 30 Mar 2022 13:35:57 +0200
Subject: [PATCH] Prefer the first tracefile for each failing assertion

---
 sbysrc/sby_engine_smtbmc.py         | 3 ++-
 tests/keepgoing_multi_step.check.py | 2 ++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 18cfb09..4ec365d 100644
--- 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 0b7d49e..78c713f 100644
--- 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())
-- 
2.30.2