Skip to content

0.3.1

Compare
Choose a tag to compare
@Saloed Saloed released this 30 Dec 15:26
· 83 commits to main since this release
5dbd7fc

Bitwuzla

  1. Fix fp support on windows (rebuild native lib)
  2. Fix Bv values internalization/conversion on windows
  3. Fix fma internalization

Z3

  1. Construct Fp values from biased exponent since unbiased exponent is sometimes incorrect in Z3
  2. Z3 array lambda converter

Core

  1. Fp constructors with biased exponent
  2. Support uninterpreted sorts in model
  3. Fix expression substitution and evaluation in quantifiers
  4. Staged ite expression simplification which is required for function app evaluation in a case of recursievly defined functions.
  5. Simplify select from array lambda
  6. Fix simplification of Bv shifts

Other

  1. Check expression ownership context in all API's
  2. Check that variables in function interpretations always match declaration arguments