-
Notifications
You must be signed in to change notification settings - Fork 262
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.
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
SMT2 back-end: fix inconsistent array flattening #8400
Conversation
We may have `let var=expr in array` expressions, which SMT2 conversion generates (and our in-tree SMT2 solver may have to consume).
Whether we flatten or don't (when datatype support is not available) depends on the expression, but we may need to unflatten when the context expects an array. Fixes: diffblue#8399
d75e3d7
to
af46479
Compare
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8400 +/- ##
========================================
Coverage 78.02% 78.02%
========================================
Files 1726 1726
Lines 189442 189488 +46
Branches 18466 18493 +27
========================================
+ Hits 147808 147850 +42
- Misses 41634 41638 +4 ☔ View full report in Codecov by Sentry. |
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.
Looks ok, would have been nice to have a test from the original issue.
Can we get this merged please? @kroening @martin-cs |
Whether we flatten or don't (when datatype support is not available) depends on the expression, but we may need to unflatten when the context expects an array.
Fixes: #8399