mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Regressions reported by Guido

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-01 13:32:13 -08:00
parent 99e2794a6d
commit faf14012ba
3 changed files with 16 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/bool_rewriter.cpp
View file

@ -282,7 +282,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
get_num_internal_exprs(m_counts2, m_todo2, args[i]);
unsigned count1 = count_internal_nodes(m_counts1, m_todo1);
unsigned count2 = count_internal_nodes(m_counts2, m_todo2);
if (count1 > count2)
if (count1 > count2 + num_args)
st = BR_FAILED;
}
if (st != BR_FAILED)

16
src/ast/rewriter/hoist_rewriter.cpp
View file

@ -137,11 +137,17 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
m_subst.insert(p, m.mk_true());
fmls.push_back(p);
}
for (auto& p : m_eqs) {
if (m.is_value(p.first))
std::swap(p.first, p.second);
m_subst.insert(p.first, p.second);
fmls.push_back(m.mk_eq(p.first, p.second));
for (auto& [a, b] : m_eqs) {
if (m.is_value(a))
std::swap(a, b);
if (m.are_equal(a, b))
continue;
if (m.are_distinct(a, b)) {
result = m.mk_false();
return BR_DONE;
}
m_subst.insert(a, b);
fmls.push_back(m.mk_eq(a, b));
}
expr_ref ors(::mk_or(m, num_args, es), m);
m_subst(ors);

5
src/smt/mam.cpp
View file

@ -2413,7 +2413,10 @@ namespace {
m_n2 = static_cast<const check *>(m_pc)->m_enode;
SASSERT(m_n1 != 0);
SASSERT(m_n2 != 0);
if (m_n1->get_root() != m_n2->get_root())
// hack to handle dynamically generated patterns:
// if the pattern is ground and an if-expression, ignore equality check.
if (m_n1->get_root() != m_n2->get_root() && !m.is_ite(m_n2->get_expr()))
goto backtrack;
// we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log