Fixed "counterexample trace:" log message for things like warmup failed

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 38222e9c07eb2b4e012454e94edb55991a08823b..efab71413dd1329a41c9c9782c8a7d00079299f9 100644 (file)
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -109,7 +109,8 @@ def run(mode, job, engine_idx, engine):
                 assert task2_status is not None
                 assert task2_status == "FAIL"
 
-                job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
+                if os.path.exists("%s/engine_%d/trace.vcd" % (job.workdir, engine_idx)):
+                    job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
 
             task2.output_callback = output_callback2
             task2.exit_callback = exit_callback2

diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index 1e3594cc980291e6452bbeb3c640cde1b0b23345..b5b20e4f4dd5159a0919b03e5b012b7219645594 100644 (file)
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -128,7 +128,8 @@ def run(mode, job, engine_idx, engine):
                     else:
                         assert task2_status == "FAIL"
 
-                    job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
+                    if os.path.exists("%s/engine_%d/trace.vcd" % (job.workdir, engine_idx)):
+                        job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
 
                 task2.output_callback = output_callback2
                 task2.exit_callback = exit_callback2

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 525f94d498e787aa62d01bbc8db0c2f9b1afcf8c..bea112341eabcb6e244b75da4200c0a18b69bd7a 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -155,7 +155,8 @@ def run(mode, job, engine_idx, engine):
             job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), task_status))
 
             if task_status == "FAIL" and mode != "cover":
-                job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
+                if os.path.exists("%s/engine_%d/trace.vcd" % (job.workdir, engine_idx)):
+                    job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
 
             job.terminate()
 
@@ -172,7 +173,8 @@ def run(mode, job, engine_idx, engine):
 
                 else:
                     job.update_status(task_status)
-                    job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
+                    if os.path.exists("%s/engine_%d/trace.vcd" % (job.workdir, engine_idx)):
+                        job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
                     job.terminate()
 
             elif mode == "prove_induction":