This F* release supports using Z3 4.13.3 (though this is opt-in and the default is Z3 4.8.5 still). Both Z3 versions are packaged and ready to use.
What's Changed
- Merge F* branch used by EverParse Windows releases (empty PR) by @tahina-pro in #3623
- FStar.Seq.Permutation: stabilize proof by @mtzguido in #3625
- Some normalizer cleanups by @mtzguido in #3624
- --ocamlenv: fix for Windows, cannot use exec by @mtzguido in #3627
- ci: install z3 4.13.3 as well by @mtzguido in #3629
- Disable Div test on Windows by @tahina-pro in #3630
- Added FILELINE and it's test file by @briangmilnes in #3597
- SMT: lazy z3 start, do not start process until we need to ask a query by @mtzguido in #3634
- SMT: fix suggestions about Z3 install by @mtzguido in #3635
- Added missing bij_comp to FStar.Functions.fst* by @briangmilnes in #3633
- Upgrade F* to use Z3 4.13.3 by @nikswamy in #3631
- Add an interface to FStarC.Common by @mtzguido in #3639
- Print a suggestion for a common Windows footgun by @mtzguido in #3640
- Remove squash axioms. by @gebner in #3638
- Adapt CI to the new official Windows opam 2.3 by @tahina-pro in #3641
- Support
get_fstar_z3.shon macos by @gebner in #3646 - Options: print the option's help when arguments are wrong by @mtzguido in #3649
- Introduce --locate_file to ask F* for the location of modules or checked files by @mtzguido in #3650
- Dep: a few tweaks by @mtzguido in #3651
- Dep: revert sorting by @mtzguido in #3654
- Fixes to check-world, and a nightly build by @mtzguido in #3653
- SMTEncoding: prevent hash inconsistencies due to filepaths by @mtzguido in #3652
- Advance to 2025.01.06~dev by @dzomo in #3656
- Fixes for release by @mtzguido in #3657
- nix: enable more systems (e.g. MacOS) by @W95Psp in #3658
Full Changelog: v2024.12.03...v2025.01.07