fix bug in euf-completion relating to missed normalization

Z3Prover · Nov 14, 2022 · ce6cfea · ce6cfea
1 parent 3fa81d6
commit ce6cfea
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 6 deletions.
diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -75,25 +75,24 @@ void elim_unconstrained::eliminate() {
             return;
 
         if (n.m_parents.empty()) {
-            --n.m_refcount;
+            n.m_refcount = 0;
             continue;
         }
         expr* e = get_parent(v);
         for (expr* p : n.m_parents)
             IF_VERBOSE(11, verbose_stream() << "parent " << mk_bounded_pp(p, m) << "\n");
         if (!e || !is_app(e) || !is_ground(e)) {
-            --n.m_refcount;
+            n.m_refcount = 0;
             continue;
         }
         app* t = to_app(e);
         m_args.reset();
         for (expr* arg : *to_app(t))
             m_args.push_back(get_node(arg).m_term);
         if (!m_inverter(t->get_decl(), m_args.size(), m_args.data(), r, side_cond)) {
-            --n.m_refcount;
+            n.m_refcount = 0;
             continue;
         }
-        --n.m_refcount;
         SASSERT(r->get_sort() == t->get_sort());
         m_stats.m_num_eliminated++;
         n.m_refcount = 0;

diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
@@ -98,7 +98,7 @@ namespace euf {
             if (g != f) {
                 m_fmls.update(i, dependent_expr(m, g, dep));
                 m_stats.m_num_rewrites++;
-                IF_VERBOSE(10, verbose_stream() << mk_bounded_pp(f, m, 3) << " -> " << mk_bounded_pp(g, m, 3) << "\n");
+                IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(f, m, 3) << " -> " << mk_bounded_pp(g, m, 3) << "\n");
             }
             CTRACE("euf_completion", g != f, tout << mk_bounded_pp(f, m) << " -> " << mk_bounded_pp(g, m) << "\n");
         }
@@ -174,7 +174,7 @@ namespace euf {
         bool change = false;
         for (expr* arg : *to_app(f)) {
             m_eargs.push_back(get_canonical(arg, d));
-            change = arg != m_eargs.back();
+            change |= arg != m_eargs.back();
         }
 
         if (!change)