feat(bv_decide): veir_bv_decide_upto tactic#912
Open
tobiasgrosser wants to merge 1 commit into
Open
Conversation
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
VeIR Benchmarks
Details
| Benchmark suite | Current: 7d91079 | Previous: 4368f8c | Ratio |
|---|---|---|---|
add-fold-worklist/create |
2330000 ns (± 50446) |
2256000 ns (± 63926) |
1.03 |
add-fold-worklist/rewrite |
4078000 ns (± 94942) |
3950000 ns (± 29970) |
1.03 |
add-fold-worklist-local/create |
2335000 ns (± 80789) |
2218000 ns (± 83244) |
1.05 |
add-fold-worklist-local/rewrite |
3469000 ns (± 76998) |
3343000 ns (± 96842) |
1.04 |
add-zero-worklist/create |
2324000 ns (± 102100) |
2208000 ns (± 108954) |
1.05 |
add-zero-worklist/rewrite |
2565000 ns (± 81705) |
2549000 ns (± 69170) |
1.01 |
add-zero-reuse-worklist/create |
1963500 ns (± 114288) |
1975000 ns (± 79912) |
0.99 |
add-zero-reuse-worklist/rewrite |
2173500 ns (± 147103) |
2121000 ns (± 42346) |
1.02 |
mul-two-worklist/create |
2289000 ns (± 258589) |
2238000 ns (± 140133) |
1.02 |
mul-two-worklist/rewrite |
5699500 ns (± 188141) |
5600000 ns (± 413824) |
1.02 |
add-fold-forwards/create |
2300500 ns (± 110718) |
2208000 ns (± 71293) |
1.04 |
add-fold-forwards/rewrite |
3101500 ns (± 41299) |
3090000 ns (± 56043) |
1.00 |
add-zero-forwards/create |
2298000 ns (± 53190) |
2212000 ns (± 39927) |
1.04 |
add-zero-forwards/rewrite |
2031000 ns (± 31467) |
2029000 ns (± 23864) |
1.00 |
add-zero-reuse-forwards/create |
1952000 ns (± 56344) |
1889000 ns (± 75381) |
1.03 |
add-zero-reuse-forwards/rewrite |
1583000 ns (± 38499) |
1592000 ns (± 20611) |
0.99 |
mul-two-forwards/create |
2245000 ns (± 21183) |
2242000 ns (± 69816) |
1.00 |
mul-two-forwards/rewrite |
3755000 ns (± 82612) |
3790000 ns (± 75939) |
0.99 |
add-zero-reuse-first/create |
1939000 ns (± 95894) |
1819000 ns (± 79615) |
1.07 |
add-zero-reuse-first/rewrite |
8000 ns (± 1675) |
8000 ns (± 378) |
1 |
add-zero-lots-of-reuse-first/create |
1927000 ns (± 94309) |
1857000 ns (± 66017) |
1.04 |
add-zero-lots-of-reuse-first/rewrite |
827000 ns (± 38492) |
781000 ns (± 17225) |
1.06 |
This comment was automatically generated by workflow using github-action-benchmark.
tobiasgrosser
changed the title
regehr
approved these changes
Jun 23, 2026
regehr
left a comment
regehr
left a comment
Collaborator
There was a problem hiding this comment.
I understand the top part of this but not the bottom, but LGTM!
math-fehr
reviewed
Jun 28, 2026
math-fehr
left a comment
math-fehr
left a comment
Collaborator
There was a problem hiding this comment.
Looks good to me, I just added a few comments but after that we can merge it
Comment on lines
+89
to
+92
| if solverRes.isSome then | ||
| remainingGoals := remainingGoals ++ [] | ||
| else | ||
| remainingGoals := remainingGoals ++ [subgoal.mvarId] |
Collaborator
There was a problem hiding this comment.
Suggested change
| if solverRes.isSome then | |
| remainingGoals := remainingGoals ++ [] | |
| else | |
| remainingGoals := remainingGoals ++ [subgoal.mvarId] | |
| if solverRes = none then | |
| remainingGoals := remainingGoals ++ [subgoal.mvarId] |
As the then branch is a no-op
| remainingGoals := remainingGoals ++ unclosed | ||
| return remainingGoals | ||
| else | ||
| -- If upper bound is zero (contradiction case), let omega clean it up |
Collaborator
There was a problem hiding this comment.
This is the case of a non-literal symbol, rather than the 0 case?
Comment on lines
+77
to
+79
| -- FIX: We no longer run the solver on the abstract parent goal here. | ||
| -- This prevents the SMT/SAT solver from running on generic, non-instantiated bitwidths | ||
| -- and avoids the "potentially spurious counterexample" error entirely. |
Collaborator
There was a problem hiding this comment.
What is this comment for? Is it for an issue that we should add, or should the comment be removed?
math-fehr
approved these changes
Jun 28, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.