diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index 52770aa4c..5cf4cd449 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -1041,9 +1041,7 @@ bool poly_rewriter::hoist_ite(expr* a, obj_hashtable& shared, nume } rational k, g1; if (is_int_numeral(a, k)) { - normalize(k); - g = gcd(g, k); - return !is_minus_one(a) && shared.empty(); + return false; } ptr_buffer adds; TO_BUFFER(is_add, adds, a);