mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

Merge pull request #2163 from levnach/Prover

Browse source 
enable lar_solver::constraint_holds
This commit is contained in:
Nikolaj Bjorner 2019-03-01 08:37:06 -08:00 committed by GitHub
parent 006590f329 69f03952a7
commit 210e448666
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/util/lp/lar_solver.cpp
View file

@ -945,7 +945,6 @@ bool lar_solver::all_constraints_hold() const {
}
bool lar_solver::constraint_holds(const lar_base_constraint & constr, std::unordered_map<var_index, mpq> & var_map) const {
return true;
mpq left_side_val = get_left_side_val(constr, var_map);
switch (constr.m_kind) {
case LE: return left_side_val <= constr.m_right_side;