diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
index d768243d..4a45f28e 100644
--- a/src/halmos/__main__.py
+++ b/src/halmos/__main__.py
@@ -949,7 +949,7 @@ def _solve_end_to_end_callback(
             print(ctx.traces[path_id], end="")
 
         if model.is_valid:
-            print(color_error(f"Counterexample: {model}"))
+            print(color_error(f"Counterexample: [{path_id}] {model}"))
             ctx.valid_counterexamples.append(model)
 
             # add the stacks from the temporary flamegraph to the global one
diff --git a/src/halmos/solve.py b/src/halmos/solve.py
index a167811d..ededf573 100644
--- a/src/halmos/solve.py
+++ b/src/halmos/solve.py
@@ -61,7 +61,7 @@ class ModelVariable:
 halmos_var_pattern = re.compile(
     r"""
     \(\s*define-fun\s+               # Match "(define-fun"
-    \|?((?:halmos_|p_)[^ |]+)\|?\s+  # Capture either halmos_* or p_*, optionally wrapped in "|"
+    \|?((?:halmos_|p_)[^ |]+|storage_[^ |]+_00)\|?\s+  # Capture halmos_* or p_* or storage_*_00 optionally wrapped in "|"
     \(\)\s+\(_\s+([^ ]+)\s+          # Capture the SMTLIB type (e.g., "BitVec 256")
     (\d+)\)\s+                       # Capture the bit-width or type argument
     (                                # Group for the value