mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fix #3033

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-17 19:14:46 -10:00
parent 23a474655b
commit 1959b7c48a
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/subpaving/tactic/expr2subpaving.cpp
View file

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