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);