cleanup: print trace counterexample in the right place

and fix off by one error in num_execs

src/halmos/__main__.py

@@ -473,16 +473,6 @@ def solve_end_to_end_callback(future: Future):
         solver_output = future.result()
         result, model = solver_output.result, solver_output.model
 
-        if args.verbose >= VERBOSITY_TRACE_COUNTEREXAMPLE:
-            id_str = f" #{path_id}" if args.verbose >= VERBOSITY_TRACE_PATHS else ""
-            print(f"Trace{id_str}:")
-            print(ctx.traces[path_id], end="")
-
-        # unsafe, can't print an Exec from a different thread
-        # if args.print_failed_states:
-        #     print(f"# {path_id}")
-        #     print(exec)
-
         if ctx.solving_ctx.executor.is_shutdown():
             # if the thread pool is in the process of shutting down,
             # we want to stop processing remaining models/timeouts/errors, etc.
@@ -501,6 +491,13 @@ def solve_end_to_end_callback(future: Future):
             warn_code(COUNTEREXAMPLE_UNKNOWN, f"Counterexample: {result}")
             return
 
+        # print counterexample trace
+        if args.verbose >= VERBOSITY_TRACE_COUNTEREXAMPLE:
+            path_id = solver_output.path_id
+            id_str = f" #{path_id}" if args.verbose >= VERBOSITY_TRACE_PATHS else ""
+            print(f"Trace{id_str}:")
+            print(ctx.traces[path_id], end="")
+
         if model.is_valid:
             print(red(f"Counterexample: {model}"))
             ctx.valid_counterexamples.append(model)
@@ -609,7 +606,7 @@ def solve_end_to_end_callback(future: Future):
             warn(f"{funsig}: {msg}: --width {args.width}")
             break
 
-    num_execs = path_id
+    num_execs = path_id + 1
 
     # the name is a bit misleading: this timer only starts after the exploration phase is complete
     # but it's possible that solvers have already been running for a while