0.11 -- 2025-11-09

• Sync the version number with crux-mir-0.11 as part of the overall Crux 0.10 release.

0.10 -- 2025-03-24

• Sync the version number with crux-mir-0.10 as part of the overall Crux 0.10 release.

0.9.1 -- 2025-03-21

• Add support for the Bitwuzla SMT solver in the test suite.
• Add --debug option for starting the Crucible debugger.
• Emit a warning when parsing an LLVM bitcode metadata record that crux-llvm does not support. (Previously, crux-llvm would throw a fatal error if this occurred, so this change makes crux-llvm more permissive with respect to unsupported LLVM versions.)

0.9 -- 2024-08-30

• Add support for GHC 9.8
• The type signatures in Crux.LLVM.Overrides now use fewer type parameters in the OverrideTemplates that they return, in accordance with downstream changes from crucible-llvm.

0.8 -- 2024-02-05

• Add support for LLVM bitcode files generated by Apple Clang on macOS.

0.7 -- 2023-06-26

New features

• When loading bitcode to execute, we now make use of a new feature of crucible-llvm which delays the translation of the LLVM bitcode until functions are actually called. This should speed up startup times and reduce memory usage for verification tasks where a small subset of functions in a bitcode module are actually executed.

• Added support for the cvc5 SMT solver.

• Added support for getting abducts during online goal solving. With the --get-abducts n option, crux-llvm returns n abducts for each goal that the SMT solver found to be sat. An abduct is a formula that makes the goal unsat (would help the SMT solver prove the goal). This feature only works with the cvc5 SMT solver.

• Support LLVM versions up to 16.

0.6

New features

• Improved support for translating LLVM debug metadata when the debug-intrinsics option is enabled, including metadata that defines metadata nodes after they are used.

• Add overrides for certain floating-point operations such as sin, cos, tan, etc. At the solver level, crux-llvm treats these as uninterpreted functions, so crux-llvm is limited to reasoning about them up to basic, syntactic equivalence checking.

• Certain error messages now print the call stack of functions leading up to the error.

Bug fixes

• Make --help and --version respect the --no-colors flag.

Library changes

• LLVMConfig now has an indeterminateLoadBehavior flag to control the MemOptions option of the same name. Refer to the crucible-llvm changelog for more details.
• A ?memOpts :: MemOptions constraint has been added to Crux.LLVM.Simulate.checkFun.