From 6d8d8f197105d86d3af180e382533f2839756f0c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Jan 2023 12:43:05 -0800 Subject: [PATCH] fix release message Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 473be8aae..6cac7cc49 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -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.