fix trace summary printing

diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py
index d306230a7af8cb760441e1abcff98725e100058a..b8d538e99e73be7e91b591643cf797845a1c4469 100644 (file)
--- a/sbysrc/sby_engine_btor.py
+++ b/sbysrc/sby_engine_btor.py
@@ -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()
 

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index b94ea45c9f032585bbeb2d6c8ff65a8f6c18f81e..b41947241f3b7d42410fa71619ae5fb485316476 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -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()