Skip to content

3.3.0

Latest
Latest
Compare
Choose a tag to compare
@sauclovian-g sauclovian-g released this 24 Mar 23:08
· 8 commits to master since this release
3.3.0
285c30d

Language changes

None

Bug fixes

  • Fix a bug where setting at timeout would cause sbv-yices, sbv-cvc4 and sbc-cvc5 to crash. Uses a deadman timer workaround for yices, due to a known issue.
    (#1808)

  • Update Yices build in CI to fix a crash when running test issue_1807.icry on Mac OS X (ARM64).
    (what4-solvers #58)

  • Fix a bug where using a timeout with a subset of the what4 solvers would cause a runtime error. Includes a version bump for what4 to address a nondeterministic crash when using timeouts with cvc4/5.
    (what4 PR #288) (#1807)

  • Fix #1437, enforce the VSeq invariant that it is not a sequence of bits. Replaces the VSeq constructor with a view-only pattern, and smart constructors mkSeq and finSeq.
    (#1437)

  • Fix #1740, removes duplicated width from word values. Note that since this changes the types, it may require changes to libraries depending on Cryptol.

  • Fix a bug in which splitting a [0] value into type [inf][0] would panic.
    (#1749)

  • Fix a bug in which the free variables of types mentioning newtypes or enums were incorrectly computed.
    (#1773)

  • The reference evaluator now evaluates the toSignedInteger and deepseq primitives instead of panicking.

  • Fix a bug in which a ^^ (x ^^ y) could be incorrectly simplified to a ^^ (x * y) at the type level.
    (#1799)

New features

  • Improved error messages during type inference for bindings. Adds a specific error message for when a binding has more arguments than expected, given its type signature.
    (#1744)

  • Improved warning messages for non-exhaustive guards. Warnings are now ordered by source location.
    (#1798)

  • More aggressive exhaustivity check that is less dependent on guard ordering.
    (#1796)

  • Improved error messages mentioning module parameters
    (#1560)

  • Improved the naming convention for anonymous modules generated by the module system
    (#1810)

  • REPL command :dumptests <FILE> <EXPR> updated to write to stdout when invoked as :dumptests - <EXPR> allowing for easier experimentation and testing.

  • The REPL properly supports tab completion for the :t and :check commands.
    (#1780)

  • Add support for incrementally loading projects via cryptol's --project flag as documented in the reference manual.
    (#1641)

  • Add support for the Bitwuzla SMT solver, which can be selected with :set prover=bitwuzla. If you want to specify a What4 or SBV backend, you can use :set prover=w4-bitwuzla or :set prover=sbv-bitwuzla, respectively.
    (#1786)

  • Add a REPL option tcSmtFile that allows writing typechecker-related SMT solver interactions to a file.

  • The typechecker can now simplify types of the form width (2^^n) to n + 1.
    (#1802)

Assets 22
Loading