Skip to content

fix: symbolic storage variables in counterexample + add path id to co… #578

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

fix: symbolic storage variables in counterexample + add path id to co… #578

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/halmos/__main__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}"))
Copy link
Collaborator

@daejunpark daejunpark Sep 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this prints as Counterexample: [N], but it might not be obvious to users what the number N means. could you make it to explicitly say that N is the path id?

ctx.valid_counterexamples.append(model)

# add the stacks from the temporary flamegraph to the global one
Expand Down
2 changes: 1 addition & 1 deletion src/halmos/solve.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 "|"
Copy link
Collaborator

@daejunpark daejunpark Sep 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

could you make including storage variables optional behind the --print-full-model flag?

for context: originally, storage variables used to be printed only when --print-full-model was enabled. that feature was somehow dropped in #437 (see the diff in __main__.py), and hasn't been brought back yet.

Copy link
Collaborator

@daejunpark daejunpark Sep 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

also, it looks like the current regex doesn't cover storage mapping variables. could you confirm that as well?

\(\)\s+\(_\s+([^ ]+)\s+ # Capture the SMTLIB type (e.g., "BitVec 256")
(\d+)\)\s+ # Capture the bit-width or type argument
( # Group for the value
Expand Down