mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
fix OSX build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
77008dc411
commit
78be471908
|
@ -56,7 +56,6 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
|
|||
bool m_anum_simp;
|
||||
bool m_elim_rem;
|
||||
bool m_eq2ineq;
|
||||
bool m_process_all_eqs;
|
||||
unsigned m_max_degree;
|
||||
|
||||
void get_coeffs_gcd(expr * t, numeral & g, bool & first, unsigned & num_consts);
|
||||
|
|
|
@ -1010,7 +1010,6 @@ bool poly_rewriter<Config>::is_var_plus_ground(expr * n, bool & inv, var * & v,
|
|||
stop = true;
|
||||
}
|
||||
if (is_ground(arg)) {
|
||||
TRACE("model_checker_bug", tout << "pushing:\n" << mk_pp(arg, m()) << "\n";);
|
||||
args.push_back(arg);
|
||||
}
|
||||
else if (is_var(arg)) {
|
||||
|
|
Loading…
Reference in a new issue