Skip to content

Crux v0.7
Compare
Choose a tag to compare
@RyanGlScott RyanGlScott released this 26 Jun 19:13
· 327 commits to master since this release
crux-v0.7
483560c

New features

  • [LLVM and MIR] Added support for the cvc5 SMT solver.

  • [LLVM] 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.

  • [LLVM] 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.

  • [LLVM] Support LLVM versions up to 16.

Assets 12