mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-05 08:30:50 +00:00
Code Activity

Merge branch 'master' into finite-sets

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-02-18 21:11:44 -08:00 • committed by GitHub
commit 7fe9b1f873
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_arith_value.h
View file

@ -47,8 +47,6 @@ namespace smt {
expr_ref get_lo(expr* e) const; expr_ref get_lo(expr* e) const;
expr_ref get_up(expr* e) const; expr_ref get_up(expr* e) const;
expr_ref get_fixed(expr* e) const; expr_ref get_fixed(expr* e) const;
lbool check_lp_feasible(vector<std::pair<bool, expr_ref>> &ineqs, literal_vector &lit_core,
enode_pair_vector &eq_core);
final_check_status final_check(unsigned ); final_check_status final_check(unsigned );
lbool check_lp_feasible(vector<std::pair<bool, expr_ref>> &ineqs, literal_vector &lit_core, lbool check_lp_feasible(vector<std::pair<bool, expr_ref>> &ineqs, literal_vector &lit_core,
enode_pair_vector &eq_core); enode_pair_vector &eq_core);