From d980ee0533d1113398261f479b1e84ac60db6cb8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Aug 2021 10:00:22 -0700 Subject: [PATCH] fix regression in FPNumRef sign --- src/api/python/z3/z3.py | 2 +- src/cmd_context/cmd_context.cpp | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 25e2a21676a..dfa1298b6eb 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -9581,7 +9581,7 @@ class FPNumRef(FPRef): def sign(self): num = (ctypes.c_int)() - nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) + nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(num)) if nsign is False: raise Z3Exception("error retrieving the sign of a numeral.") return num.value != 0 diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index bd76220b4bc..1e5ce62f323 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1201,7 +1201,11 @@ bool cmd_context::try_mk_pdecl_app(symbol const & s, unsigned num_args, expr * c return true; if (m().is_uninterp(ps) && ps->get_name().is_numerical()) { int index = ps->get_name().get_num(); + if (index < 0) + return false; binding.reserve(index + 1); + if (binding.get(index) && binding.get(index) != s) + return false; binding[index] = s; return true; }