·
58 commits
to develop
since this release
0.9.6.3.3 (2025-03-22)
- Add support for GHC HEAD (9.13) #745.
- Expose SMTLIB define-fun to users of liquid-fixpoint #744.
- Check that expressions in refinements are Bool-sorted #743.
- Fix crashes when a datatype is declared with a
Map_t
field #738. - Simplify expressions in fqout files #741.
0.9.6.3.2 (2025-03-06)
- Expose relatedSymbols from EnvironmentReduction. Needed for improving error messages in LH
#2346. - Support extensionality in PLE #704
- Add a new flag
--etabeta
to reason with lambdas in PLE #705 - Add support for reflected lambdas in PLE #725
- Implement Bags and Maps reasoning with Arrays #703
- Support conditional elaboration of theories for cvc5 #734 - Generate smt2 files only when using
--save
#712 - Parameterize Expr and Reft by the variable type #708 - Preserve location of operators in the parser #721
- Optimize elaboration #736
0.9.6.3.1 (2024-08-21)
- Added support for ghc-9.10.1
- Use
;
for comments in SMTParse (as done in SMTLIB) #700. - Extend SMTParser to support lits e.g. for bitvec #698.
- refactor
Set->Array
elaboration #696. - Fixed the polymorphism-related crash caused by a restrictive Set theory encoding #688.
- Do not constant-fold div by zero #686.
- Copy over the HOF configuraration options in hornFInfo #684.
- Use SMTLIB style serialization/deserialization for Horn queries #683.
- Print SMT preamble to the logfile when constructing context #681.
- Allow reading/saving horn queries from/to JSON #680.
- Extend parser to allow boolean function arguments #678.