fix regression in FPNumRef sign

Z3Prover · Aug 18, 2021 · d980ee0 · d980ee0
1 parent b3db9a1
commit d980ee0
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git 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
@@ -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;
         }