fix #4266

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/ast.cpp

@@ -1824,6 +1824,9 @@ ast * ast_manager::register_node_core(ast * n) {
 
     n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
 
+    if (n->m_id == 28 && is_lambda(n)) {
+        // SASSERT(false);
+    }
     // track_id(*this, n, 254);
 
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);

src/ast/rewriter/rewriter_def.h

@@ -19,6 +19,7 @@ Notes:
 #include "ast/rewriter/rewriter.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_ll_pp.h"
+#include "ast/ast_pp.h"
 
 template<typename Config>
 template<bool ProofGen>
@@ -80,7 +81,6 @@ bool rewriter_tpl<Config>::process_const(app * t0) {
  retry:
     SASSERT(t->get_num_args() == 0);
     br_status st = m_cfg.reduce_app(t->get_decl(), 0, nullptr, m_r, m_pr);
-    SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
     TRACE("reduce_app",
           tout << "t0:" << mk_bounded_pp(t0, m()) << "\n";
           if (t != t0) tout << "t: " << mk_bounded_pp(t, m()) << "\n";
@@ -89,6 +89,11 @@ bool rewriter_tpl<Config>::process_const(app * t0) {
           tout << "\n";
           if (m_pr) tout << mk_bounded_pp(m_pr, m()) << "\n";
           );
+    CTRACE("reduce_app", 
+           st != BR_FAILED && m().get_sort(m_r) != m().get_sort(t),
+           tout << mk_pp(m().get_sort(t), m()) << ": " << mk_pp(t, m()) << "\n";
+           tout << m_r->get_id() << " " << mk_pp(m().get_sort(m_r), m()) << ": " << m_r << "\n";);
+    SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
     switch (st) {
     case BR_FAILED:
         if (!retried) {

src/model/func_interp.cpp

@@ -357,14 +357,14 @@ expr * func_interp::get_interp_core() const {
     return r;
 }
 
-expr* func_interp::get_array_interp_core(func_decl * f) const {
+expr_ref func_interp::get_array_interp_core_(func_decl * f) const {
     if (m_else == nullptr) 
-        return nullptr;
+        return expr_ref(m_manager);
     ptr_vector<sort> domain;
     for (sort* s : *f) {
         domain.push_back(s);
     }
-    expr* r;
+    expr_ref r(m_manager);
 
     bool ground = is_ground(m_else);
     for (func_entry * curr : m_entries) {
@@ -376,13 +376,17 @@ expr* func_interp::get_array_interp_core(func_decl * f) const {
     if (!ground) {
         r = get_interp();
         if (!r) return r;
-        sort_ref_vector vars(m_manager);
+        sort_ref_vector sorts(m_manager);
+        expr_ref_vector vars(m_manager);
         svector<symbol> var_names;
+        var_subst sub(m_manager, false);
         for (unsigned i = 0; i < m_arity; ++i) {
             var_names.push_back(symbol(i));
-            vars.push_back(domain.get(m_arity - i - 1));
+            sorts.push_back(domain.get(i));
+            vars.push_back(m_manager.mk_var(m_arity - i - 1, sorts.back()));
         }
-        r = m_manager.mk_lambda(vars.size(), vars.c_ptr(), var_names.c_ptr(), r);        
+        r = sub(r, vars);
+        r = m_manager.mk_lambda(sorts.size(), sorts.c_ptr(), var_names.c_ptr(), r);        
         return r;
     }
 
@@ -419,11 +423,11 @@ expr * func_interp::get_interp() const {
     return r;
 }
 
-expr * func_interp::get_array_interp(func_decl * f) const {
+expr_ref func_interp::get_array_interp_(func_decl * f) const {
     if (m_array_interp != nullptr)
-        return m_array_interp;
-    expr* r = get_array_interp_core(f);
-    if (r != nullptr) {
+        return expr_ref(m_array_interp, m_manager);
+    expr_ref r = get_array_interp_core_(f);
+    if (r) {
         const_cast<func_interp*>(this)->m_array_interp = r;
         m_manager.inc_ref(m_array_interp);
     }

src/model/func_interp.h

@@ -79,7 +79,7 @@ class func_interp {
 
     expr * get_interp_core() const;
 
-    expr * get_array_interp_core(func_decl * f) const;
+    expr_ref get_array_interp_core_(func_decl * f) const;
 
 public:
     func_interp(ast_manager & m, unsigned arity);
@@ -116,7 +116,7 @@ public:
 
     expr * get_interp() const;
 
-    expr * get_array_interp(func_decl* f) const;
+    expr_ref get_array_interp_(func_decl* f) const;
 
     func_interp * translate(ast_translation & translator) const;
 

src/model/model.cpp

@@ -448,7 +448,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
                 // only expand auxiliary definitions that occur once.
                 if (can_inline_def(ts, f)) {
                     fi = get_func_interp(f);
-                    new_t = fi->get_array_interp(f);
+                    new_t = fi->get_array_interp_(f);
                     TRACE("model", tout << "array interpretation:" << new_t << "\n";);
                 }
             }

src/model/model_evaluator.cpp

@@ -253,7 +253,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 return BR_DONE;
             }
             func_interp * fi = m_model.get_func_interp(g);
-            if (fi && (result = fi->get_array_interp(g))) {
+            if (fi && (result = fi->get_array_interp_(g))) {
                 model_evaluator ev(m_model, m_params);
                 result = ev(result);
                 m_pinned.push_back(result);