mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 04:11:21 +00:00
Code Activity

update test in qe_arith

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-12 13:32:35 -07:00
parent 196aed785e
commit 1741671a9c
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/qe/qe_arith.cpp
View file

@ -168,7 +168,7 @@ namespace qe {
unsigned find_max(model& mdl, bool do_pos) { unsigned find_max(model& mdl, bool do_pos) {
unsigned result; unsigned result;
bool found = false; bool found = false;
rational found_val(0), r; rational found_val(0), r, found_c;
expr_ref val(m); expr_ref val(m);
for (unsigned i = 0; i < m_ineq_terms.size(); ++i) { for (unsigned i = 0; i < m_ineq_terms.size(); ++i) {
rational const& ac = m_ineq_coeffs[i]; rational const& ac = m_ineq_coeffs[i];
@ -180,11 +180,15 @@ namespace qe {
if (!found || r > found_val) { if (!found || r > found_val) {
result = i; result = i;
found_val = r; found_val = r;
found_c = ac;
found = true; found = true;
} }
} }
} }
SASSERT(found); SASSERT(found);
if (a.is_int(m_var->x()) && !found_c.is_one()) {
throw cant_project();
}
return result; return result;
} }