From 13413d052954fde2f009873995081b1d16606d25 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Jul 2018 15:08:16 -0700 Subject: [PATCH] update for int return value Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 2 +- src/tactic/core/reduce_invertible_tactic.cpp | 6 ++++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 10198fcc5..f6a5b1950 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -2455,7 +2455,7 @@ def _is_numeral(ctx, a): return Z3_is_numeral_ast(ctx.ref(), a) def _is_algebraic(ctx, a): - return Z3_is_algebraic_number(ctx.ref(), a) + return 0 != Z3_is_algebraic_number(ctx.ref(), a) def is_int_value(a): """Return `True` if `a` is an integer value of sort Int. diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index 75b8cae0c..5fe6e9d76 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -178,11 +178,12 @@ private: if (m_bv.is_bv_mul(p)) { expr_ref rest(m); for (expr* arg : *to_app(p)) { - if (arg != v) + if (arg != v) { if (rest) rest = m_bv.mk_bv_mul(rest, arg); else rest = arg; + } } if (!rest) return false; @@ -251,11 +252,12 @@ private: if (m_arith.is_mul(p) && m_arith.is_real(p)) { expr_ref rest(m); for (expr* arg : *to_app(p)) { - if (arg != v) + if (arg != v) { if (rest) rest = m_arith.mk_mul(rest, arg); else rest = arg; + } } if (!rest) return false; expr_ref zero(m_arith.mk_real(0), m);