Skip to content

Commit

Permalink
fix release message
Browse files Browse the repository at this point in the history
Signed-off-by: Nikolaj Bjorner <[email protected]>
  • Loading branch information
NikolajBjorner committed Jan 31, 2023
1 parent e6f8fe3 commit 6d8d8f1
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion RELEASE_NOTES.md
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ Version 4.12.2
implies that the modulus is redundant. This tactic is useful for
benchmarks created by converting bit-vector semantics to integer
reasoning.
- change API function Z3_mk_real to take two int64 as arguments instead of int.
- add API function Z3_mk_real_int64 to take two int64 as arguments. The Z3_mk_real function takes integers.
- Add _simplifiers_ as optional incremental pre-processing to solvers.
They are exposed over the SMTLIB API using the command [`set-simplifier`](https://microsoft.github.io/z3guide/docs/strategies/simplifiers).
Simplifiers are similar to tactics, but they operate on solver state that can be incrementally updated.
Expand Down

0 comments on commit 6d8d8f1

Please sign in to comment.