From d980ee0533d1113398261f479b1e84ac60db6cb8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
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 25e2a2167..dfa1298b6 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 bd76220b4..1e5ce62f3 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;
}