mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

fix bug in qe-lite when substituting inside quantifiers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-19 05:20:45 -08:00
parent a94d3a21ee
commit 5bf20f9125
1 changed files with 10 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/muz_qe/qe_lite.cpp
View file

@ -342,17 +342,22 @@ class der2 {
void apply_substitution(quantifier * q, expr_ref & r) {
expr * e = q->get_expr();
unsigned num_args = to_app(e)->get_num_args();
unsigned num_args = 1;
expr* const* args = &e;
if ((q->is_forall() && m.is_or(e)) ||
(q->is_exists() && m.is_and(e))) {
num_args = to_app(e)->get_num_args();
args = to_app(e)->get_args();
}
bool_rewriter rw(m);
// get a new expression
m_new_args.reset();
for(unsigned i = 0; i < num_args; i++) {
int x = m_pos2var[i];
if (x != -1 && m_map[x] != 0)
continue; // this is a disequality/equality with definition (vanishes)
m_new_args.push_back(to_app(e)->get_arg(i));
if (x == -1 || m_map[x] == 0) {
m_new_args.push_back(args[i]);
}
}
expr_ref t(m);