From f2697c23c047a0e7b13c26f03823a0dbd428cde3 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 21 Aug 2018 14:00:30 +0200 Subject: [PATCH] Fixed "counterexample trace:" log message for things like warmup failed Signed-off-by: Clifford Wolf --- sbysrc/sby_engine_abc.py | 3 ++- sbysrc/sby_engine_aiger.py | 3 ++- sbysrc/sby_engine_smtbmc.py | 6 ++++-- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 38222e9..efab714 100644 --- 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 1e3594c..b5b20e4 100644 --- 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 525f94d..bea1123 100644 --- 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": -- 2.30.2