Skip to content

fix: immediately halt execution on assert(false)#572

Merged
daejunpark merged 3 commits intomainfrom
fix/assert-false
Aug 4, 2025
Merged

fix: immediately halt execution on assert(false)#572
daejunpark merged 3 commits intomainfrom
fix/assert-false

Conversation

@daejunpark
Copy link
Collaborator

@daejunpark daejunpark commented Aug 4, 2025

fixes foundry-rs/forge-std#705

previously, halmos didn't immediately halt execution for trivially false assertions, e.g., assert(false). this became problematic with the updated forge-std assertion logic (foundry-rs/forge-std#693), as it led to path explosion in complex tests like snekmate.

this pr fixes the behavior: when an assertion condition is trivially unsat, its execution path is now halted immediately.

if funsig in assert_cheatcode_handler:
vm_assert = assert_cheatcode_handler[funsig](arg)
not_cond = simplify(Not(vm_assert.cond))
cond = vm_assert.cond
Copy link
Contributor

Choose a reason for hiding this comment

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

do we guarantee that vm_assert.cond is already simplify'ed?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

it will be simplified later during ex.check().

Copy link
Contributor

@0xkarmacoma 0xkarmacoma left a comment

Choose a reason for hiding this comment

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

clever!

@daejunpark daejunpark merged commit e20e8f6 into main Aug 4, 2025
43 checks passed
@daejunpark daejunpark deleted the fix/assert-false branch August 4, 2025 23:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Branch Explosion in halmos (Yices SMT Solver) Due to PR #693

2 participants