From 4a451b10d8ba9f8186789048b08379e19776a4d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Dec 2022 09:07:13 -0800 Subject: [PATCH] add custom coercion for floats. fix #6482 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 05df8186eed..72a3cd05f13 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1194,7 +1194,7 @@ def _coerce_expr_merge(s, a): else: if z3_debug(): _z3_assert(s1.ctx == s.ctx, "context mismatch") - _z3_assert(False, "sort mismatch") + _z3_assert(False, "sort mismatch") else: return s @@ -1207,6 +1207,11 @@ def _coerce_exprs(a, b, ctx=None): a = StringVal(a, b.ctx) if isinstance(b, str) and isinstance(a, SeqRef): b = StringVal(b, a.ctx) + if isinstance(a, float) and isinstance(b, ArithRef): + a = RealVal(a, b.ctx) + if isinstance(b, float) and isinstance(a, ArithRef): + b = RealVal(b, a.ctx) + s = None s = _coerce_expr_merge(s, a) s = _coerce_expr_merge(s, b)