From ebe8442a6ae50e46635113dd42410d8a9369d8cd Mon Sep 17 00:00:00 2001 From: kn0t Date: Fri, 12 Sep 2025 23:54:39 +0300 Subject: [PATCH] fix: symbolic storage variables in counterexample + add path id to counterexample for debugging/extra purposes --- src/halmos/__main__.py | 2 +- src/halmos/solve.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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