diff --git a/src/smt/smt_arith_value.h b/src/smt/smt_arith_value.h index 083d3adc8..7e351e43d 100644 --- a/src/smt/smt_arith_value.h +++ b/src/smt/smt_arith_value.h @@ -47,8 +47,6 @@ namespace smt { expr_ref get_lo(expr* e) const; expr_ref get_up(expr* e) const; expr_ref get_fixed(expr* e) const; - lbool check_lp_feasible(vector> &ineqs, literal_vector &lit_core, - enode_pair_vector &eq_core); final_check_status final_check(unsigned ); lbool check_lp_feasible(vector> &ineqs, literal_vector &lit_core, enode_pair_vector &eq_core);