Skip to content

nightly-2025-01-30

Pre-release
Pre-release
Compare
Choose a tag to compare
@leodemoura leodemoura released this 30 Jan 08:45
· 1 commit to main since this release
nightly-2025-01-30
e922edf
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Changes since nightly-2025-01-29:

Full commit log

  • e922edf feat: Bool.and, Bool.or, and Bool.not propagation in grind (#6861)
  • 5b1c6b5 feat: align take/drop/extract across List/Array/Vector (#6860)
  • 21e8a99 feat: refactor of find functions on List/Array/Vector (#6833)
  • 49fe87e feat: missing propagation rules in grind (#6858)
  • 61c843a refactor: pull out some LRAT functionality from bv_decide (#6856)
  • ca3c757 chore: update stage0
  • 5075153 feat: better support for inductive predicates in grind (#6854)
  • c7dec60 feat: support UIntX and USize in bv_decide (#6711)
  • 41fe7bc feat: bv_normalize rewrite shifts by BitVec const to shift by Nat const (#6851)
  • 2c00f8f fix: consume mdata in casesOnStuckLHS when checking that major is fvar (#6791)
  • 6865329 chore: re-enable Lake
  • 729d6e5 chore: update stage0
  • c6677e0 perf: avoid environment extension indirection
  • 0c43f05 feat: add BitVec add_self/self_add lemmas (#6848)
  • 3c8cf7a chore: remove unneeded LawfulBEq hypotheses (#6847)
  • 51b56b2 feat: missing monadic functions on List/Array/Vector (#6845)
  • 5c0231f feat: add BitVec add/sub injectivity lemmas (#6828)
Assets 14
Loading