Merge branch 'master' of https://github.com/z3prover/z3 into derive

src/api/CMakeLists.txt

@@ -66,7 +66,7 @@ z3_add_component(api
     z3_replayer.cpp
     ${full_path_generated_files}
   COMPONENT_DEPENDENCIES
-    opt
+    z3_opt
     euf
     portfolio
     realclosure

src/api/c++/z3++.h

@@ -4925,7 +4925,7 @@ namespace z3 {
         
         void check_context(rcf_num const& other) const {
             if (m_ctx != other.m_ctx) {
-                throw exception("rcf_num objects from different contexts");
+                Z3_THROW(exception("rcf_num objects from different contexts"));
             }
         }
         
@@ -5105,9 +5105,9 @@ namespace z3 {
     */
     inline std::vector<rcf_num> rcf_roots(context& c, std::vector<rcf_num> const& coeffs) {
         if (coeffs.empty()) {
-            throw exception("polynomial coefficients cannot be empty");
+            Z3_THROW(exception("polynomial coefficients cannot be empty"));
         }
-        
+
         unsigned n = static_cast<unsigned>(coeffs.size());
         std::vector<Z3_rcf_num> a(n);
         std::vector<Z3_rcf_num> roots(n);

src/api/java/CMakeLists.txt

@@ -48,17 +48,18 @@ target_include_directories(z3java PRIVATE
   "${PROJECT_BINARY_DIR}/src/api"
   ${JNI_INCLUDE_DIRS}
 )
-# Add header padding for macOS to allow install_name_tool to modify the dylib
+# On macOS, set rpath so libz3java.dylib can find libz3.dylib in the same directory,
+# and add header padding to allow install_name_tool to modify the dylib.
 if (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
+  set_target_properties(z3java PROPERTIES
+    MACOSX_RPATH TRUE
+    INSTALL_RPATH "@loader_path"
+    BUILD_RPATH "@loader_path"
+  )
   target_link_options(z3java PRIVATE "-Wl,-headerpad_max_install_names")
 endif()
 # FIXME: Should this library have SONAME and VERSION set?
 
-# On macOS, add headerpad for install_name_tool compatibility
-if(CMAKE_SYSTEM_NAME STREQUAL "Darwin")
-  target_link_options(z3java PRIVATE "-Wl,-headerpad_max_install_names")
-endif()
-
 # This prevents CMake from automatically defining ``z3java_EXPORTS``
 set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "")
 

src/api/python/z3/z3.py

@@ -7396,8 +7396,8 @@ class Statistics:
         >>> s.check()
         sat
         >>> st = s.statistics()
-        >>> len(st)
-        7
+        >>> len(st) > 0
+        True
         """
         return int(Z3_stats_size(self.ctx.ref(), self.stats))
 
@@ -7410,8 +7410,8 @@ class Statistics:
         >>> s.check()
         sat
         >>> st = s.statistics()
-        >>> len(st)
-        7
+        >>> len(st) > 0
+        True
         >>> st[0]
         ('nlsat propagations', 2)
         >>> st[1]

src/ast/ast.cpp

@@ -242,21 +242,14 @@ func_decl_info::func_decl_info(family_id family_id, decl_kind k, unsigned num_pa
     m_injective(false),
     m_idempotent(false),
     m_skolem(false),
-    m_lambda(false),
     m_polymorphic(false) {
 }
 
 bool func_decl_info::operator==(func_decl_info const & info) const {
-    return decl_info::operator==(info) &&
-        m_left_assoc == info.m_left_assoc &&
-        m_right_assoc == info.m_right_assoc &&
-        m_flat_associative == info.m_flat_associative &&
-        m_commutative == info.m_commutative &&
-        m_chainable == info.m_chainable &&
-        m_pairwise == info.m_pairwise &&
-        m_injective == info.m_injective &&
-        m_skolem == info.m_skolem &&
-        m_lambda == info.m_lambda;
+    return decl_info::operator==(info) && m_left_assoc == info.m_left_assoc && m_right_assoc == info.m_right_assoc &&
+           m_flat_associative == info.m_flat_associative && m_commutative == info.m_commutative &&
+           m_chainable == info.m_chainable && m_pairwise == info.m_pairwise && m_injective == info.m_injective &&
+           m_skolem == info.m_skolem;
 }
 
 std::ostream & operator<<(std::ostream & out, func_decl_info const & info) {
@@ -270,7 +263,6 @@ std::ostream & operator<<(std::ostream & out, func_decl_info const & info) {
     if (info.is_injective()) out << " :injective ";
     if (info.is_idempotent()) out << " :idempotent ";
     if (info.is_skolem()) out << " :skolem ";
-    if (info.is_lambda()) out << " :lambda ";
     if (info.is_polymorphic()) out << " :polymorphic ";
     return out;
 }
@@ -1625,19 +1617,6 @@ bool ast_manager::are_distinct(expr* a, expr* b) const {
     return false;
 }
 
-void ast_manager::add_lambda_def(func_decl* f, quantifier* q) {
-    TRACE(model, tout << "add lambda def " << mk_pp(q, *this) << "\n");
-    m_lambda_defs.insert(f, q);
-    f->get_info()->set_lambda(true);
-    inc_ref(q);
-}
-
-quantifier* ast_manager::is_lambda_def(func_decl* f) {
-    if (f->get_info() && f->get_info()->is_lambda()) 
-        return m_lambda_defs[f];
-    return nullptr;
-}
-
 
 void ast_manager::register_plugin(family_id id, decl_plugin * plugin) {
     SASSERT(m_plugins.get(id, 0) == 0);
@@ -1832,10 +1811,6 @@ void ast_manager::delete_node(ast * n) {
                 m_poly_roots.erase(f);
             if (f->m_info != nullptr) {
                 func_decl_info * info = f->get_info();
-                if (info->is_lambda()) {
-                    push_dec_ref(m_lambda_defs[f]);
-                    m_lambda_defs.remove(f);
-                }
                 info->del_eh(*this);
                 dealloc(info);
             }

src/ast/ast.h

@@ -404,7 +404,6 @@ struct func_decl_info : public decl_info {
     bool m_injective:1;
     bool m_idempotent:1;
     bool m_skolem:1;
-    bool m_lambda:1;
     bool m_polymorphic:1;
 
     func_decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind, unsigned num_parameters = 0, parameter const * parameters = nullptr);
@@ -419,7 +418,6 @@ struct func_decl_info : public decl_info {
     bool is_injective() const { return m_injective; }
     bool is_idempotent() const { return m_idempotent; }
     bool is_skolem() const { return m_skolem; }
-    bool is_lambda() const { return m_lambda; }
     bool is_polymorphic() const { return m_polymorphic; }
 
     void set_associative(bool flag = true) { m_left_assoc = flag; m_right_assoc = flag; }
@@ -432,7 +430,6 @@ struct func_decl_info : public decl_info {
     void set_injective(bool flag = true) { m_injective = flag; }
     void set_idempotent(bool flag = true) { m_idempotent = flag; }
     void set_skolem(bool flag = true) { m_skolem = flag; }
-    void set_lambda(bool flag = true) { m_lambda = flag; }
     void set_polymorphic(bool flag = true) { m_polymorphic = flag; }
 
     bool operator==(func_decl_info const & info) const;
@@ -661,7 +658,6 @@ public:
     bool is_pairwise() const { return get_info() != nullptr && get_info()->is_pairwise(); }
     bool is_injective() const { return get_info() != nullptr && get_info()->is_injective(); }
     bool is_skolem() const { return get_info() != nullptr && get_info()->is_skolem(); }
-    bool is_lambda() const { return get_info() != nullptr && get_info()->is_lambda(); }
     bool is_idempotent() const { return get_info() != nullptr && get_info()->is_idempotent(); }
     bool is_polymorphic() const { return get_info() != nullptr && get_info()->is_polymorphic(); }
     unsigned get_arity() const { return m_arity; }
@@ -1513,7 +1509,6 @@ protected:
     proof_gen_mode            m_proof_mode;
     bool                      m_int_real_coercions; // If true, use hack that automatically introduces to_int/to_real when needed.
     ast_table                 m_ast_table;
-    obj_map<func_decl, quantifier*> m_lambda_defs;
     id_gen                    m_expr_id_gen;
     id_gen                    m_decl_id_gen;
     sort *                    m_bool_sort;
@@ -1643,15 +1638,7 @@ public:
     bool are_distinct(expr * a, expr * b) const;
 
     bool contains(ast * a) const { return m_ast_table.contains(a); }
-    
-    bool is_lambda_q(quantifier* q) const { return q->get_qid() == m_lambda_def; }
-    void add_lambda_def(func_decl* f, quantifier* q);
-    quantifier* is_lambda_def(func_decl* f);
-    quantifier* is_lambda_def(expr* e) { return is_app(e) ? is_lambda_def(to_app(e)->get_decl()) : nullptr; }
-    obj_map<func_decl, quantifier*> const& lambda_defs() const { return m_lambda_defs; }
-
-    symbol const& lambda_def_qid() const { return m_lambda_def; }
-
+   
     unsigned get_num_asts() const { return m_ast_table.size(); }
 
     void debug_ref_count() { m_debug_ref_count = true; }

src/ast/ast_ll_pp.cpp

@@ -21,6 +21,7 @@ Revision History:
 #include "ast/for_each_ast.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/datatype_decl_plugin.h"
+#include "ast/ast_smt2_pp.h"
 
 // #define AST_LL_PP_SHOW_FAMILY_NAME
 
@@ -44,7 +45,7 @@ class ll_printer {
     }
 
     void display_name(func_decl * decl) {
-        m_out << decl->get_name();
+        m_out << ensure_quote(decl->get_name());
     }
 
     bool process_numeral(expr * n) {

src/ast/ast_smt_pp.cpp

@@ -507,6 +507,7 @@ class smt_printer {
         case forall_k: m_out << "forall "; break;
         case exists_k: m_out << "exists "; break;
         case lambda_k: m_out << "lambda "; break;
+        case choice_k: m_out << "choice "; break;
         }
         m_out << "(";
         for (unsigned i = 0; i < q->get_num_decls(); ++i) {

src/ast/ast_translation.cpp

@@ -181,20 +181,12 @@ void ast_translation::mk_func_decl(func_decl * f, frame & fr) {
         new_fi.set_injective(fi->is_injective());
         new_fi.set_skolem(fi->is_skolem()); 
         new_fi.set_idempotent(fi->is_idempotent());
-        new_fi.set_lambda(fi->is_lambda());
 
         new_f = m_to_manager.mk_func_decl(f->get_name(),
                                           f->get_arity(),
                                           new_domain,
                                           new_range,
                                           new_fi);
-
-        if (new_fi.is_lambda()) {
-            quantifier* q = from().is_lambda_def(f);
-            ast_translation tr(from(), to());
-            quantifier* new_q = tr(q);
-            to().add_lambda_def(new_f, new_q);
-        }
     }
     TRACE(ast_translation, 
           tout << f->get_name() << " "; if (fi) tout << *fi; tout << "\n";

src/ast/euf/euf_mam.cpp

@@ -1951,14 +1951,12 @@ namespace euf {
 
         enode * get_next_f_app(func_decl * lbl, unsigned num_expected_args, enode * first, enode * curr) {
             curr = curr->get_next();
-            enode *matching_cgr = nullptr, *min_gen_match = nullptr;
             while (curr != first) {
-                get_f_app(lbl, num_expected_args, curr, matching_cgr, min_gen_match);
+                if (curr->get_decl() == lbl && curr->num_args() == num_expected_args && curr->is_cgr())
+                    return curr;
                 curr = curr->get_next();
             }
-            if (matching_cgr)
-                update_max_generation(min_gen_match, first);
-            return matching_cgr;
+            return nullptr;
         }
 
         /**

src/ast/euf/ho_matcher.cpp

@@ -240,7 +240,6 @@ namespace euf {
             else
                 break;
         }
-        r = unfold_lambda_def(r); 
         return r;    
     }
 
@@ -254,34 +253,6 @@ namespace euf {
         }
     }
 
-    // We assume that m_rewriter should produce
-    // something amounting to weak-head normal form WHNF
-
-    // Unfold a lambda-def application f(args) to the corresponding lambda expression.
-    // For a func_decl f with arity n and lambda-def quantifier (lambda (x1..xk) body),
-    // f(a1,...,an) is unfolded to (lambda (x1..xk) body[params := a1..an]).
-    // For a constant f (arity 0) that is a lambda-def, returns the lambda directly.
-    expr_ref ho_matcher::unfold_lambda_def(expr* e) const {
-        if (!is_app(e))
-            return expr_ref(e, m);
-        app* a = to_app(e);
-        func_decl* f = a->get_decl();
-        quantifier* lam = m.is_lambda_def(f);
-        if (!lam)
-            return expr_ref(e, m);
-        
-        unsigned arity = f->get_arity();
-        SASSERT(is_lambda(lam));
-        
-        if (arity == 0) 
-            // Constant lambda-def: just return the lambda expression
-            return expr_ref(lam, m);        
-
-        var_subst subst(m, false);
-        expr_ref r = subst(lam, to_app(e)->get_num_args(), to_app(e)->get_args());
-        return r;        
-    }
-
     void ho_matcher::reduce(match_goal& wi) {
         wi.pat = whnf_star(wi.pat, wi.pat_offset());
         wi.t = whnf_star(wi.t, wi.term_offset());
@@ -684,7 +655,7 @@ namespace euf {
         }
         auto is_ho = any_of(subterms::all(expr_ref(p, m)), [&](expr* t) { 
             return m_unitary.is_flex(0, t) || 
-                   m.is_lambda_def(t) || 
+                   // m.is_lambda_def(t) || 
                    is_lambda(t); 
         });
         if (!is_ho)
@@ -703,7 +674,8 @@ namespace euf {
                 todo.pop_back();
                 continue;
             }
-            if ((m_unitary.is_flex(0, t) && lvl > 1) || m.is_lambda_def(t) || is_lambda(t)) {
+            if ((m_unitary.is_flex(0, t) && lvl > 1) || // m.is_lambda_def(t) || 
+                is_lambda(t)) {
                 if (!contains_pat2abs)
                     m_pat2abs.insert_if_not_there(p, svector<std::pair<unsigned, expr*>>()).push_back({ nb, t });
                 auto v = m.mk_var(nb++, t->get_sort());

src/ast/euf/ho_matcher.h

@@ -355,8 +355,6 @@ namespace euf {
 
         void reduce(match_goal& wi);
 
-        expr_ref unfold_lambda_def(expr* e) const;
-
         trail_stack& trail() { return m_trail; }
 
         std::ostream& display(std::ostream& out) const;

src/ast/normal_forms/defined_names.cpp

@@ -121,9 +121,6 @@ app * defined_names::impl::gen_name(expr * e, sort_ref_buffer & var_sorts, buffe
     sort * range = e->get_sort();
     func_decl * new_skolem_decl = m.mk_fresh_func_decl(m_z3name, symbol::null, domain.size(), domain.data(), range);
     app * n = m.mk_app(new_skolem_decl, new_args.size(), new_args.data());
-    if (is_lambda(e)) {
-        m.add_lambda_def(new_skolem_decl, to_quantifier(e));
-    }
     return n;
 }
 

src/ast/normal_forms/pull_quant.cpp

@@ -188,7 +188,7 @@ struct pull_quant::imp {
 				 var_names.data(),
 				 nested_q->get_expr(),
 				 std::min(q->get_weight(), nested_q->get_weight()),
-				 m.is_lambda_q(q) ? symbol("pulled-lambda") : q->get_qid());
+				 q->get_qid());
         }
 
         void pull_quant1(quantifier * q, expr * new_expr, expr_ref & result) {

src/ast/pattern/pattern_inference.cpp

@@ -554,7 +554,7 @@ bool pattern_inference_cfg::is_forbidden(app * n) const {
     // Remark: skolem constants should not be used in patterns, since they do not
     // occur outside of the quantifier. That is, Z3 will never match this kind of
     // pattern.
-    if (m_params.m_pi_avoid_skolems && decl->is_skolem() && !m.is_lambda_def(decl)) {
+    if (m_params.m_pi_avoid_skolems && decl->is_skolem()) {
         CTRACE(pattern_inference_skolem, decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m) << "\n";);
         return true;
     }

src/ast/rewriter/CMakeLists.txt

@@ -40,6 +40,7 @@ z3_add_component(rewriter
     seq_axioms.cpp
     seq_eq_solver.cpp
     seq_derive.cpp
+    seq_subset.cpp
     seq_rewriter.cpp
     seq_skolem.cpp
     th_rewriter.cpp

src/ast/rewriter/seq_rewriter.cpp

@@ -4014,51 +4014,7 @@ bool seq_rewriter::are_complements(expr* r1, expr* r2) const {
  * basic subset checker.
  */
 bool seq_rewriter::is_subset(expr* r1, expr* r2) const {
-    // return false;
-    expr* ra1 = nullptr, *ra2 = nullptr, *ra3 = nullptr;
-    expr* rb1 = nullptr, *rb2 = nullptr, *rb3 = nullptr;
-    unsigned la, ua, lb, ub;
-    if (re().is_complement(r1, ra1) && 
-        re().is_complement(r2, rb1)) {
-        return is_subset(rb1, ra1);
-    }
-    auto is_concat = [&](expr* r, expr*& a, expr*& b, expr*& c) {
-        return re().is_concat(r, a, b) && re().is_concat(b, b, c);
-    };
-    while (true) {
-        if (r1 == r2)
-            return true;
-        if (re().is_full_seq(r2))
-            return true;
-        if (re().is_dot_plus(r2) && re().get_info(r1).nullable == l_false)
-            return true;
-        if (is_concat(r1, ra1, ra2, ra3) &&
-            is_concat(r2, rb1, rb2, rb3) && ra1 == rb1 && ra2 == rb2) {
-            r1 = ra3;
-            r2 = rb3;
-            continue;
-        }
-        if (re().is_concat(r1, ra1, ra2) && 
-            re().is_concat(r2, rb1, rb2) && re().is_full_seq(rb1)) {
-            r1 = ra2;
-            continue;
-        }
-        // r1=ra3{la,ua}ra2, r2=rb3{lb,ub}rb2, ra3=rb3, lb<=la, ua<=ub
-        if (re().is_concat(r1, ra1, ra2) && re().is_loop(ra1, ra3, la, ua) &&
-            re().is_concat(r2, rb1, rb2) && re().is_loop(rb1, rb3, lb, ub) &&
-            ra3 == rb3 && lb <= la && ua <= ub) {
-            r1 = ra2;
-            r2 = rb2;
-            continue;
-        }
-        // ra1=ra3{la,ua}, r2=rb3{lb,ub}, ra3=rb3, lb<=la, ua<=ub
-        if (re().is_loop(r1, ra3, la, ua) &&
-            re().is_loop(r2, rb3, lb, ub) &&
-            ra3 == rb3 && lb <= la && ua <= ub) {
-            return true;
-        }
-        return false;
-    }
+    return m_subset.is_subset(r1, r2);
 }
 
 br_status seq_rewriter::mk_re_union0(expr* a, expr* b, expr_ref& result) {
@@ -5628,4 +5584,3 @@ bool seq_rewriter::get_bounds(expr* e, unsigned& low, unsigned& high) {
     }
     return low <= high;
 }
-

src/ast/rewriter/seq_rewriter.h

@@ -24,6 +24,7 @@ Notes:
 #include "ast/arith_decl_plugin.h"
 #include "ast/rewriter/rewriter_types.h"
 #include "ast/rewriter/bool_rewriter.h"
+#include "ast/rewriter/seq_subset.h"
 #include "util/params.h"
 #include "util/lbool.h"
 #include "util/sign.h"
@@ -131,6 +132,7 @@ class seq_rewriter {
     friend class seq::derive;
 
     seq_util       m_util;
+    seq_subset     m_subset;
     arith_util     m_autil;
     bool_rewriter  m_br;
     seq::derive    m_derive;
@@ -334,7 +336,7 @@ class seq_rewriter {
 
 public:
     seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
-        m_util(m), m_autil(m), m_br(m, p), m_derive(m, *this), // m_re2aut(m), 
+        m_util(m), m_subset(m_util.re), m_autil(m), m_br(m, p), m_derive(m, *this),
         m_op_cache(m), m_es(m), 
         m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
     }
@@ -418,4 +420,3 @@ public:
     */
     lbool some_string_in_re(expr* r, zstring& s);
 };
-

src/ast/rewriter/seq_subset.cpp

@@ -0,0 +1,146 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    seq_subset.cpp
+
+Abstract:
+
+    Heuristic regular-expression subset checks used by seq_rewriter.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2026-6-8
+
+--*/
+
+#include "ast/rewriter/seq_subset.h"
+
+bool seq_subset::is_subset_rec(expr* a, expr* b, unsigned depth) const {
+    while (true) {
+        
+        if (a == b)
+            return true;
+        if (m_re.is_empty(a))
+            return true;
+        if (m_re.is_full_seq(b))
+            return true;
+        if (m_re.is_epsilon(a) && m_re.get_info(b).nullable == l_true)
+            return true;
+
+        if (depth >= m_max_depth)
+            return false;        
+
+        expr* a1 = nullptr, * a2 = nullptr, * b1 = nullptr, * b2 = nullptr;
+        unsigned la, ua, lb, ub;
+
+        // a ⊆ .+ iff a is non-nullable
+        if (m_re.is_dot_plus(b) && m_re.get_info(a).nullable == l_false)
+            return true;
+
+        // a ⊆ a*
+        if (m_re.is_star(b, b1) && is_subset_rec(a, b1, depth))
+            return true;
+
+        // e ⊆ a*
+        if (m_re.is_epsilon(a) && m_re.is_star(b, b1))
+            return true;
+
+        // R ⊆ R*
+        if (m_re.is_star(b, b1) && is_subset_rec(a, b1, depth + 1))
+            return true;
+
+        // R1* ⊆ R2* if R1 ⊆ R2
+        if (m_re.is_star(a, a1) && m_re.is_star(b, b1) && is_subset_rec(a1, b1, depth + 1))
+            return true;
+
+        // R1+ ⊆ R2+ if R1 ⊆ R2
+        if (m_re.is_plus(a, a1) && m_re.is_plus(b, b1) && is_subset_rec(a1, b1, depth))
+            return true;
+
+        // R ⊆ R+
+        if (m_re.is_plus(b, b1) && is_subset_rec(a, b1, depth))
+            return true;
+
+        // R+ ⊆ R*
+        if (m_re.is_plus(a, a1) && m_re.is_star(b, b1) && is_subset_rec(a1, b1, depth + 1))
+            return true;
+
+        // range containment
+        if (m_re.is_range(a, la, ua) && m_re.is_range(b, lb, ub) && lb <= la && ua <= ub)
+            return true;
+
+        // to_re(s) ⊆ range
+        if (m_re.is_to_re(a, a1) && m_re.is_range(b, lb, ub) && is_app(a1)) {
+            func_decl* f = to_app(a1)->get_decl();
+            if (f->get_decl_kind() == OP_STRING_CONST && f->get_num_parameters() == 1) {
+                zstring const& s = f->get_parameter(0).get_zstring();
+                if (s.length() == 1 && lb <= s[0] && s[0] <= ub)
+                    return true;
+            }
+        }
+
+        // a ⊆ b1 ∪ b2 if a ⊆ b1 or a ⊆ b2
+        if (m_re.is_union(b, b1, b2) && (is_subset_rec(a, b1, depth + 1) || is_subset_rec(a, b2, depth + 1)))
+            return true;
+
+        // a1 ∪ a2 ⊆ b if a1 ⊆ b and a2 ⊆ b
+        if (m_re.is_union(a, a1, a2) && is_subset_rec(a1, b, depth + 1) && is_subset_rec(a2, b, depth + 1))
+            return true;
+
+        // a1 ∩ a2 ⊆ b if a1 ⊆ b or a2 ⊆ b
+        if (m_re.is_intersection(a, a1, a2) && (is_subset_rec(a1, b, depth + 1) || is_subset_rec(a2, b, depth + 1)))
+            return true;
+
+        // a ⊆ b1 ∩ b2 if a ⊆ b1 and a ⊆ b2
+        if (m_re.is_intersection(b, b1, b2) && is_subset_rec(a, b1, depth + 1) && is_subset_rec(a, b2, depth + 1))
+            return true;
+
+        // R{la,ua} ⊆  R'{lb,ub} if  R ⊆ R', lb<=la, ua<=ub
+        if (m_re.is_loop(a, a1, la, ua) &&
+            m_re.is_loop(b, b1, lb, ub) &&
+            lb <= la && ua <= ub && is_subset_rec(a1, b1, depth + 1)) {
+            return true;
+        }
+
+        // a1 \ a2 ⊆ b if a1 ⊆ b
+        if (m_re.is_diff(a, a1, a2) && is_subset_rec(a1, b, depth + 1))
+            return true;
+
+        // R ⊆ Σ*·R' if R ⊆ R'
+        if (m_re.is_concat(b, b1, b2) && m_re.is_full_seq(b1) && is_subset_rec(a, b2, depth))
+            return true;
+
+        // R ⊆ R'·Σ* if R ⊆ R'
+        if (m_re.is_concat(b, b1, b2) && m_re.is_full_seq(b2) && is_subset_rec(a, b1, depth))
+            return true;
+
+        // star absorption: R·R* ⊆ R*, R*·R ⊆ R*
+        bool const is_concat_star = m_re.is_concat(a, a1, a2) && m_re.is_star(b, b1);
+        if (is_concat_star &&
+            is_subset_rec(a1, b1, depth + 1) && is_subset_rec(a2, b, depth + 1))
+            return true;
+        if (is_concat_star &&
+            is_subset_rec(a2, b1, depth + 1) && is_subset_rec(a1, b, depth + 1))
+            return true;
+
+        // concat monotonicity:
+        // tail-recursive on second arguments (without increasing depth bound).
+        if (m_re.is_concat(a, a1, a2) && m_re.is_concat(b, b1, b2) && is_subset_rec(a1, b1, depth + 1)) {
+            a = a2;
+            b = b2;
+            continue;
+        }
+
+        // complement: ~a ⊆ ~b if b ⊆ a
+        if (m_re.is_complement(a, a1) && m_re.is_complement(b, b1))
+            return is_subset_rec(b1, a1, depth + 1);
+
+        return false;
+    }
+}
+
+bool seq_subset::is_subset(expr* a, expr* b) const {
+    return is_subset_rec(a, b, 0);
+}

src/ast/rewriter/seq_subset.h

@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    seq_subset.h
+
+Abstract:
+
+    Heuristic regular-expression subset checks used by seq_rewriter.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2026-6-8
+
+--*/
+#pragma once
+
+#include "ast/seq_decl_plugin.h"
+
+class seq_subset {
+    seq_util::rex& m_re;
+    static constexpr unsigned m_max_depth = 3;
+
+    bool is_subset_rec(expr* a, expr* b, unsigned depth) const;
+
+public:
+    explicit seq_subset(seq_util::rex& re) : m_re(re) {}
+    bool is_subset(expr* a, expr* b) const;
+};

src/ast/simplifiers/dependent_expr_state.cpp

@@ -88,22 +88,6 @@ void dependent_expr_state::freeze_recfun() {
     m_num_recfun = sz;
 }
 
-/**
-* Freeze all functions used in lambda defined declarations
-*/
-void dependent_expr_state::freeze_lambda() {
-    auto& m = m_frozen_trail.get_manager();
-    unsigned sz = m.lambda_defs().size();
-    if (m_num_lambdas >= sz)
-        return;
-
-    ast_mark visited;
-    for (auto const& [f, body] : m.lambda_defs()) 
-        freeze_terms(body, false, visited);
-    m_trail.push(value_trail(m_num_lambdas));
-    m_num_lambdas = sz;
-}
-
 
 /**
 * The current qhead is to be updated to qtail. 
@@ -122,8 +106,7 @@ void dependent_expr_state::freeze_suffix() {
     if (m_suffix_frozen)
         return;
     m_suffix_frozen = true;
-    freeze_recfun();
-    freeze_lambda();
+    freeze_recfun();    
     auto& m = m_frozen_trail.get_manager();
     ast_mark visited;
     ptr_vector<expr> es;

src/ast/simplifiers/dependent_expr_state.h

@@ -51,7 +51,6 @@ class dependent_expr_state {
     func_decl_ref_vector m_frozen_trail;
     void freeze_prefix();
     void freeze_recfun();
-    void freeze_lambda();
     void freeze_terms(expr* term, bool only_as_array, ast_mark& visited);
     void freeze(func_decl* f);
     struct thaw : public trail {

src/ast/sls/sls_seq_plugin.cpp

@@ -172,9 +172,7 @@ namespace sls {
                     return false;
                 if (r > sx.length() && update(x, sx + zstring(random_char())))
                     return false;
-                // This case seems to imply unsat
-                verbose_stream() << "The input might be unsat\n"; // example to trigger: (assert (and (>= (str.len X) 2) (= (str.substr X 0 1) "")))
-                VERIFY(false);
+                // Both updates failed. Treat as unsatisfied and let outer search continue.
                 return false;
             }
 
@@ -198,8 +196,16 @@ namespace sls {
                 return false;
             }
             if (seq.str.is_last_index(e, x, y) && seq.is_string(x->get_sort())) {
-                // TODO
-                NOT_IMPLEMENTED_YET();
+                auto sx = strval0(x);
+                auto sy = strval0(y);
+                rational val_e;
+                if (!a.is_numeral(ctx.get_value(e), val_e))
+                    return false;
+                rational actual(sx.last_indexof(sy));
+                if (val_e == actual)
+                    continue;
+                update(e, actual);
+                return false;
             }
             if (seq.str.is_stoi(e, x) && seq.is_string(x->get_sort())) {
                 auto sx = strval0(x);
@@ -753,7 +759,7 @@ namespace sls {
             for (unsigned j = 1; j <= val_other.length() - i; ++j) {
                 zstring sub = val_other.extract(i, j);
                 if (set.contains(sub))
-                    break;
+                    continue;
                 set.insert(sub);
             }
         }
@@ -906,7 +912,7 @@ namespace sls {
                         m_string_updates.reset();
                         u[i][j] = d[i - 1][j];
                     }
-                    if (d[i][j - 1] < u[i][j] && b.can_add(i - 1)) {
+                    if (d[i][j - 1] < u[i][j] && b.can_add(j - 1)) {
                         m_string_updates.reset();
                         u[i][j] = d[i][j - 1];
                     }

src/cmd_context/tactic_cmds.cpp

@@ -232,7 +232,9 @@ public:
                 }
                 ctx.validate_check_sat_result(r);
             }
-            t.collect_statistics(result->m_stats);
+            statistics stats;
+            t.collect_statistics(stats);
+            result->add_statistics(stats);
         }
 
         if (ctx.produce_unsat_cores()) {

src/math/lp/dioph_eq.cpp

@@ -709,8 +709,8 @@ namespace lp {
             while (column.size() > 1) {
                 auto& c = column.back();
                 SASSERT(c.var() != last_row_index);
-                m_l_matrix.pivot_row_to_row_given_cell(last_row_index, c, j);
                 m_changed_rows.insert(c.var());
+                m_l_matrix.pivot_row_to_row_given_cell(last_row_index, c, j);
             }
         }
 

src/math/lp/lp_core_solver_base_def.h

@@ -277,13 +277,11 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) {
         m_A.m_rows[c.var()][c.offset()].offset() = pivot_col_cell_index;
     }
     while (column.size() > 1) {
-        auto & c = column.back();
+        auto& c = column.back();
         SASSERT(c.var() != piv_row_index);
-        if(! m_A.pivot_row_to_row_given_cell(piv_row_index, c, j)) {
-            return false;
-        }
-        if (m_touched_rows!= nullptr)
+        if (m_touched_rows != nullptr)
             m_touched_rows->insert(c.var());
+        m_A.pivot_row_to_row_given_cell(piv_row_index, c, j);
     }
 
     if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs)

src/math/lp/static_matrix.cpp

@@ -51,8 +51,8 @@ namespace lp {
     template void static_matrix<mpq, numeric_pair<mpq> >::set(unsigned int, unsigned int, mpq const&);
 
 
-    template bool static_matrix<mpq, mpq>::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int);
-    template bool static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int);
+    template void static_matrix<mpq, mpq>::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int);
+    template void static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int);
     template void static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell_with_sign(unsigned int, column_cell&, unsigned int, int);
     template void static_matrix<mpq, mpq>::pivot_row_to_row_given_cell_with_sign(unsigned int, row_cell<empty_struct>&, unsigned int, int);
     template void static_matrix<mpq, numeric_pair<mpq> >::add_rows(mpq const&, unsigned int, unsigned int);

src/math/lp/static_matrix.h

@@ -293,7 +293,7 @@ public:
 
 
 // pivot row i to row ii
-    bool pivot_row_to_row_given_cell(unsigned i, column_cell& c, unsigned j);
+    void pivot_row_to_row_given_cell(unsigned i, column_cell& c, unsigned j);
     void pivot_row_to_row_given_cell_with_sign(unsigned piv_row_index, column_cell& c, unsigned j, int j_sign);
     void transpose_rows(unsigned i, unsigned ii) {
         auto t = m_rows[i];

src/math/lp/static_matrix_def.h

@@ -48,7 +48,7 @@ namespace lp {
     }
 
 
-    template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_given_cell(unsigned i, 
+    template <typename T, typename X> void static_matrix<T, X>::pivot_row_to_row_given_cell(unsigned i, 
                                                                                             column_cell & c, unsigned pivot_col) {
         unsigned ii = c.var();
         SASSERT(i < row_count() && ii < column_count() && i != ii);
@@ -82,7 +82,7 @@ namespace lp {
             if (is_zero(rowii[k].coeff()))
                 remove_element(rowii, rowii[k]);
         }
-        return !rowii.empty();
+        SASSERT(!rowii.empty());
     }
 
     

src/model/model_core.cpp

@@ -130,19 +130,3 @@ void model_core::unregister_decl(func_decl * d) {
     }
 }
 
-void model_core::add_lambda_defs() {
-    unsigned sz = get_num_decls();
-    for (unsigned i = sz; i-- > 0; ) {
-        func_decl* f = get_decl(i);
-        quantifier* q = m.is_lambda_def(f);
-        if (!q)
-            continue;
-        if (f->get_arity() > 0) {
-            func_interp* fi = alloc(func_interp, m, f->get_arity());
-            fi->set_else(q);
-            register_decl(f, fi);
-        }
-        else
-            register_decl(f, q);
-    }
-}

src/muz/spacer/spacer_iuc_solver.cpp

@@ -185,7 +185,7 @@ namespace spacer {
         return m_base_defs.is_proxy (a, def);
     }
 
-    void iuc_solver::collect_statistics (statistics &st) const {
+    void iuc_solver::collect_statistics_core (statistics &st) const {
         m_solver.collect_statistics (st);
         st.update ("time.iuc_solver.get_iuc", m_iuc_sw.get_seconds());
         st.update ("time.iuc_solver.get_iuc.hyp_reduce1", m_hyp_reduce1_sw.get_seconds());

src/muz/spacer/spacer_iuc_solver.h

@@ -147,7 +147,7 @@ public:
 
     /* check_sat_result interface */
 
-    void collect_statistics(statistics &st) const override ;
+    void collect_statistics_core(statistics &st) const override ;
     virtual void reset_statistics();
 
     void get_unsat_core(expr_ref_vector &r) override;

src/muz/spacer/spacer_qe_project.cpp

@@ -1148,6 +1148,7 @@ class arith_project_util {
                         expr_ref_vector const &lits) {
         app_ref_vector new_vars(m);
         expr_ref_vector result(lits);
+        model::scoped_model_completion _smc(mdl, true);
         for (unsigned i = 0; i < vars.size(); ++i) {
             app *v = vars.get(i);
             m_var = alloc(contains_app, m, v);
@@ -1183,6 +1184,12 @@ class arith_project_util {
                     expr_map &map) {
         app_ref_vector new_vars(m);
 
+        // Variables to be projected may not be assigned in the model
+        // (e.g. grounded auxiliary variables that are don't-cares). Enable
+        // model completion so their evaluation yields concrete numerals,
+        // matching the behavior of the native MBP arith projector.
+        model::scoped_model_completion _smc(mdl, true);
+
         // factor out mod terms by introducing new variables
         TRACE(qe, tout << "before factoring out mod terms:" << "\n";
               tout << mk_pp(fml, m) << "\n"; tout << "mdl:\n";

src/opt/CMakeLists.txt

@@ -1,4 +1,4 @@
-z3_add_component(opt
+z3_add_component(z3_opt
   SOURCES
     maxcore.cpp
     maxlex.cpp

src/opt/opt_context.cpp

@@ -1745,7 +1745,7 @@ namespace opt {
         m_pareto1 = p != nullptr;
     }
 
-    void context::collect_statistics(statistics& stats) const {
+    void context::collect_statistics_core(statistics& stats) const {
         if (m_solver) 
             m_solver->collect_statistics(stats);
         if (m_simplify) 

src/opt/opt_context.h

@@ -235,7 +235,7 @@ namespace opt {
         void get_model_core(model_ref& _m) override;
         void get_box_model(model_ref& _m, unsigned index) override;
         void fix_model(model_ref& _m) override;
-        void collect_statistics(statistics& stats) const override;
+        void collect_statistics_core(statistics& stats) const override;
         proof* get_proof_core() override { return nullptr; }
         void get_labels(svector<symbol> & r) override;
         void get_unsat_core(expr_ref_vector & r) override;

src/opt/opt_sls_solver.h

@@ -66,7 +66,7 @@ namespace opt {
         virtual void collect_param_descrs(param_descrs & r) {
             m_solver->collect_param_descrs(r);
         }
-        virtual void collect_statistics(statistics & st) const {
+        virtual void collect_statistics_core(statistics & st) const {
             m_solver->collect_statistics(st);
             if (m_bvsls) m_bvsls->collect_statistics(st);
             if (m_pbsls) m_pbsls->collect_statistics(st);

src/opt/opt_solver.cpp

@@ -76,7 +76,7 @@ namespace opt {
         m_context.collect_param_descrs(r);
     }
     
-    void opt_solver::collect_statistics(statistics & st) const {        
+    void opt_solver::collect_statistics_core(statistics & st) const {        
         m_context.collect_statistics(st);
     }
     

src/opt/opt_solver.h

@@ -89,7 +89,7 @@ namespace opt {
         solver* translate(ast_manager& m, params_ref const& p) override;
         void updt_params(params_ref const& p) override;
         void collect_param_descrs(param_descrs & r) override;
-        void collect_statistics(statistics & st) const override;
+        void collect_statistics_core(statistics & st) const override;
         void assert_expr_core(expr * t) override;
         void push_core() override;
         void pop_core(unsigned n) override;

src/qe/mbp/mbp_dt_tg.cpp

@@ -163,6 +163,23 @@ struct mbp_dt_tg::impl {
             if (is_app(term) &&
                 m_dt_util.is_accessor(to_app(term)->get_decl()) &&
                 has_var(to_app(term)->get_arg(0))) {
+                // Only apply rm_accessor if the model confirms the argument
+                // has the constructor that this accessor belongs to.
+                // Otherwise we introduce a contradictory is-cons literal.
+                func_decl *acc_cons =
+                    m_dt_util.get_accessor_constructor(to_app(term)->get_decl());
+                func_decl *rec = m_dt_util.get_constructor_recognizer(acc_cons);
+                expr_ref is_rec(m.mk_app(rec, to_app(term)->get_arg(0)), m);
+                if (!m_mdl.is_true(is_rec)) {
+                    // The accessor's argument does not have the expected constructor in the model.
+                    // Add a guard literal and skip rm_accessor so we don't force a contradictory
+                    // constructor constraint on the argument.
+                    expr_ref is(m.mk_not(is_rec), m);
+                    m_tg.add_lit(is);
+                    mark_seen(term);
+                    progress = true;
+                    continue;
+                }
                 mark_seen(term);
                 progress = true;
                 rm_accessor(term);

src/sat/sat_solver/inc_sat_solver.cpp

@@ -387,7 +387,7 @@ public:
         if (p1.euf() && !get_euf()) 
             ensure_euf();        
     }
-    void collect_statistics(statistics & st) const override {
+    void collect_statistics_core(statistics & st) const override {
         if (m_preprocess) m_preprocess->collect_statistics(st);
         m_solver.collect_statistics(st);
     }

src/sat/sat_solver/sat_smt_solver.cpp

@@ -334,7 +334,7 @@ public:
             ensure_euf();
     }
     
-    void collect_statistics(statistics & st) const override {
+    void collect_statistics_core(statistics & st) const override {
         m_solver.collect_statistics(st);
     }
     

src/shell/CMakeLists.txt

@@ -8,7 +8,7 @@ set (shell_object_files "")
 
 # We are only using these dependencies to enforce a build
 # order. We don't use this list for actual linking.
-set(shell_deps api extra_cmds opt sat)
+set(shell_deps api extra_cmds z3_opt sat)
 z3_expand_dependencies(shell_expanded_deps ${shell_deps})
 get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS)
 foreach (component ${Z3_LIBZ3_COMPONENTS_LIST})

src/smt/fingerprints.cpp

@@ -20,10 +20,9 @@ Revision History:
 
 namespace smt {
 
-    fingerprint::fingerprint(region & r, void * d, unsigned d_h, expr* def, unsigned n, enode * const * args):
+    fingerprint::fingerprint(region & r, void * d, unsigned d_h, unsigned n, enode * const * args):
         m_data(d), 
         m_data_hash(d_h),
-        m_def(def),
         m_num_args(n), 
         m_args(nullptr) {
         m_args = new (r) enode*[n];
@@ -62,7 +61,7 @@ namespace smt {
     }
 
     
-    fingerprint * fingerprint_set::insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def) {
+    fingerprint * fingerprint_set::insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args) {
         
         struct arg_data {
             unsigned data_hash;
@@ -93,9 +92,8 @@ namespace smt {
             return nullptr;
         }
         TRACE(fingerprint_bug, tout << "inserting @" << m_scopes.size() << " " << *d;);
-        fingerprint * f = new (m_region) fingerprint(m_region, data, data_hash, def, num_args, d->m_args);
+        fingerprint * f = new (m_region) fingerprint(m_region, data, data_hash, num_args, d->m_args);
         m_fingerprints.push_back(f);
-        m_defs.push_back(def);
         m_set.insert(f);
         return f;
     }
@@ -106,15 +104,12 @@ namespace smt {
             return true;
         for (unsigned i = 0; i < num_args; ++i)
             d->m_args[i] = d->m_args[i]->get_root();
-        if (m_set.contains(d))
-            return true;
-        return false;
+        return m_set.contains(d);
     }
     
     void fingerprint_set::reset() {
         m_set.reset();
         m_fingerprints.reset();
-        m_defs.reset();
     }
         
     void fingerprint_set::push_scope() {
@@ -134,7 +129,6 @@ namespace smt {
                 m_set.erase(m_fingerprints[i]);
         }
         m_fingerprints.shrink(old_size);
-        m_defs.shrink(old_size);
         m_scopes.shrink(new_lvl);
         TRACE(fingerprint_bug, tout << "pop @" << m_scopes.size() << "\n";);
     }

src/smt/fingerprints.h

@@ -27,16 +27,14 @@ namespace smt {
     protected:
         void*         m_data = nullptr;
         unsigned      m_data_hash = 0;
-        expr*         m_def = nullptr;
         unsigned      m_num_args = 0;
         enode**       m_args = nullptr;
 
         friend class fingerprint_set;
         fingerprint() = default;
     public:
-        fingerprint(region & r, void * d, unsigned d_hash, expr* def, unsigned n, enode * const * args);
+        fingerprint(region & r, void * d, unsigned d_hash, unsigned n, enode * const * args);
         void * get_data() const { return m_data; }
-        expr * get_def() const { return m_def; }
         unsigned get_data_hash() const { return m_data_hash; }
         unsigned get_num_args() const { return m_num_args;  }
         enode * const * get_args() const { return m_args; }
@@ -59,7 +57,6 @@ namespace smt {
         region &                 m_region;
         set                      m_set;
         ptr_vector<fingerprint>  m_fingerprints;
-        expr_ref_vector          m_defs;
         unsigned_vector          m_scopes;
         ptr_vector<enode>        m_tmp;
         fingerprint              m_dummy;
@@ -67,8 +64,8 @@ namespace smt {
         fingerprint * mk_dummy(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
 
     public:
-        fingerprint_set(ast_manager& m, region & r): m_region(r), m_defs(m) {}
-        fingerprint * insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def);
+        fingerprint_set(ast_manager& m, region & r): m_region(r) {}
+        fingerprint * insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
         unsigned size() const { return m_fingerprints.size(); }
         bool contains(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
         void reset();

src/smt/mam.cpp

@@ -1881,8 +1881,10 @@ namespace {
             m_pool.recycle(v);
         }
 
-        void update_max_generation(enode * n, enode * prev) {
-            m_max_generation = std::max(m_max_generation, n->get_generation());
+        void update_max_generation(enode * n, enode * prev, enode * min_gen_match=nullptr) {
+            unsigned new_gen = min_gen_match ? min_gen_match->get_generation() : n->get_generation();
+
+            m_max_generation = std::max(m_max_generation, new_gen);
 
             if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality))
                 m_used_enodes.push_back(std::make_tuple(prev, n));
@@ -1910,15 +1912,18 @@ namespace {
             }
             while (curr != first);
             if (matching_cgr)
-                update_max_generation(min_gen_match, first);  
+                update_max_generation(matching_cgr, first, min_gen_match);  
             return matching_cgr;
         }
 
         enode * get_next_f_app(func_decl * lbl, unsigned num_expected_args, enode * first, enode * curr) {
             curr = curr->get_next();
             while (curr != first) {
-                if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args && curr->is_cgr())
+                if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args && curr->is_cgr()) {
+                    if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality))
+                        m_used_enodes.push_back(std::make_tuple(first, curr));
                     return curr;
+                }
                 curr = curr->get_next();
             }
             return nullptr;
@@ -3975,7 +3980,7 @@ namespace {
 #endif
             unsigned min_gen = 0, max_gen = 0;
             m_interpreter.get_min_max_top_generation(min_gen, max_gen);
-            m_context.add_instance(qa, pat, num_bindings, bindings, nullptr, max_generation, min_gen, max_gen, used_enodes);
+            m_context.add_instance(qa, pat, num_bindings, bindings, max_generation, min_gen, max_gen, used_enodes);
         }
 
         bool is_shared(enode * n) const override {

src/smt/qi_queue.cpp

@@ -331,9 +331,6 @@ namespace smt {
         unsigned gen = get_new_gen(q, generation, ent.m_cost);
         display_instance_profile(f, q, num_bindings, bindings, proof_id, gen);
         m_context.internalize_instance(lemma, pr1, gen);
-        if (f->get_def()) {
-            m_context.internalize(f->get_def(), true);
-        }
         TRACE_CODE({
             static unsigned num_useless = 0;
             if (m.is_or(lemma)) {

src/smt/smt_context.cpp

@@ -69,7 +69,6 @@ namespace smt {
         m_fingerprints(m, get_region()),
         m_b_internalized_stack(m),
         m_e_internalized_stack(m),
-        m_l_internalized_stack(m),
         m_final_check_idx(0),
         m_cg_table(m),
         m_conflict(null_b_justification),
@@ -81,7 +80,6 @@ namespace smt {
         m_unsat_core(m),
         m_mk_bool_var_trail(*this),
         m_mk_enode_trail(*this),
-        m_mk_lambda_trail(*this),
         m_lemma_visitor(m) {
 
         SASSERT(m_scope_lvl == 0);
@@ -1777,9 +1775,11 @@ namespace smt {
         return m_fingerprints.contains(q, q->get_id(), num_bindings, bindings);
     }
 
-    bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation,
+    bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, //expr* def, 
+        unsigned max_generation,
                                unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode *>> & used_enodes) {
-        return m_qmanager->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_top_generation, used_enodes);
+        return m_qmanager->add_instance(q, pat, num_bindings, bindings, 
+            max_generation, min_top_generation, max_top_generation, used_enodes);
     }
 
     void context::rescale_bool_var_activity() {
@@ -4662,7 +4662,7 @@ namespace smt {
             return false;
         }
         case 1: {
-            if (m_qmanager->is_shared(n) && !m.is_lambda_def(n->get_expr()) && !m_lambdas.contains(n)) 
+            if (m_qmanager->is_shared(n) && !m_lambdas.contains(n)) 
                 return true;
 
             // the variable is shared if the equivalence class of n

src/smt/smt_context.h

@@ -122,7 +122,6 @@ namespace smt {
         // enodes. Examples: boolean expression nested in an
         // uninterpreted function.
         expr_ref_vector             m_e_internalized_stack; // stack of the expressions already internalized as enodes.
-        quantifier_ref_vector       m_l_internalized_stack;
 
         ptr_vector<justification>   m_justifications;
 
@@ -620,8 +619,8 @@ namespace smt {
             return m_asserted_formulas.has_quantifiers();
         }
 
-        fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = nullptr) {
-            return m_fingerprints.insert(data, data_hash, num_args, args, def);
+        fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args) {
+            return m_fingerprints.insert(data, data_hash, num_args, args);
         }
 
         theory_id get_var_theory(bool_var v) const {
@@ -870,16 +869,6 @@ namespace smt {
         mk_enode_trail   m_mk_enode_trail;
         void undo_mk_enode();
 
-        friend class mk_lambda_trail;
-        class mk_lambda_trail : public trail {
-            context& ctx;
-        public:
-            mk_lambda_trail(context& ctx) :ctx(ctx) {}
-            void undo() override { ctx.undo_mk_lambda(); }
-        };
-        mk_lambda_trail   m_mk_lambda_trail;
-        void undo_mk_lambda();
-
 
         void apply_sort_cnstr(app * term, enode * e);
 
@@ -1113,8 +1102,8 @@ namespace smt {
 
         bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings);
 
-        bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation,
-                          unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
+        bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, 
+            unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
 
         void set_global_generation(unsigned generation) { m_generation = generation; }
 

src/smt/smt_enode.cpp

@@ -25,7 +25,7 @@ namespace smt {
     /**
        \brief Initialize an enode in the given memory position.
     */
-    enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, 
+    enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner, 
                         unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                         bool cgc_enabled, bool update_children_parent) {
         SASSERT(m.is_bool(owner) || !merge_tf);
@@ -42,7 +42,7 @@ namespace smt {
         n->m_interpreted      = false;
         n->m_suppress_args    = suppress_args;
         n->m_eq               = m.is_eq(owner);
-        n->m_commutative      = n->get_num_args() == 2 && owner->get_decl()->is_commutative();
+        n->m_commutative      = n->get_num_args() == 2 && n->get_decl()->is_commutative();
         n->m_bool             = m.is_bool(owner);
         n->m_merge_tf         = merge_tf;
         n->m_cgc_enabled      = cgc_enabled;
@@ -52,7 +52,7 @@ namespace smt {
         n->m_is_shared        = 2;
         unsigned num_args     = n->get_num_args();
         for (unsigned i = 0; i < num_args; ++i) {            
-            enode * arg  = app2enode[owner->get_arg(i)->get_id()];
+            enode * arg  = app2enode[to_app(owner)->get_arg(i)->get_id()];
             n->m_args[i] = arg;
             arg->get_root()->m_is_shared = 2;
             SASSERT(n->get_arg(i) == arg);
@@ -64,11 +64,11 @@ namespace smt {
         return n;
     }
 
-    enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, 
+    enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner, 
                            unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                            bool cgc_enabled, bool update_children_parent) {
         SASSERT(m.is_bool(owner) || !merge_tf);
-        unsigned sz           = get_enode_size(suppress_args ? 0 : owner->get_num_args());
+        unsigned sz           = get_enode_size(suppress_args || !::is_app(owner) ? 0 : to_app(owner)->get_num_args());
         void * mem            = r.allocate(sz);
         return init(m, mem, app2enode, owner, generation, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent);
     }

src/smt/smt_enode.h

@@ -132,7 +132,7 @@ namespace smt {
 
         friend class tmp_enode;
 
-        static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, 
+        static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner, 
                             unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                             bool cgc_enabled, bool update_children_parent);
     public:
@@ -141,7 +141,7 @@ namespace smt {
             return sizeof(enode) + num_args * sizeof(enode*);
         }
         
-        static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, 
+        static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner, 
                           unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                           bool cgc_enabled, bool update_children_parent);
 

src/smt/smt_internalizer.cpp

@@ -597,16 +597,9 @@ namespace smt {
         SASSERT(is_lambda(q));
         if (e_internalized(q)) 
             return;
-        app_ref lam_name(m.mk_fresh_const("lambda", q->get_sort()), m);
-        m.add_lambda_def(lam_name->get_decl(), q);
-        if (!e_internalized(lam_name)) 
-            internalize_uninterpreted(lam_name);
-        enode* lam_node = get_enode(lam_name);
-        push_trail(insert_obj_map<enode, quantifier*>(m_lambdas, lam_node));
-        m_lambdas.insert(lam_node, q);
-        m_app2enode.setx(q->get_id(), lam_node, nullptr);
-        m_l_internalized_stack.push_back(q);
-        m_trail_stack.push_ptr(&m_mk_lambda_trail);
+        mk_enode(q, true, /* do suppress args */
+                    false,    /* it is a term, so it should not be merged with true/false */
+                    true);
     }
 
     bool context::has_lambda() {
@@ -1008,7 +1001,7 @@ namespace smt {
             CTRACE(cached_generation, generation != m_generation,
                    tout << "cached_generation: #" << n->get_id() << " " << generation << " " << m_generation << "\n";);
         }
-        enode *e = enode::mk(m, get_region(), m_app2enode, to_app(n), generation, suppress_args, merge_tf, m_scope_lvl,
+        enode *e = enode::mk(m, get_region(), m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl,
                              cgc_enabled, true);
         TRACE(mk_enode_detail, tout << "e.get_num_args() = " << e->get_num_args() << "\n";);
         if (m.is_unique_value(n))
@@ -1063,14 +1056,6 @@ namespace smt {
         return e;
     }
 
-    void context::undo_mk_lambda() {
-        SASSERT(!m_l_internalized_stack.empty());
-        m_stats.m_num_del_enode++;
-        quantifier * n         = m_l_internalized_stack.back();
-        m_app2enode[n->get_id()] = nullptr;
-        m_l_internalized_stack.pop_back();
-    }
-
     void context::undo_mk_enode() {
         SASSERT(!m_e_internalized_stack.empty());
         m_stats.m_num_del_enode++;
@@ -1078,7 +1063,6 @@ namespace smt {
         TRACE(undo_mk_enode, tout << "undo_enode: #" << n->get_id() << "\n" << mk_pp(n, m) << "\n";);
         TRACE(mk_var_bug, tout << "undo_mk_enode: " << n->get_id() << "\n";);
         unsigned n_id         = n->get_id();
-        SASSERT(is_app(n));
         enode * e             = m_app2enode[n_id];
         m_app2enode[n_id]     = nullptr;
         if (e->is_cgr() && !e->is_true_eq() && e->is_cgc_enabled()) {

src/smt/smt_model_checker.cpp

@@ -203,7 +203,7 @@ namespace smt {
         unsigned num_decls = q->get_num_decls();
         // Remark: sks were created for the flat version of q.
         SASSERT(sks.size() >= num_decls);
-        expr_ref_vector bindings(m), defs(m);
+        expr_ref_vector bindings(m);
         expr_ref def(m);
         bindings.resize(num_decls);
         unsigned max_generation = 0;
@@ -249,6 +249,7 @@ namespace smt {
                 sk_value = get_type_compatible_term(sk_value);
             }
             func_decl * f = nullptr;
+            expr_ref sk_term(sk_value, m);
             if (autil.is_as_array(sk_value, f) && cex->get_func_interp(f) && cex->get_func_interp(f)->get_interp()) {
                 expr_ref body(cex->get_func_interp(f)->get_interp(), m);
                 if (contains_model_value(body))
@@ -257,30 +258,25 @@ namespace smt {
                 svector<symbol> names;
                 for (unsigned i = 0; i < f->get_arity(); ++i) 
                     names.push_back(symbol(i));
-                defined_names dn(m);
                 body = replace_value_from_ctx(body);
                 body = m.mk_lambda(sorts.size(), sorts.data(), names.data(), body);
-                // sk_value = m.mk_fresh_const(0, m.get_sort(sk_value));  // get rid of as-array
-                body = dn.mk_definition(body, to_app(sk_value));
-                defs.push_back(body);
+                sk_term = body;
             }
-            bindings.set(num_decls - i - 1, sk_value);
+            bindings.set(num_decls - i - 1, sk_term);
         }
 
-        TRACE(model_checker, tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: " << bindings << "\ndefs:\n" << defs << "\n";);
-        if (!defs.empty()) def = mk_and(defs);
+        TRACE(model_checker, tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: " << bindings << "\n");
         max_generation = std::max(m_qm->get_generation(q), max_generation);
-        add_instance(q, bindings, max_generation, def.get());
+        add_instance(q, bindings, max_generation);
         return true;
     }
 
-    void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation, expr* def) {
+    void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) {
         SASSERT(q->get_num_decls() == bindings.size());
         unsigned offset = m_pinned_exprs.size();
         m_pinned_exprs.append(bindings);
         m_pinned_exprs.push_back(q);
-        m_pinned_exprs.push_back(def);
-        m_new_instances.push_back(instance(q, offset, def, max_generation));
+        m_new_instances.push_back(instance(q, offset, max_generation));
     }
 
     void model_checker::operator()(expr *n) {
@@ -457,12 +453,6 @@ namespace smt {
 
         TRACE(model_checker, tout << "MODEL_CHECKER INVOKED\n";
         tout << "model:\n"; model_pp(tout, *m_curr_model););
-
-        for (quantifier* q : *m_qm)
-            if (m.is_lambda_q(q)) {
-                md->add_lambda_defs();
-                break;
-            }
 	
         md->compress();
 
@@ -518,8 +508,7 @@ namespace smt {
         for (quantifier * q : *m_qm) {
             if (!(m_qm->mbqi_enabled(q) &&
                   m_context->is_relevant(q) &&
-                  m_context->get_assignment(q) == l_true &&
-                  (!m_context->get_fparams().m_ematching || !m.is_lambda_q(q)))) {
+                  m_context->get_assignment(q) == l_true)) {
                 if (!m_qm->mbqi_enabled(q))
                     ++num_failures;
                 continue;
@@ -588,27 +577,11 @@ namespace smt {
                     bindings.push_back(m_context->get_enode(b));
                 }
 
-                if (inst.m_def) {
-                    unsigned n = 1;
-                    expr* const* args = &inst.m_def;
-                    if (m.is_and(inst.m_def)) {
-                        n = to_app(inst.m_def)->get_num_args();
-                        args = to_app(inst.m_def)->get_args();
-                    }
-                    for (unsigned i = 0; i < n; ++i) {
-                        proof* pr = nullptr;
-                        expr* arg = args[i];
-                        if (m.proofs_enabled()) 
-                            pr = m.mk_def_intro(arg);
-                        m_context->internalize_assertion(arg, pr, gen);
-                    }
-                }
-
                 TRACE(model_checker_bug_detail, tout << "instantiating... q:\n" << mk_pp(q, m) << "\n";
                       tout << "inconsistent: " << m_context->inconsistent() << "\n";
                       tout << "bindings:\n" << expr_ref_vector(m, num_decls, m_pinned_exprs.data() + offset) << "\n";
-                      tout << "def " << mk_pp(inst.m_def, m) << "\n";);
-                m_context->add_instance(q, nullptr, num_decls, bindings.data(), inst.m_def, gen, gen, gen, dummy);
+                          );
+                m_context->add_instance(q, nullptr, num_decls, bindings.data(), gen, gen, gen, dummy);
                 TRACE(model_checker_bug_detail, tout << "after instantiating, inconsistent: " << m_context->inconsistent() << "\n";);
             }
         }

src/smt/smt_model_checker.h

@@ -23,7 +23,6 @@ Revision History:
 #include "util/obj_hashtable.h"
 #include "ast/ast.h"
 #include "ast/array_decl_plugin.h"
-#include "ast/normal_forms/defined_names.h"
 #include "params/qi_params.h"
 #include "params/smt_params.h"
 
@@ -70,9 +69,8 @@ namespace smt {
         struct instance {
             quantifier * m_q;
             unsigned     m_generation;
-            expr *       m_def;
             unsigned     m_bindings_offset;
-            instance(quantifier * q, unsigned offset, expr* def, unsigned gen):m_q(q), m_generation(gen), m_def(def), m_bindings_offset(offset) {}
+            instance(quantifier * q, unsigned offset, unsigned gen):m_q(q), m_generation(gen), m_bindings_offset(offset) {}
         };
 
         svector<instance>                          m_new_instances;
@@ -86,7 +84,7 @@ namespace smt {
         struct is_model_value {};
         expr_mark m_visited;
         bool contains_model_value(expr * e);
-        void add_instance(quantifier * q, expr_ref_vector const & bindings, unsigned max_generation, expr * def);
+        void add_instance(quantifier * q, expr_ref_vector const & bindings, unsigned max_generation);
         bool is_safe_for_mbqi(quantifier * q) const;
 
     public:

src/smt/smt_model_finder.cpp

@@ -291,8 +291,8 @@ namespace smt {
             }
 
             void insert(expr* n, unsigned generation) {
-                SASSERT(is_ground(n));
-                get_root()->m_set->insert(n, generation);
+                if (is_ground(n))
+                    get_root()->m_set->insert(n, generation);
             }
 
             void display(std::ostream& out, ast_manager& m) const {
@@ -1690,7 +1690,7 @@ namespace smt {
             typedef ptr_vector<cond_macro>::const_iterator macro_iterator;
 
             static quantifier_ref mk_flat(ast_manager& m, quantifier* q) {
-                if (has_quantifiers(q->get_expr()) && !m.is_lambda_q(q)) {
+                if (has_quantifiers(q->get_expr())) {
                     proof_ref pr(m);
                     expr_ref  new_q(m);
                     pull_quant pull(m);
@@ -2279,7 +2279,6 @@ namespace smt {
             void operator()(quantifier_info* d) {
                 m_info = d;
                 quantifier* q = d->get_flat_q();
-                if (m.is_lambda_q(q)) return;
                 expr* e = q->get_expr();
                 reset_cache();
                 if (!m.inc()) return;

src/smt/smt_model_generator.cpp

@@ -428,6 +428,8 @@ namespace smt {
             if (!m_context->is_relevant(t))
                 continue;
             enode * n         = m_context->get_enode(t);
+            if (!n->is_app())
+                continue;
             unsigned num_args = n->get_num_args();
             func_decl * f     = n->get_decl();
             if (num_args == 0 && include_func_interp(f)) {

src/smt/smt_quantifier.cpp

@@ -292,7 +292,6 @@ namespace smt {
         bool add_instance(quantifier * q, app * pat,
                           unsigned num_bindings,
                           enode * const * bindings,
-                          expr* def,
                           unsigned max_generation,
                           unsigned min_top_generation,
                           unsigned max_top_generation,
@@ -310,7 +309,7 @@ namespace smt {
             max_generation = std::max(max_generation, get_generation(q));
             
             get_stat(q)->update_max_generation(max_generation);
-            fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def);
+            fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings);
             if (f) {
                 if (is_trace_enabled(TraceTag::causality)) {
                     log_causality(f,pat,used_enodes);
@@ -484,17 +483,17 @@ namespace smt {
     bool quantifier_manager::add_instance(quantifier * q, app * pat,
                                           unsigned num_bindings,
                                           enode * const * bindings,
-                                          expr* def,
                                           unsigned max_generation,
                                           unsigned min_top_generation,
                                           unsigned max_top_generation,
                                           vector<std::tuple<enode *, enode *>> & used_enodes) {
-        return m_imp->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_top_generation, used_enodes);
+        return m_imp->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_top_generation, used_enodes);
     }
 
-    bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation) {
+    bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation) {
         vector<std::tuple<enode *, enode *>> tmp;
-        return add_instance(q, nullptr, num_bindings, bindings, def, generation, generation, generation, tmp);
+        return add_instance(q, nullptr, num_bindings, bindings,
+            generation, generation, generation, tmp);
     }
 
     void quantifier_manager::init_search_eh() {
@@ -721,7 +720,7 @@ namespace smt {
 
             vector<std::tuple<enode*, enode*>> used_enodes;
             m_context->add_instance(q, nullptr, new_bindings.size(), new_bindings.data(),
-                                    nullptr, max_gen, st.m_min_top_generation, st.m_max_top_generation, used_enodes);
+                                    max_gen, st.m_min_top_generation, st.m_max_top_generation, used_enodes);
         }
 
         bool try_ho_refine(quantifier* qa, app* pat, unsigned num_bindings, enode* const* bindings,

src/smt/smt_quantifier.h

@@ -60,12 +60,11 @@ namespace smt {
         bool add_instance(quantifier * q, app * pat,
                           unsigned num_bindings,
                           enode * const * bindings,
-                          expr* def,
                           unsigned max_generation,
                           unsigned min_top_generation,
                           unsigned max_top_generation,
                           vector<std::tuple<enode *, enode *>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
-        bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation = 0);
+        bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0);
 
         void init_search_eh();
         void assign_eh(quantifier * q);

src/smt/smt_quick_checker.cpp

@@ -236,7 +236,7 @@ namespace smt {
                     TRACE(quick_checker_sizes, tout << "found new candidate\n"; 
                           for (unsigned i = 0; i < m_num_bindings; ++i) tout << "#" << m_bindings[i]->get_owner_id() << " "; tout << "\n";);
                     unsigned max_generation = get_max_generation(m_num_bindings, m_bindings.data());
-                    if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.data(), nullptr, 
+                    if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.data(), 
                                                max_generation,
                                                0,  // min_top_generation is only available for instances created by the MAM
                                                0,  // max_top_generation is only available for instances created by the MAM

src/smt/smt_solver.cpp

@@ -142,7 +142,7 @@ namespace {
             insert_ctrl_c(r);
         }
 
-        void collect_statistics(statistics & st) const override {
+        void collect_statistics_core(statistics & st) const override {
             m_context.collect_statistics(st);
         }
 

src/smt/theory_array.cpp

@@ -68,12 +68,12 @@ namespace smt {
         m_var_data.push_back(alloc(var_data));
         var_data * d  = m_var_data[r];
         TRACE(array, tout << mk_bounded_pp(n->get_expr(), m) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) <<
-              ", is_store: " << is_store(n) << ", is_lambda: " << is_lambda(n) << "\n";);
+              ", is_store: " << is_store(n) << ", is_lambda: " << is_lambda(n->get_expr()) << "\n";);
         d->m_is_array  = is_array_sort(n);
         if (d->m_is_array) 
             register_sort(n->get_expr()->get_sort());
         d->m_is_select = is_select(n);        
-        if (is_store(n) || is_lambda(n))
+        if (is_store(n) || is_lambda(n->get_expr()))
             d->m_stores.push_back(n);
         ctx.attach_th_var(n, this, r);
         if (laziness() <= 1 && is_store(n))
@@ -95,7 +95,7 @@ namespace smt {
 
         if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
             for (enode* store : d->m_parent_stores) {
-                SASSERT(is_store(store) || is_lambda(store));
+                SASSERT(is_store(store) || is_lambda(store->get_expr()));
                 if (!m_params.m_array_cg || store->is_cgr()) {
                     instantiate_axiom2b(s, store);
                 }
@@ -106,7 +106,7 @@ namespace smt {
     void theory_array::add_parent_store(theory_var v, enode * s) {
         if (m_params.m_array_cg && !s->is_cgr())
             return;
-        SASSERT(is_store(s) || is_lambda(s));
+        SASSERT(is_store(s) || is_lambda(s->get_expr()));
         v                = find(v);
         var_data * d     = m_var_data[v];
         d->m_parent_stores.push_back(s);
@@ -177,7 +177,7 @@ namespace smt {
     void theory_array::add_store(theory_var v, enode * s) {
         if (m_params.m_array_cg && !s->is_cgr())
             return;
-        SASSERT(is_store(s) || is_lambda(s));
+        SASSERT(is_store(s) || is_lambda(s->get_expr()));
         v                = find(v);
         var_data * d     = m_var_data[v];
         unsigned lambda_equiv_class_size = get_lambda_equiv_size(v, d);
@@ -204,7 +204,7 @@ namespace smt {
     void theory_array::instantiate_axiom2a(enode * select, enode * store) {
         TRACE(array, tout << "axiom 2a: #" << select->get_owner_id() << " #" << store->get_owner_id() << "\n";);
         SASSERT(is_select(select));
-        SASSERT(is_store(store) || is_lambda(store));
+        SASSERT(is_store(store) || is_lambda(store->get_expr()));
         if (assert_store_axiom2(store, select))
             m_stats.m_num_axiom2a++;
     }
@@ -212,7 +212,7 @@ namespace smt {
     bool theory_array::instantiate_axiom2b(enode * select, enode * store) {
         TRACE(array_axiom2b, tout << "axiom 2b: #" << select->get_owner_id() << " #" << store->get_owner_id() << "\n";);
         SASSERT(is_select(select));
-        SASSERT(is_store(store) || is_lambda(store));
+        SASSERT(is_store(store) || is_lambda(store->get_expr()));
         if (assert_store_axiom2(store, select)) {
             m_stats.m_num_axiom2b++;
             return true;
@@ -298,11 +298,6 @@ namespace smt {
 
     void theory_array::new_eq_eh(theory_var v1, theory_var v2) {
         m_find.merge(v1, v2);
-        enode* n1 = get_enode(v1), *n2 = get_enode(v2);
-        if (n1->get_decl()->is_lambda() ||
-            n2->get_decl()->is_lambda()) {
-            assert_congruent(n1, n2);
-        }
     }
 
     void theory_array::new_diseq_eh(theory_var v1, theory_var v2) {

src/smt/theory_array_base.cpp

@@ -219,13 +219,14 @@ namespace smt {
     }
 
     void theory_array_base::assert_lambda_axiom_core(enode* n, enode* select) {
-        SASSERT(is_lambda(n));
+        SASSERT(is_lambda(n->get_expr()));
         SASSERT(is_select(select));
         expr *e = n->get_expr();
+        SASSERT(is_lambda(e));
         app *s = select->get_app();
-        auto q = is_quantifier(e) ? to_quantifier(e) : m.is_lambda_def(e);
+        auto q = to_quantifier(e);
         SASSERT(q);
-        SASSERT(::is_lambda(q));
+
         SASSERT(q->get_num_decls() == s->get_num_args() - 1);
         // do the same thing as in sat/smt/array_axioms:
         ptr_vector<expr> args(s->get_num_args(), s->get_args());
@@ -241,7 +242,7 @@ namespace smt {
     }
     
     bool theory_array_base::assert_store_axiom2(enode * store, enode * select) { 
-        SASSERT(is_store(store) || is_lambda(store));
+        SASSERT(is_store(store) || is_lambda(store->get_expr()));
         unsigned num_args = select->get_num_args();
         unsigned        i = 1;
         for (; i < num_args; ++i) 
@@ -397,8 +398,8 @@ namespace smt {
         literal n1_eq_n2 = mk_eq(e1, e2, true);
         ctx.mark_as_relevant(n1_eq_n2);
         expr_ref_vector args1(m), args2(m);
-        args1.push_back(instantiate_lambda(e1));
-        args2.push_back(instantiate_lambda(e2));
+        args1.push_back(e1);
+        args2.push_back(e2);
         svector<symbol> names;
         sort_ref_vector sorts(m);
         for (unsigned i = 0; i < dimension; ++i) {
@@ -422,17 +423,6 @@ namespace smt {
         assert_axiom(~n1_eq_n2, fa_eq);
     }
 
-    expr_ref theory_array_base::instantiate_lambda(expr* e) {
-        quantifier * q = m.is_lambda_def(e);
-        expr_ref f(e, m);
-        if (q) {
-            // the variables in q are maybe not consecutive.
-            var_subst sub(m, false);
-            f = sub(q, to_app(e)->get_num_args(), to_app(e)->get_args());
-        }
-        return f;
-    }
-
     bool theory_array_base::can_propagate() {
         return 
             !m_axiom1_todo.empty() || 
@@ -443,7 +433,7 @@ namespace smt {
     }
 
     void theory_array_base::propagate() {
-        while (can_propagate()) {
+        while (theory_array_base::can_propagate()) {
             for (unsigned i = 0; i < m_axiom1_todo.size(); ++i)
                 assert_store_axiom1_core(m_axiom1_todo[i]);
             m_axiom1_todo.reset();

src/smt/theory_array_base.h

@@ -46,9 +46,6 @@ namespace smt {
         bool is_choice(expr const* n) const { return is_app(n) && to_app(n)->is_app_of(get_id(), OP_CHOICE); }
         bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); }
         bool is_array_sort(expr const* n) const { return is_array_sort(n->get_sort()); }
-        bool is_lambda(expr *n) const {
-            return m.is_lambda_def(n) || ::is_lambda(n);
-        }
         
 
         bool is_store(enode const * n) const { return is_store(n->get_expr()); }
@@ -59,9 +56,6 @@ namespace smt {
         bool is_choice(enode const* n) const { return is_choice(n->get_expr()); }
         bool is_default(enode const* n) const { return is_default(n->get_expr()); }
         bool is_array_sort(enode const* n) const { return is_array_sort(n->get_sort()); }
-        bool is_lambda(enode const *n) const {
-            return is_lambda(n->get_expr());
-        }
         
         
         

src/smt/theory_array_full.cpp

@@ -248,7 +248,7 @@ namespace smt {
             instantiate_default_as_array_axiom(n);
             d->m_as_arrays.push_back(n);
         }
-        else if (is_lambda(n)) {
+        else if (is_lambda(n->get_expr())) {
             instantiate_default_lambda_def_axiom(n);
             d->m_lambdas.push_back(n);
             m_lambdas.push_back(n);
@@ -578,13 +578,12 @@ namespace smt {
         if (!ctx.add_fingerprint(this, m_default_lambda_fingerprint, 1, &arr))
             return false;
         m_stats.m_num_default_lambda_axiom++;
-        expr* e = arr->get_expr();
-        expr_ref def(mk_default(e), m);
-        quantifier* lam = is_quantifier(e) ? to_quantifier(e) : m.is_lambda_def(e);
-        TRACE(array, tout << mk_pp(lam, m) << "\n" << mk_pp(e, m) << "\n");
+        quantifier *lam = to_quantifier(arr->get_expr());
+        expr_ref def(mk_default(arr->get_expr()), m);
+        TRACE(array, tout << mk_pp(lam, m) << "\n");
         expr_ref_vector args(m);       
         var_subst subst(m, false);
-        args.push_back(subst(lam, to_app(e)->get_num_args(), to_app(e)->get_args()));
+        args.push_back(lam);
         for (unsigned i = 0; i < lam->get_num_decls(); ++i) 
             args.push_back(mk_epsilon(lam->get_decl_sort(i)).first);
         expr_ref val(mk_select(args), m);

src/smt/theory_fpa.cpp

@@ -494,6 +494,31 @@ namespace smt {
         else if (is_app(n) && to_app(n)->get_family_id() == get_family_id()) {
             // These are the conversion functions fp.to_* */
             SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n));
+
+            // The conversion equality and side conditions for fp.to_* terms are
+            // emitted in internalize_term(), which runs exactly once. Those are
+            // asserted as theory axioms at the current decision level and are
+            // undone on DPLL backtracking, while internalize_term() is not run
+            // again for the already-internalized term (e.g. when the term lives
+            // at the user push base level and its clause is not reinitialized).
+            // The side conditions include the axioms linking FP uninterpreted
+            // functions to their bit-vector counterparts; losing them leaves the
+            // BV counterpart unconstrained and causes an incremental-mode
+            // soundness bug. relevant_eh re-fires on relevancy re-propagation
+            // after a backtrack, so re-emit them here to keep them in force.
+            switch ((fpa_op_kind)to_app(n)->get_decl_kind()) {
+            case OP_FPA_TO_FP:
+            case OP_FPA_TO_UBV:
+            case OP_FPA_TO_SBV:
+            case OP_FPA_TO_REAL:
+            case OP_FPA_TO_IEEE_BV: {
+                expr_ref conv = convert(n);
+                assert_cnstr(m.mk_eq(n, conv));
+                assert_cnstr(mk_side_conditions());
+                break;
+            }
+            default: /* ignore */;
+            }
         }
         else {
             /* Theory variables can be merged when (= bv-term (bvwrap fp-term)),

src/solver/check_sat_result.cpp

@@ -70,9 +70,6 @@ simple_check_sat_result::simple_check_sat_result(ast_manager & m):
     m_proof(m) {
     }
 
-void simple_check_sat_result::collect_statistics(statistics & st) const { 
-    st.copy(m_stats); 
-}
 
 void simple_check_sat_result::get_unsat_core(expr_ref_vector & r) { 
     if (m_status == l_false) {

src/solver/check_sat_result.h

@@ -46,6 +46,8 @@ protected:
     lbool       m_status = l_undef; 
     model_converter_ref m_mc0;
     double      m_time = 0;
+    statistics m_stats;
+
 public:
     check_sat_result(ast_manager& m): m(m), m_log(m), m_proof(m) {}
     virtual ~check_sat_result() = default;
@@ -53,7 +55,18 @@ public:
     void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
     lbool set_status(lbool r) { return m_status = r; }
     lbool status() const { return m_status; }
-    virtual void collect_statistics(statistics & st) const = 0;
+    void collect_statistics(statistics &st) const {
+        collect_statistics_core(st);
+        st.copy(m_stats);       
+    }
+    void add_statistics(statistics const &st) {
+        m_stats.copy(st);
+    }
+    void reset_statistics() {
+        m_stats.reset();
+    }
+   
+    virtual void collect_statistics_core(statistics &st) const = 0;
     virtual void get_unsat_core(expr_ref_vector & r) = 0;
     void set_model_converter(model_converter* mc) { m_mc0 = mc; }
     model_converter* mc0() const { return m_mc0.get(); }
@@ -92,7 +105,6 @@ public:
    \brief Very simple implementation of the check_sat_result object.
 */
 struct simple_check_sat_result : public check_sat_result {
-    statistics      m_stats;
     model_ref       m_model;
     expr_ref_vector m_core;
     proof_ref       m_proof;
@@ -100,9 +112,9 @@ struct simple_check_sat_result : public check_sat_result {
     
     simple_check_sat_result(ast_manager & m);
     ast_manager& get_manager() const override { return m_proof.get_manager(); }
-    void collect_statistics(statistics & st) const override;
     void get_unsat_core(expr_ref_vector & r) override;
     void get_model_core(model_ref & m) override;
+    void collect_statistics_core(statistics &st) const override {}
     proof * get_proof_core() override;
     std::string reason_unknown() const override;
     void get_labels(svector<symbol> & r) override;

src/solver/combined_solver.cpp

@@ -290,7 +290,7 @@ public:
         return m_solver1->display(out, n, es);
     }
 
-    void collect_statistics(statistics & st) const override {
+    void collect_statistics_core(statistics & st) const override {
         m_solver2->collect_statistics(st);
         if (m_use_solver1_results)
             m_solver1->collect_statistics(st);

src/solver/simplifier_solver.cpp

@@ -229,7 +229,7 @@ public:
         return s->check_sat_core(num_assumptions, _assumptions.data()); 
     }
 
-    void collect_statistics(statistics& st) const override { 
+    void collect_statistics_core(statistics& st) const override { 
         s->collect_statistics(st); 
         m_preprocess.collect_statistics(st);
     }

src/solver/slice_solver.cpp

@@ -319,7 +319,7 @@ public:
         return s->check_sat_core(num_assumptions, assumptions);
     }
 
-    void collect_statistics(statistics& st) const override { s->collect_statistics(st); }
+    void collect_statistics_core(statistics& st) const override { s->collect_statistics(st); }
 
     void get_model_core(model_ref& mdl) override { s->get_model_core(mdl); }
 

src/solver/solver_pool.cpp

@@ -83,7 +83,7 @@ public:
     void pop_params() override {m_base->pop_params();}
     
     void collect_param_descrs(param_descrs & r) override { m_base->collect_param_descrs(r); }
-    void collect_statistics(statistics & st) const override { m_base->collect_statistics(st); }
+    void collect_statistics_core(statistics & st) const override { m_base->collect_statistics(st); }
     unsigned get_num_assertions() const override { return m_base->get_num_assertions(); }
     expr * get_assertion(unsigned idx) const override { return m_base->get_assertion(idx); }
 

src/solver/tactic2solver.cpp

@@ -49,7 +49,7 @@ class tactic2solver : public solver_na2as {
     bool                         m_produce_models;
     bool                         m_produce_proofs;
     bool                         m_produce_unsat_cores;
-    statistics                   m_stats;
+//    statistics                   m_stats;
     bool                         m_minimizing = false;
     
 public:
@@ -70,7 +70,7 @@ public:
     void pop_core(unsigned n) override;
     lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override;
 
-    void collect_statistics(statistics & st) const override;
+    void collect_statistics_core(statistics & st) const override;
     void get_unsat_core(expr_ref_vector & r) override;
     void get_model_core(model_ref & m) override;
     proof * get_proof_core() override;
@@ -284,8 +284,9 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
         m_result->m_unknown = ex.what();
         m_result->m_proof = pr;
     }
-    m_tactic->collect_statistics(m_result->m_stats);
-    m_tactic->collect_statistics(m_stats);
+    statistics stats;
+    m_tactic->collect_statistics(stats);
+    m_result->add_statistics(stats);
     m_result->m_model = md;
     m_result->m_proof = pr;
     if (m_produce_unsat_cores) {
@@ -311,7 +312,7 @@ solver* tactic2solver::translate(ast_manager& m, params_ref const& p) {
 }
 
 
-void tactic2solver::collect_statistics(statistics & st) const {    
+void tactic2solver::collect_statistics_core(statistics & st) const {    
     st.copy(m_stats);
     if (m_stats.size() == 0 && m_tactic)
         m_tactic->collect_statistics(st);

src/tactic/fd_solver/bounded_int2bv_solver.cpp

@@ -159,7 +159,7 @@ public:
     void collect_param_descrs(param_descrs & r) override { m_solver->collect_param_descrs(r); }
     void set_produce_models(bool f) override { m_solver->set_produce_models(f); }
     void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback);  }
-    void collect_statistics(statistics & st) const override { m_solver->collect_statistics(st); }
+    void collect_statistics_core(statistics & st) const override { m_solver->collect_statistics(st); }
     void get_unsat_core(expr_ref_vector & r) override { m_solver->get_unsat_core(r); }
     void set_phase(expr* e) override { m_solver->set_phase(e); }
     phase* get_phase() override { return m_solver->get_phase(); }

src/tactic/fd_solver/enum2bv_solver.cpp

@@ -85,7 +85,7 @@ public:
     void collect_param_descrs(param_descrs & r) override { m_solver->collect_param_descrs(r); }    
     void set_produce_models(bool f) override { m_solver->set_produce_models(f); }
     void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback);  }
-    void collect_statistics(statistics & st) const override { m_solver->collect_statistics(st); }
+    void collect_statistics_core(statistics & st) const override { m_solver->collect_statistics(st); }
     void get_unsat_core(expr_ref_vector & r) override { m_solver->get_unsat_core(r); }
     void set_phase(expr* e) override { m_solver->set_phase(e); }
     phase* get_phase() override { return m_solver->get_phase(); }

src/tactic/fd_solver/pb2bv_solver.cpp

@@ -82,7 +82,7 @@ public:
     void collect_param_descrs(param_descrs & r) override { m_solver->collect_param_descrs(r); m_rewriter.collect_param_descrs(r);}    
     void set_produce_models(bool f) override { m_solver->set_produce_models(f); }
     void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback);  }
-    void collect_statistics(statistics & st) const override { 
+    void collect_statistics_core(statistics & st) const override { 
         m_rewriter.collect_statistics(st);
         m_solver->collect_statistics(st); 
     }

src/tactic/fd_solver/smtfd_solver.cpp

@@ -2032,7 +2032,7 @@ namespace smtfd {
 
         void set_produce_models(bool f) override { }
         void set_progress_callback(progress_callback * callback) override { }
-        void collect_statistics(statistics & st) const override {
+        void collect_statistics_core(statistics & st) const override {
             if (m_fd_sat_solver) {
                 m_fd_sat_solver->collect_statistics(st); 
                 m_fd_core_solver->collect_statistics(st); 

src/test/CMakeLists.txt

@@ -115,6 +115,7 @@ add_executable(test-z3
   prime_generator.cpp
   proof_checker.cpp
   qe_arith.cpp
+  mbp_qel.cpp
   quant_elim.cpp
   quant_solve.cpp
   random.cpp

src/test/main.cpp

@@ -163,6 +163,7 @@
     X(rcf) \
     X(polynorm) \
     X(qe_arith) \
+    X(mbp_qel) \
     X(expr_substitution) \
     X(sorting_network) \
     X(theory_pb) \

src/test/mbp_qel.cpp

@@ -0,0 +1,251 @@
+
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    mbp_qel.cpp
+
+Abstract:
+
+    Unit tests for model-based projection with QEL (term-graph based)
+
+Author:
+
+    Hari Govind V K (hgvk94) 2025-05-25
+
+--*/
+
+#include "qe/qe_mbp.h"
+#include "ast/reg_decl_plugins.h"
+#include "ast/datatype_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/ast_pp.h"
+#include "smt/smt_context.h"
+#include "params/smt_params.h"
+#include <iostream>
+
+// Test that MBP with QEL does not return false for a satisfiable formula
+// involving datatype accessors applied past the end of a list.
+//
+// Formula: (and ((_ is cons) x) ((_ is nil) (tl x)) (= nil (tl (tl x))) (< 8 n))
+// Project: x
+// Expected: result should imply n >= 9 (and model should satisfy it)
+// Bug: QEL was returning false because rm_accessor unconditionally
+//      assumed (tl x) has constructor cons when eliminating (tl (tl x)),
+//      contradicting the ((_ is nil) (tl x)) literal.
+static void test_dt_accessor_past_end() {
+    std::cout << "test_dt_accessor_past_end\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    datatype_util dt(m);
+    arith_util a(m);
+
+    // Create list datatype: (declare-datatypes ((L 0)) (((cons (hd Int) (tl L)) (nil))))
+    sort_ref int_sort(a.mk_int(), m);
+    func_decl_ref cons(m), is_cons(m), head(m), tail(m), nil(m), is_nil(m);
+    sort_ref L = dt.mk_list_datatype(int_sort, symbol("L"),
+                                     cons, is_cons, head, tail, nil, is_nil);
+
+    // Declare variables
+    app_ref x(m.mk_const("x", L), m);
+    app_ref n(m.mk_const("n", int_sort), m);
+
+    // Build formula: (and ((_ is cons) x) ((_ is nil) (tl x)) (= nil (tl (tl x))) (< 8 n))
+    expr_ref tl_x(m.mk_app(tail, x.get()), m);
+    expr_ref tl_tl_x(m.mk_app(tail, tl_x.get()), m);
+    expr_ref nil_val(m.mk_const(nil), m);
+
+    expr_ref is_cons_x(m.mk_app(is_cons, x.get()), m);
+    expr_ref is_nil_tl_x(m.mk_app(is_nil, tl_x.get()), m);
+    expr_ref eq_nil_tl_tl_x(m.mk_eq(nil_val, tl_tl_x), m);
+    expr_ref lt_8_n(a.mk_lt(a.mk_int(8), n), m);
+
+    expr_ref_vector conjs(m);
+    conjs.push_back(is_cons_x).push_back(is_nil_tl_x).push_back(eq_nil_tl_tl_x).push_back(lt_8_n);
+    expr_ref fml(m.mk_and(conjs), m);
+
+    std::cout << "  formula:\n     " << mk_pp(fml, m, 5) << "\n";
+
+    // Get a model
+    smt_params params;
+    params.m_model = true;
+    model_ref mdl;
+    {
+        smt::context ctx(m, params);
+        ctx.assert_expr(fml);
+        lbool result = ctx.check();
+        VERIFY(result == l_true);
+        ctx.get_model(mdl);
+    }
+
+    std::cout << "  model: x = " << mk_pp((*mdl)(x), m)
+              << ", n = " << mk_pp((*mdl)(n), m) << "\n";
+
+    // Call MBP with QEL enabled
+    app_ref_vector vars(m);
+    vars.push_back(x);
+
+    params_ref p;
+    p.set_bool("qsat_use_qel", true);
+    qe::mbproj mbp(m, p);
+    expr_ref projected(fml, m);
+    mbp.spacer(vars, *mdl.get(), projected);
+
+    std::cout << "  projected (qel=true):\n     " << mk_pp(projected, m, 5) << "\n";
+
+    // The result must not be false
+    VERIFY(!m.is_false(projected));
+
+    // The model should satisfy the projected formula
+    VERIFY(mdl->is_true(projected));
+
+    // x should have been eliminated
+    VERIFY(vars.empty());
+
+    std::cout << "  PASS\n\n";
+}
+
+// Same test but with a deeper list structure:
+// x is a 2-element list with a past-end accessor constraint
+// Formula: (and ((_ is cons) x) ((_ is cons) (tl x)) ((_ is nil) (tl (tl x)))
+//               (= nil (tl (tl (tl x)))) (< 8 n))
+static void test_dt_accessor_past_end_depth2() {
+    std::cout << "test_dt_accessor_past_end_depth2\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    datatype_util dt(m);
+    arith_util a(m);
+
+    sort_ref int_sort(a.mk_int(), m);
+    func_decl_ref cons(m), is_cons(m), head(m), tail(m), nil(m), is_nil(m);
+    sort_ref L = dt.mk_list_datatype(int_sort, symbol("L"),
+                                     cons, is_cons, head, tail, nil, is_nil);
+
+    app_ref x(m.mk_const("x", L), m);
+    app_ref n(m.mk_const("n", int_sort), m);
+
+    // Build: (and (is-cons x) (is-cons (tl x)) (is-nil (tl (tl x)))
+    //             (= nil (tl (tl (tl x)))) (< 8 n))
+    expr_ref tl_x(m.mk_app(tail, x.get()), m);
+    expr_ref tl_tl_x(m.mk_app(tail, tl_x.get()), m);
+    expr_ref tl_tl_tl_x(m.mk_app(tail, tl_tl_x.get()), m);
+    expr_ref nil_val(m.mk_const(nil), m);
+
+    expr_ref is_cons_x(m.mk_app(is_cons, x.get()), m);
+    expr_ref is_cons_tl_x(m.mk_app(is_cons, tl_x.get()), m);
+    expr_ref is_nil_tl_tl_x(m.mk_app(is_nil, tl_tl_x.get()), m);
+    expr_ref eq_nil_tl3(m.mk_eq(nil_val, tl_tl_tl_x), m);
+    expr_ref lt_8_n(a.mk_lt(a.mk_int(8), n), m);
+
+    expr_ref_vector conjs(m);
+    conjs.push_back(is_cons_x).push_back(is_cons_tl_x).push_back(is_nil_tl_tl_x).push_back(eq_nil_tl3).push_back(lt_8_n);
+    expr_ref fml(m.mk_and(conjs), m);
+
+    std::cout << "  formula:\n     " << mk_pp(fml, m, 5) << "\n";
+
+    smt_params sparams;
+    sparams.m_model = true;
+    model_ref mdl;
+    {
+        smt::context ctx(m, sparams);
+        ctx.assert_expr(fml);
+        lbool result = ctx.check();
+        VERIFY(result == l_true);
+        ctx.get_model(mdl);
+    }
+
+    std::cout << "  model: x = " << mk_pp((*mdl)(x), m)
+              << ", n = " << mk_pp((*mdl)(n), m) << "\n";
+
+    app_ref_vector vars(m);
+    vars.push_back(x);
+
+    params_ref p;
+    p.set_bool("qsat_use_qel", true);
+    qe::mbproj mbp(m, p);
+    expr_ref projected(fml, m);
+    mbp.spacer(vars, *mdl.get(), projected);
+
+    std::cout << "  projected (qel=true):\n     " << mk_pp(projected, m, 5) << "\n";
+
+    VERIFY(!m.is_false(projected));
+    VERIFY(mdl->is_true(projected));
+    VERIFY(vars.empty());
+
+    std::cout << "  PASS\n\n";
+}
+
+// Test with multiple DT variables projected simultaneously
+// Formula: (and (= nil (tl (tl (tl x)))) ((_ is nil) (tl (tl x)))
+//               ((_ is cons) y) ((_ is nil) (tl y)) (< 8 n))
+// Project: x, y
+static void test_dt_multiple_vars() {
+    std::cout << "test_dt_multiple_vars\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    datatype_util dt(m);
+    arith_util a(m);
+
+    sort_ref int_sort(a.mk_int(), m);
+    func_decl_ref cons(m), is_cons(m), head(m), tail(m), nil(m), is_nil(m);
+    sort_ref L = dt.mk_list_datatype(int_sort, symbol("L"),
+                                     cons, is_cons, head, tail, nil, is_nil);
+
+    app_ref x(m.mk_const("x", L), m);
+    app_ref y(m.mk_const("y", L), m);
+    app_ref n(m.mk_const("n", int_sort), m);
+
+    expr_ref tl_x(m.mk_app(tail, x.get()), m);
+    expr_ref tl_tl_x(m.mk_app(tail, tl_x.get()), m);
+    expr_ref tl_tl_tl_x(m.mk_app(tail, tl_tl_x.get()), m);
+    expr_ref tl_y(m.mk_app(tail, y.get()), m);
+    expr_ref nil_val(m.mk_const(nil), m);
+
+    expr_ref eq_nil_tl3x(m.mk_eq(nil_val, tl_tl_tl_x), m);
+    expr_ref is_nil_tl2x(m.mk_app(is_nil, tl_tl_x.get()), m);
+    expr_ref is_cons_y(m.mk_app(is_cons, y.get()), m);
+    expr_ref is_nil_tl_y(m.mk_app(is_nil, tl_y.get()), m);
+    expr_ref lt_8_n(a.mk_lt(a.mk_int(8), n), m);
+
+    expr_ref_vector conjs(m);
+    conjs.push_back(eq_nil_tl3x).push_back(is_nil_tl2x).push_back(is_cons_y).push_back(is_nil_tl_y).push_back(lt_8_n);
+    expr_ref fml(m.mk_and(conjs), m);
+
+    std::cout << "  formula:\n     " << mk_pp(fml, m, 5) << "\n";
+
+    smt_params sparams;
+    sparams.m_model = true;
+    model_ref mdl;
+    {
+        smt::context ctx(m, sparams);
+        ctx.assert_expr(fml);
+        lbool result = ctx.check();
+        VERIFY(result == l_true);
+        ctx.get_model(mdl);
+    }
+
+    app_ref_vector vars(m);
+    vars.push_back(x);
+    vars.push_back(y);
+
+    params_ref p;
+    p.set_bool("qsat_use_qel", true);
+    qe::mbproj mbp(m, p);
+    expr_ref projected(fml, m);
+    mbp.spacer(vars, *mdl.get(), projected);
+
+    std::cout << "  projected (qel=true):\n     " << mk_pp(projected, m, 5) << "\n";
+
+    VERIFY(!m.is_false(projected));
+    VERIFY(mdl->is_true(projected));
+    VERIFY(vars.empty());
+
+    std::cout << "  PASS\n\n";
+}
+
+void tst_mbp_qel() {
+    test_dt_accessor_past_end();
+    test_dt_accessor_past_end_depth2();
+    test_dt_multiple_vars();
+}

src/test/sls_seq_plugin.cpp

@@ -351,4 +351,28 @@ void tst_sls_seq_plugin() {
     app_ref eq(m.mk_eq(l, r), m);
     verbose_stream() << eq << "\n";
     ts.repair_down_str_eq_edit_distance_incremental(eq);
+
+    test_seq::string_instance lhs, rhs;
+    lhs.s = zstring("a");
+    lhs.is_value.push_back(false);
+    lhs.prev_is_var.push_back(false);
+    lhs.next_is_var.push_back(false);
+    rhs.s = zstring("ab");
+    rhs.is_value.push_back(true);
+    rhs.prev_is_var.push_back(false);
+    rhs.next_is_var.push_back(false);
+    rhs.is_value.push_back(false);
+    rhs.prev_is_var.push_back(false);
+    rhs.next_is_var.push_back(false);
+
+    ENSURE(ts.edit_distance_with_updates(lhs, rhs) == 0);
+    ENSURE(ts.m_string_updates.size() == 2);
+    ENSURE(ts.m_string_updates[0].side == test_seq::side_t::right);
+    ENSURE(ts.m_string_updates[0].op == test_seq::op_t::add);
+    ENSURE(ts.m_string_updates[0].i == 0);
+    ENSURE(ts.m_string_updates[0].j == 1);
+    ENSURE(ts.m_string_updates[1].side == test_seq::side_t::right);
+    ENSURE(ts.m_string_updates[1].op == test_seq::op_t::del);
+    ENSURE(ts.m_string_updates[1].i == 1);
+    ENSURE(ts.m_string_updates[1].j == 0);
 }

src/test/smt2print_parse.cpp

@@ -322,8 +322,8 @@ void tst_smt2print_parse() {
     // Test ?
 
     test_repeated_eval();
-    //test_ho_curried_application();
-    //test_ho_choice_expression();
+    test_ho_curried_application();
+    test_ho_choice_expression();
 
     test_symbol_escape();
 

src/test/tptp.cpp

@@ -73,10 +73,10 @@ fof(c1,conjecture, p(a)).)",
 R"(cnf(c1,axiom, p(X)).
 cnf(c2,axiom, ~ p(a)).)",
          "% SZS status Unsatisfiable"},
-        {"fof-bare-constant-equality",
-R"(fof(a1,axiom, ! [X] : (X = a)).
-fof(c1,conjecture, b = a).)",
-         "% SZS status Theorem"},
+//        {"fof-bare-constant-equality",
+//  R"(fof(a1,axiom, ! [X] : (X = a)).
+//fof(c1,conjecture, b = a).)",
+//         "% SZS status Theorem"},
         {"tff-negative-literal",
 R"(tff(c1,conjecture, $less(-2,2)).)",
          "% SZS status Theorem"},
@@ -115,6 +115,7 @@ R"(tff(c1,conjecture, $let(a: $int, a := 5, $let(b: $int, b := 3, $less(b,a)))).
     };
     for (auto const& c : cases) {
         std::string out = run_tptp(c.input);
+        std::cout << c.name << " status: " << c.expected_status << " out: " << out << "\n";
         ENSURE(out.find(c.expected_status) != std::string::npos);
     }
 

src/util/timeout.cpp

@@ -19,6 +19,7 @@ Revision History:
 
 --*/
 #include<iostream>
+#include<signal.h>
 #include "util/util.h"
 #include "util/timeout.h"
 #include "util/error_codes.h"
@@ -29,15 +30,28 @@ Revision History:
 static scoped_timer * g_timeout = nullptr;
 static void (* g_on_timeout)() = nullptr;
 
+static void do_timeout() {
+    std::cout << "timeout\n";
+    std::cout.flush();
+    if (g_on_timeout)
+        g_on_timeout();
+}
+
+#ifdef SIGXCPU
+// React to SIGXCPU (an external CPU limit, e.g. ulimit -t) like a -T timeout.
+static void STD_CALL on_sigxcpu(int) {
+    signal(SIGXCPU, SIG_DFL);
+    do_timeout();
+    raise(SIGXCPU);
+}
+#endif
+
 namespace {
 class g_timeout_eh : public event_handler {
 public:
     void operator()(event_handler_caller_t caller_id) override {
         m_caller_id = caller_id;
-        std::cout << "timeout\n";
-        std::cout.flush();
-        if (g_on_timeout)
-            g_on_timeout();
+        do_timeout();
         throw z3_error(ERR_TIMEOUT);
     }
 };
@@ -56,4 +70,8 @@ void disable_timeout() {
 
 void register_on_timeout_proc(void (*proc)()) {
     g_on_timeout = proc;
+#ifdef SIGXCPU
+    // Handle external CPU limits (SIGXCPU) like our own timeouts.
+    signal(SIGXCPU, on_sigxcpu);
+#endif
 }