From 1959b7c48a330d76585e97a208364bf020825341 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 Feb 2020 19:14:46 -1000 Subject: [PATCH] fix #3033 Signed-off-by: Nikolaj Bjorner --- src/math/subpaving/tactic/expr2subpaving.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math/subpaving/tactic/expr2subpaving.cpp b/src/math/subpaving/tactic/expr2subpaving.cpp index b5e27abea..70b86c94d 100644 --- a/src/math/subpaving/tactic/expr2subpaving.cpp +++ b/src/math/subpaving/tactic/expr2subpaving.cpp @@ -267,12 +267,12 @@ struct expr2subpaving::imp { subpaving::var process_power(app * t, unsigned depth, mpz & n, mpz & d) { rational k; SASSERT(t->get_num_args() == 2); - if (!m_autil.is_numeral(t->get_arg(1), k) || !k.is_int() || !k.is_unsigned()) { + if (!m_autil.is_numeral(t->get_arg(1), k) || !k.is_int() || !k.is_unsigned() || k.is_zero()) { qm().set(n, 1); qm().set(d, 1); return mk_var_for(t); } - unsigned _k = k.get_unsigned(); + unsigned _k = k.get_unsigned(); subpaving::var x = process(t->get_arg(0), depth+1, n, d); if (x != subpaving::null_var) { subpaving::power p(x, _k);