bring back model output in solve_end_to_end

src/halmos/__main__.py

@@ -561,6 +561,7 @@ def log_future_result(future: Future):
                     break
                 elapsed = timedelta(seconds=int(timer.elapsed()))
                 status.update(f"[{elapsed}] solving queries: {done} / {total}")
+
                 time.sleep(0.1)
 
     ctx.thread_pool.shutdown(wait=True)

src/halmos/solve.py

@@ -10,6 +10,7 @@
 from halmos.config import Config as HalmosConfig
 from halmos.constants import VERBOSITY_TRACE_COUNTEREXAMPLE, VERBOSITY_TRACE_PATHS
 from halmos.logs import (
+    COUNTEREXAMPLE_INVALID,
     COUNTEREXAMPLE_UNKNOWN,
     debug,
     error,
@@ -18,7 +19,7 @@
 )
 from halmos.processes import PopenExecutor, PopenFuture, TimeoutExpired
 from halmos.sevm import Exec, SMTQuery
-from halmos.utils import con, stringify
+from halmos.utils import con, red, stringify
 
 
 @dataclass
@@ -467,13 +468,17 @@ def solve_end_to_end(ctx: PathContext) -> None:
         return
 
     if model.is_valid:
+        print(red(f"Counterexample: {model}"))
         fun_ctx.valid_counterexamples.append(model)
 
         # we have a valid counterexample, so we are eligible for early exit
         if args.early_exit:
             debug(f"Shutting down {fun_ctx.info.name}'s solver executor")
             fun_ctx.solver_executor.shutdown(wait=False)
     else:
+        warn_str = f"Counterexample (potentially invalid): {model}"
+        warn_code(COUNTEREXAMPLE_INVALID, warn_str)
+
         fun_ctx.invalid_counterexamples.append(model)