fix #9657

src/ast/euf/ho_matcher.cpp

@@ -92,7 +92,7 @@ namespace euf {
         while (!m_backtrack.empty()) {
             auto& wi = *m_backtrack.back();
             bool st = consume_work(wi);
-            IF_VERBOSE(3, display(verbose_stream() << "ho_matcher::consume_work: " << wi.pat << " =?= " << wi.t << " -> " << (st?"true":"false") << "\n"););
+            TRACE(ho_matching, display(tout << "ho_matcher::consume_work: " << mk_bounded_pp(wi.pat, m) << " =?= " << mk_bounded_pp(wi.t, m) << " -> " << (st?"true":"false") << "\n"););
             if (st) {
                 if (m_goals.empty())                     
                     m_on_match(m_subst);                
@@ -653,7 +653,8 @@ namespace euf {
     void ho_matcher::add_binding(var* v, unsigned offset, expr* t) {
         SASSERT(v->get_idx() >= offset);
         m_subst.set(v->get_idx() - offset, t);
-        IF_VERBOSE(10, verbose_stream() << "ho_matcher::add_binding: v" << v->get_idx() - offset << " -> " << mk_pp(t, m) << "\n";);
+        SASSERT(v->get_sort() == t->get_sort());
+        TRACE(ho_matching, tout << "ho_matcher::add_binding: v" << v->get_idx() - offset << " -> " << mk_pp(t, m) << "\n";);
         m_trail.push(undo_set(m_subst, v->get_idx() - offset));
     }
 
@@ -821,13 +822,13 @@ namespace euf {
                 m_subst.set(idx, s.get(i));
         }
 
-        IF_VERBOSE(10, verbose_stream() << "refine " << mk_pp(p, m) << "\n" << s << "\n");
+        TRACE(ho_matching, tout << "refine " << mk_pp(p, m) << "\n" << s << "\n");
 
         unsigned num_bound = 0, level = 0;
         for (auto [v, pat] : m_pat2abs[fo_pat]) {
             var_subst sub(m, true);
             auto pat_refined = sub(pat, s);
-            IF_VERBOSE(10, verbose_stream() << mk_pp(pat, m) << " -> " << pat_refined << "\n");
+            TRACE(ho_matching, tout << mk_pp(pat, m) << " -> " << pat_refined << "\n");
             m_goals.push(level, num_bound, pat_refined, m_subst.get(v));
         }
 

src/ast/euf/ho_matcher.h

@@ -25,6 +25,7 @@ Author:
 #include "ast/for_each_expr.h"
 #include "ast/reg_decl_plugins.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 #include "ast/rewriter/array_rewriter.h"
 #include "ast/rewriter/var_subst.h"
 
@@ -88,13 +89,15 @@ namespace euf {
         }
 
         match_goal(unsigned level, unsigned offset, expr_ref const& pat, expr_ref const& t) noexcept : 
-            base_offset(offset), pat(pat), t(t),  level(level)  {}
+            base_offset(offset), pat(pat), t(t),  level(level)  {
+            SASSERT(pat->get_sort() == t->get_sort());
+        }
 
         unsigned term_offset() const { return base_offset + delta_offset; }
         unsigned pat_offset() const { return base_offset + delta_offset; }
 
         std::ostream& display(std::ostream& out) const {
-            return out << "[" << level << ":" << base_offset + delta_offset << "] " << pat << " ~ " << t << "\n";
+            return out << "[" << level << ":" << base_offset + delta_offset << "] " << mk_bounded_pp(pat, pat.m()) << " ~ " << mk_bounded_pp(t, t.m()) << "\n";
         }
     };
 

src/ast/rewriter/rewriter_def.h

@@ -668,7 +668,7 @@ template<typename Config>
 void rewriter_tpl<Config>::display_bindings(std::ostream& out) {
     for (unsigned i = 0; i < m_bindings.size(); ++i) {
         if (m_bindings[i])
-            out << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << ";\n";
+            out << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << " : " << mk_pp(m_bindings[i]->get_sort(), m()) << ";\n";
     }
 }
 

src/smt/smt_quantifier.cpp

@@ -677,12 +677,15 @@ namespace smt {
             // The HO quantifier has extra vars at higher indices; drop them.
             // Binding is indexed by var index: binding[i] = value for var i.
             // First substitute any remaining vars, then keep only original vars.
+            TRACE(ho_matching, tout << "num bound variables " << q->get_num_decls() << " for " << mk_bounded_pp(q, m)
+                                    << "\n"
+                                    << binding << "\n";);
             if (binding.size() > q->get_num_decls()) {
                 var_subst sub(m);
                 bool change = true;
                 while (change) {
                     change = false;
-                    for (unsigned i = 0; i < binding.size(); ++i) {
+                    for (unsigned i = 1; i < binding.size(); ++i) {
                         if (!binding.get(i)) continue;
                         auto r = sub(binding.get(i), binding);
                         change |= r != binding.get(i);
@@ -691,12 +694,15 @@ namespace smt {
                 }
                 binding.shrink(q->get_num_decls());
             }
+            if (binding.size() < q->get_num_decls())
+                return;
+
+            binding.reverse();
 
             // Create enodes for the refined bindings and add instance
             ptr_buffer<enode> new_bindings;
             unsigned max_gen = st.m_max_generation;
-            for (unsigned i = 0; i < q->get_num_decls(); ++i) {
-                expr* e = binding.get(i);
+            for (expr* e : binding) {
                 if (!e)
                     return; // incomplete binding
                 if (!m_context->e_internalized(e)) {
@@ -711,7 +717,7 @@ namespace smt {
             TRACE(ho_matching,
                 tout << "ho_match refined for " << mk_pp(q, m) << "\n";
                 for (unsigned i = 0; i < new_bindings.size(); ++i)
-                    tout << "  binding[" << i << "] = " << mk_pp(new_bindings[i]->get_expr(), m) << "\n";);
+                    tout << "  binding[" << i << "] = " << mk_bounded_pp(new_bindings[i]->get_expr(), m) << "\n";);
 
             vector<std::tuple<enode*, enode*>> used_enodes;
             m_context->add_instance(q, nullptr, new_bindings.size(), new_bindings.data(),