diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
index df6ae8cf..2d27d1bb 100644
--- a/src/halmos/__main__.py
+++ b/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)
diff --git a/src/halmos/solve.py b/src/halmos/solve.py
index d46fad74..b93485b4 100644
--- a/src/halmos/solve.py
+++ b/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,6 +468,7 @@ 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
@@ -474,6 +476,9 @@ def solve_end_to_end(ctx: PathContext) -> None:
             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)