mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-29 08:25:51 +00:00
Code Activity

fix trace summary printing

Browse source
This commit is contained in:
N. Engelhardt 2020-05-13 18:15:33 +02:00
parent 842e9a121a
commit 6a95ef33c8
2 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
sbysrc/sby_engine_btor.py
View file

@ -70,15 +70,14 @@ def run(mode, job, engine_idx, engine):
job.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status))
job.summary.append("engine_{} ({}) returned {}".format(engine_idx, " ".join(engine), task_status))
common_state.produced_traces.sort()
if len(common_state.produced_traces) == 0:
job.log("engine_{}: Engine did not produce a counter example.".format(engine_idx))
elif len(common_state.produced_traces) < common_state.print_traces_max:
elif len(common_state.produced_traces) <= common_state.print_traces_max:
job.summary.extend(common_state.produced_traces)
else:
job.summary.extend(common_state.produced_traces[:common_state.print_traces_max])
excess_traces = len(common_state.produced_traces) - common_state.print_traces_max
job.summary.append("and {} further trace{}".format(excess_traces, "s" if excess_traces > 1 else {}))
job.summary.append("and {} further trace{}".format(excess_traces, "s" if excess_traces > 1 else ""))
job.terminate()

2
sbysrc/sby_engine_smtbmc.py
View file

@ -192,7 +192,7 @@ def run(mode, job, engine_idx, engine):
while os.path.exists("{}/engine_{}/trace{}.vcd".format(job.workdir, engine_idx, print_traces_max + excess_traces)):
excess_traces += 1
if excess_traces > 0:
job.summary.append("and {} further trace{}".format(excess_traces, "s" if excess_traces > 1 else {}))
job.summary.append("and {} further trace{}".format(excess_traces, "s" if excess_traces > 1 else ""))
job.terminate()