Skip to content

Commit 036ae3f

Browse files
authored
Adding recently fixed Silicon bug to release notes
1 parent 7d8be9d commit 036ae3f

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

Diff for: ReleaseNotes.md

+1
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@
3131
- Fixed unsound definitions of snapshots inside quantifiers with exhaleMode 1 / moreCompleteExhale https://github.com/viperproject/silicon/pull/898
3232
- Fixed unsound constraints for wildcard variables in function axioms with exhaleMode 1 / moreCompleteExhale https://github.com/viperproject/silicon/pull/895
3333
- Fixed case where wildcard amount could be unsoundly constrained against itself https://github.com/viperproject/silicon/pull/893
34+
- Fixed unsound snapshot definitions in function axioms resulting from state consolidation https://github.com/viperproject/silicon/pull/904
3435
- Performance improvements:
3536
- Avoiding generating snapshot definitions that will not be used, reducing potential quantifier instantiations https://github.com/viperproject/silicon/pull/879
3637
- State consolidation now also merged quantified chunks https://github.com/viperproject/silicon/pull/860

0 commit comments

Comments
 (0)