2025-03-10
* Version bump (4.3). (#82)
* Add `smtSolver` option to `VerifierOptions`. (#78)
* Add `smtFloatMode` option to `VerifierOptions`. (#79)
2025-01-20
* Version bump (4.2). (#76)
* Reject specs that use multiple triggers with the same name. (#74)
2024-11-08
* Version bump (4.1). (#72)
2024-09-09
* Version bump (4.0). (#69)
* Support verifying programs that use array updates. (#63)
* Support verifying programs that use struct updates. (#57)
2024-08-03
* Support building with `crucible-llvm-0.7` and `crux-llvm-0.9`. (#64)
* Support GHC 9.4 through 9.8. (#65)
2024-07-30
* When using `Noisy` verbosity, always log proof goals related to the
core correspondence proof, even if the goals are trivial. (#51)
* When using `Noisy` verbosity, log more information about which proof
goals arise before or after calling the `step()` function. (#52)
2024-07-11
* Version bump (3.20). (#58)
2024-03-08
* Version bump (3.19). (#53)
* Provide more detailed feedback upon a successful run of the verifier.
* Make the examples build with Copilot 3.19. (#53)
2024-02-06
* Initial release of `copilot-verifier`.