mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
complement regular expressions when used in negated membership constraints #1224
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
974eaab01c
commit
0ebb917268
|
@ -1726,8 +1726,6 @@ ast * ast_manager::register_node_core(ast * n) {
|
|||
}
|
||||
|
||||
n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
|
||||
static unsigned s_counter = 0;
|
||||
|
||||
|
||||
TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
|
||||
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
|
||||
|
|
|
@ -130,13 +130,13 @@ private:
|
|||
else {
|
||||
//true case
|
||||
curr_bv.push_back(true);
|
||||
ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m);
|
||||
ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m);
|
||||
generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_pos);
|
||||
curr_bv.pop_back();
|
||||
|
||||
//false case
|
||||
curr_bv.push_back(false);
|
||||
ref_t neg(m_ba.mk_not(constraints[i]), m);
|
||||
ref_t neg(m_ba.mk_not(constraints[i]), m);
|
||||
ref_t new_pred_neg(m_ba.mk_and(curr_pred, neg), m);
|
||||
generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_neg);
|
||||
curr_bv.pop_back();
|
||||
|
|
Loading…
Reference in a new issue