mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

fix #3858

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-09 09:22:02 -07:00
parent 2673807a7f
commit 8cf5a7525b
2 changed files with 6 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/muz/transforms/dl_mk_elim_term_ite.cpp
View file

@ -98,17 +98,15 @@ namespace datalog {
expr_ref_vector new_conjs(m);
expr_ref tmp(m);
for (unsigned i = utsz; i < tsz; ++i)
for (unsigned i = 0; i < tsz; ++i)
new_conjs.push_back(r.get_tail(i));
flatten_and(new_conjs);
expr_ref fml1(m), fml2(m), body(m), head(m);
// blast ite
body = m.mk_and(new_conjs.size(), new_conjs.c_ptr());
body = mk_and(new_conjs);
if (!has_term_ite(body)) {
TRACE("dl_term_ite", tout << "No term-ite, skipping a rule\n";);
new_rules.add_rule(&r);
return false;
}

10
src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
View file

@ -582,13 +582,11 @@ namespace datalog {
bool mk_interp_tail_simplifier::transform_rules(const rule_set & orig, rule_set & tgt) {
bool modified = false;
rule_manager& rm = m_context.get_rule_manager();
rule_set::iterator rit = orig.begin();
rule_set::iterator rend = orig.end();
for (; rit!=rend; ++rit) {
for (rule * r : orig) {
rule_ref new_rule(rm);
if (transform_rule(*rit, new_rule)) {
rm.mk_rule_rewrite_proof(**rit, *new_rule.get());
bool is_modified = *rit != new_rule;
if (transform_rule(r, new_rule)) {
rm.mk_rule_rewrite_proof(*r, *new_rule.get());
bool is_modified = r != new_rule;
modified |= is_modified;
tgt.add_rule(new_rule);
}