mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Fix bug

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-11 17:55:03 -08:00
parent 3cc072f3a7
commit 5ce70eb521
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/math/realclosure/realclosure.cpp
View file

@ -1925,7 +1925,7 @@ namespace realclosure {
SASSERT(new_M_s.m() == new_taqrs.size());
SASSERT(new_M_s.m() == new_prs.size());
// The system must have a solution
sc_cardinalities.resize(new_taqrs.size());
sc_cardinalities.resize(new_taqrs.size(), 0);
// Solve
// new_M_s * sc_cardinalities = new_taqrs
VERIFY(mm().solve(new_M_s, sc_cardinalities.c_ptr(), new_taqrs.c_ptr()));
@ -3383,7 +3383,9 @@ namespace realclosure {
scoped_mpbqi num_i(bqim()), den_i(bqim());
polynomial_interval(v->num(), v->ext()->interval(), num_i);
polynomial_interval(v->den(), v->ext()->interval(), den_i);
div(num_i, den_i, inc_precision(prec, 2), v->interval());
if (!contains_zero(num_i) && !contains_zero(den_i)) {
div(num_i, den_i, inc_precision(prec, 2), v->interval());
}
}
}
@ -3883,7 +3885,7 @@ namespace realclosure {
}
}
int_buffer sc_cardinalities;
sc_cardinalities.resize(new_taqrs.size());
sc_cardinalities.resize(new_taqrs.size(), 0);
// Solve
// new_M_s * sc_cardinalities = new_taqrs
VERIFY(mm().solve(new_M_s, sc_cardinalities.c_ptr(), new_taqrs.c_ptr()));