mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

elim_bounds bugfix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-22 17:48:02 -08:00
parent ea876715e3
commit 72d2cd546e
2 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/simplifier/elim_bounds.cpp
View file

@ -110,6 +110,7 @@ void elim_bounds::operator()(quantifier * q, expr_ref & r) {
return; return;
} }
expr * n = q->get_expr(); expr * n = q->get_expr();
unsigned num_vars = q->get_num_decls();
ptr_buffer<expr> atoms; ptr_buffer<expr> atoms;
if (m_manager.is_or(n)) if (m_manager.is_or(n))
atoms.append(to_app(n)->get_num_args(), to_app(n)->get_args()); atoms.append(to_app(n)->get_num_args(), to_app(n)->get_args());
@ -138,11 +139,11 @@ void elim_bounds::operator()(quantifier * q, expr_ref & r) {
var * lower = 0; var * lower = 0;
var * upper = 0; var * upper = 0;
if (is_bound(a, lower, upper)) { if (is_bound(a, lower, upper)) {
if (lower != 0 && !m_used_vars.contains(lower->get_idx())) { if (lower != 0 && !m_used_vars.contains(lower->get_idx()) && lower->get_idx() < num_vars) {
ADD_CANDIDATE(lower); ADD_CANDIDATE(lower);
m_lowers.insert(lower); m_lowers.insert(lower);
} }
if (upper != 0 && !m_used_vars.contains(upper->get_idx())) { if (upper != 0 && !m_used_vars.contains(upper->get_idx()) && upper->get_idx() < num_vars) {
ADD_CANDIDATE(upper); ADD_CANDIDATE(upper);
m_uppers.insert(upper); m_uppers.insert(upper);
} }
@ -176,6 +177,7 @@ void elim_bounds::operator()(quantifier * q, expr_ref & r) {
switch (atoms.size()) { switch (atoms.size()) {
case 0: case 0:
r = m_manager.mk_false(); r = m_manager.mk_false();
TRACE("elim_bounds", tout << mk_pp(q, m_manager) << "\n" << mk_pp(r, m_manager) << "\n";);
return; return;
case 1: case 1:
new_body = atoms[0]; new_body = atoms[0];

3
src/tactic/smtlogics/quant_tactics.cpp
View file

@ -102,7 +102,8 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
or_else(try_for(mk_smt_tactic(), 100), or_else(try_for(mk_smt_tactic(), 100),
try_for(qe::mk_sat_tactic(m), 1000), try_for(qe::mk_sat_tactic(m), 1000),
try_for(mk_smt_tactic(), 1000), try_for(mk_smt_tactic(), 1000),
and_then(mk_qe_tactic(m), mk_smt_tactic()))); and_then(mk_qe_tactic(m), mk_smt_tactic())
));
st->updt_params(p); st->updt_params(p);
return st; return st;