-
Notifications
You must be signed in to change notification settings - Fork 1.5k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
remaining perf bug is dealing with very large bit-widths. mod 2^n should be computed natively based on n instead of 2^n because we pre-populate an array with all values up to n. Suppose n is 10000, the array has size 10000.
- Loading branch information
1 parent
f24c5ca
commit 202ce1e
Showing
2 changed files
with
16 additions
and
4 deletions.
There are no files selected for viewing
This file contains 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
This file contains 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
202ce1e
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm seeing a lot of regressions with this patch. Tests are now failing with
smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)
202ce1e
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's the array rewriter bit that is at fault.
202ce1e
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Bug fixed in: 41deed5
The previous code was advancing the store chain one too much. This was happening:
The fixed code produces: