diff --git a/src/math/lp/factorization.h b/src/math/lp/factorization.h index 94c309473..04529d033 100644 --- a/src/math/lp/factorization.h +++ b/src/math/lp/factorization.h @@ -30,13 +30,12 @@ struct factorization_factory; enum class factor_type { VAR, MON }; class factor { - lpvar m_var{ UINT_MAX }; - factor_type m_type{ factor_type::VAR }; - bool m_sign{ false }; + lpvar m_var = UINT_MAX; + factor_type m_type = factor_type::VAR; + bool m_sign = false; public: - factor(): factor(false) {} - explicit factor(lpvar var): m_var(var), m_type(factor_type::VAR), m_sign(false) {} - explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t), m_sign(false) {} + factor() { } + explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t) {} unsigned var() const { return m_var; } factor_type type() const { return m_type; } void set(lpvar v, factor_type t) { m_var = v; m_type = t; } diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 94ddc4d9b..2cf5ac004 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -116,7 +116,7 @@ void order::order_lemma_on_factor_binomial_rm(const monic& ac, bool k, const mon tout << "bd=" << pp_mon_with_vars(_(), bd) << "\n"; ); factor d(_().m_evars.find(ac.vars()[k]).var(), factor_type::VAR); - factor b(false); + factor b; if (c().divide(bd, d, b)) { order_lemma_on_binomial_ac_bd(ac, k, bd, b, d.var()); } @@ -192,7 +192,7 @@ bool order::order_lemma_on_ac_and_bc(const monic& rm_ac, tout << "rm_bd = " << pp_mon_with_vars(_(), rm_bd) << "\n"; tout << "ac_f[k] = "; c().print_factor_with_vars(ac_f[k], tout);); - factor b(false); + factor b; return c().divide(rm_bd, ac_f[k], b) && order_lemma_on_ac_and_bc_and_factors(rm_ac, ac_f[!k], ac_f[k], rm_bd, b); diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index db1986398..40ee967ba 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -444,7 +444,7 @@ struct purify_arith_proc { expr * x = args[0]; bool is_int = u().is_int(x); - expr * k = mk_fresh_var(is_int); + expr * k = mk_fresh_var(false); result = k; mk_def_proof(k, t, result_pr); cache_result(t, result, result_pr); @@ -454,7 +454,7 @@ struct purify_arith_proc { if (y.is_zero()) { expr* p0; if (is_int) { - if (!m_ipower0) m_ipower0 = mk_fresh_var(true); + if (!m_ipower0) m_ipower0 = mk_fresh_var(false); p0 = m_ipower0; } else {