0.53.0

Changed

• Minimum distance requirements are now asserted for Keccak function calls. They assert that it's hard to generate two Keccak's that are less than 256 afar.
• Keccak concretization is now done only after all simplifications are performed. This helps with simplification pre-concretization
• Added an IllegalOverflow error in case the system tries to allocate a large amount of memory during
  abstract gas execution but concrete running. In these cases, the interpreter can out-of-heap
  as the only check is that the size allocated is less than $2**{64}$, but that is too large to fit in memory. Now,
  we check more stringently, and still return an IllegalOverflow
• Fixed --root option for the test subcommand

Added

• Optimized smt queries that significantly improve performance when dealing with solidity mappings and arrays
• Support for using Bitwuzla as a solver
• More efficient encoding for failure in ds-test style tests
• Symbolic tests now support statically sized arrays as parameters
• hevm test now has a num-solvers parameter that controls how many solver instances to spawn
• New solc-specific simplification rules that should make the final Props a lot more readable
• Prop is now correctly ordered, better BufLength and Max simplifications of Expr,
  and further solc-specific simplifications of Expr
• Simplify earlier and don't check reachability for things statically determined to be FALSE
• New concrete fuzzer that can be controlled via --num-cex-fuzz
• Partial support for dynamic jumps when the jump destination can be computed
  given already available information
• Added three forking cheatcodes: createFork, selectFork, and activeFork

Fixed

• Traces now correctly perform source mapping to display contract details
• Event traces now correctly display indexed arguments and argument names
• JSON reading of foundry JSONs was dependent on locale and did not work with many locales.
• CVC5 needs --incremental flag to work properly in abstraction-refinement mode