diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp
index b820b5213..198514671 100644
--- a/src/ast/array_decl_plugin.cpp
+++ b/src/ast/array_decl_plugin.cpp
@@ -35,9 +35,7 @@ array_decl_plugin::array_decl_plugin():
     m_set_complement_sym("complement"),
     m_set_subset_sym("subset"),
     m_array_ext_sym("array-ext"),
-    m_as_array_sym("as-array"),
-    m_set_has_size_sym("set-has-size"),
-    m_set_card_sym("card") {
+    m_as_array_sym("as-array") {
 }
 
 #define ARRAY_SORT_STR "Array"
@@ -442,40 +440,6 @@ func_decl * array_decl_plugin::mk_set_subset(unsigned arity, sort * const * doma
                                    func_decl_info(m_family_id, OP_SET_SUBSET));
 }
 
-func_decl * array_decl_plugin::mk_set_card(unsigned arity, sort * const* domain) {
-    if (arity != 1) {
-        m_manager->raise_exception("card takes only one argument");
-        return nullptr;
-    }    
-
-    arith_util arith(*m_manager);
-    if (!is_array_sort(domain[0]) || !m_manager->is_bool(get_array_range(domain[0]))) {
-        m_manager->raise_exception("card expects an array of Booleans");
-    }
-    sort * int_sort = arith.mk_int();
-    return m_manager->mk_func_decl(m_set_card_sym, arity, domain, int_sort,
-                                   func_decl_info(m_family_id, OP_SET_CARD));
-}
-
-func_decl * array_decl_plugin::mk_set_has_size(unsigned arity, sort * const* domain) {
-    if (arity != 2) {
-        m_manager->raise_exception("set-has-size takes two arguments");
-        return nullptr;
-    }    
-    m_manager->raise_exception("set-has-size is not supported");
-    // domain[0] is a Boolean array,
-    // domain[1] is Int
-    arith_util arith(*m_manager);
-    if (!arith.is_int(domain[1])) {
-        m_manager->raise_exception("set-has-size expects second argument to be an integer");
-    }
-    if (!is_array_sort(domain[0]) || !m_manager->is_bool(get_array_range(domain[0]))) {
-        m_manager->raise_exception("set-has-size expects first argument to be an array of Booleans");
-    }
-    sort * bool_sort = m_manager->mk_bool_sort();
-    return m_manager->mk_func_decl(m_set_has_size_sym, arity, domain, bool_sort,
-                                   func_decl_info(m_family_id, OP_SET_HAS_SIZE));
-}
 
 func_decl * array_decl_plugin::mk_as_array(func_decl * f) {
     vector<parameter> parameters;
@@ -541,10 +505,6 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         return mk_set_complement(arity, domain);
     case OP_SET_SUBSET:
         return mk_set_subset(arity, domain);
-    case OP_SET_HAS_SIZE:
-        return mk_set_has_size(arity, domain);
-    case OP_SET_CARD:
-        return mk_set_card(arity, domain);
     case OP_AS_ARRAY: {
         if (num_parameters != 1 ||
             !parameters[0].is_ast() || 
diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
index 50c9cf5d1..36403f3ca 100644
--- a/src/ast/array_decl_plugin.h
+++ b/src/ast/array_decl_plugin.h
@@ -62,8 +62,6 @@ enum array_op_kind {
     OP_SET_DIFFERENCE,
     OP_SET_COMPLEMENT,
     OP_SET_SUBSET,
-    OP_SET_HAS_SIZE,
-    OP_SET_CARD,
     OP_AS_ARRAY, // used for model construction
     LAST_ARRAY_OP
 };
@@ -81,8 +79,6 @@ class array_decl_plugin : public decl_plugin {
     symbol m_set_subset_sym;
     symbol m_array_ext_sym;
     symbol m_as_array_sym;
-    symbol m_set_has_size_sym;
-    symbol m_set_card_sym;
 
     bool check_set_arguments(unsigned arity, sort * const * domain);
 
@@ -110,10 +106,6 @@ class array_decl_plugin : public decl_plugin {
 
     func_decl * mk_as_array(func_decl * f);
 
-    func_decl* mk_set_has_size(unsigned arity, sort * const* domain);
-
-    func_decl* mk_set_card(unsigned arity, sort * const* domain);
-
     bool is_array_sort(sort* s) const;
  public:
     array_decl_plugin();
@@ -173,8 +165,6 @@ public:
     bool is_complement(expr* n) const { return is_app_of(n, m_fid, OP_SET_COMPLEMENT); }
     bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
     bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); }
-    bool is_set_has_size(expr* e) const { return is_app_of(e, m_fid, OP_SET_HAS_SIZE); }
-    bool is_set_card(expr* e) const { return is_app_of(e, m_fid, OP_SET_CARD); }
     bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); }
     bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); }
     bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
@@ -182,8 +172,6 @@ public:
     bool is_union(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_UNION); }
     bool is_intersect(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_INTERSECT); }
     bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
-    bool is_set_has_size(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_HAS_SIZE); }
-    bool is_set_card(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_CARD); }
     bool is_default(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_DEFAULT); }
     bool is_default(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_DEFAULT); }
     bool is_subset(expr const* n) const { return is_app_of(n, m_fid, OP_SET_SUBSET); }
@@ -307,14 +295,6 @@ public:
         return m_manager.mk_app(m_fid, OP_SET_UNION, s1, s2);
     }
 
-    app* mk_has_size(expr* set, expr* n) {
-        return m_manager.mk_app(m_fid, OP_SET_HAS_SIZE, set, n);
-    }
-
-    app* mk_card(expr* set) {
-        return m_manager.mk_app(m_fid, OP_SET_CARD, set);
-    }
-
     func_decl * mk_array_ext(sort* domain, unsigned i);
 
     sort * mk_array_sort(sort* dom, sort* range) { return mk_array_sort(1, &dom, range); }
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 8a8c3c8f8..c58a887c4 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1282,7 +1282,7 @@ void core::add_bounds() {
     }    
 }
 
-lbool core::check() {
+lbool core::check(unsigned level) {
     lp_settings().stats().m_nla_calls++;
     TRACE(nla_solver, tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";);
     lra.get_rid_of_inf_eps();
@@ -1363,7 +1363,7 @@ lbool core::check() {
             ret = bounded_nlsat();
     }
 
-    if (no_effect() && params().arith_nl_nra()) {
+    if (no_effect() && params().arith_nl_nra() && level >= 2) {
         scoped_limits sl(m_reslim);
         sl.push_child(&m_nra_lim);
         params_ref p;
@@ -1432,7 +1432,7 @@ bool core::no_lemmas_hold() const {
     
 lbool core::test_check() {
     lra.set_status(lp::lp_status::OPTIMAL);
-    return check();
+    return check(2);
 }
 
 std::unordered_set<lpvar> core::get_vars_of_expr_with_opening_terms(const nex *e ) {
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index baacbc8e8..fed6dfe72 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -394,7 +394,7 @@ public:
 
     bool  conflict_found() const;
     
-    lbool check();
+    lbool check(unsigned level);
     lbool check_power(lpvar r, lpvar x, lpvar y);
     void check_bounded_divisions();
 
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index dcf2266c1..eb669ab4b 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -46,8 +46,8 @@ namespace nla {
     
     bool solver::need_check() { return m_core->has_relevant_monomial(); }
     
-    lbool solver::check() {
-        return m_core->check();
+    lbool solver::check(unsigned level) {
+        return m_core->check(level);
     }
 
     void solver::propagate() {
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index 133117149..e6d02e793 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -37,7 +37,7 @@ namespace nla {
         void push();
         void pop(unsigned scopes);
         bool need_check();
-        lbool check();
+        lbool check(unsigned level);
         void propagate();
         void simplify() { m_core->simplify(); }
         lbool check_power(lpvar r, lpvar x, lpvar y);
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 1695f5e41..0fab5105c 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1000,6 +1000,7 @@ namespace arith {
     }
 
     sat::check_result solver::check() {
+        unsigned level = 2;
         force_push();
         m_model_is_initialized = false;
         IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
@@ -1042,7 +1043,7 @@ namespace arith {
         if (!check_delayed_eqs())
             return sat::check_result::CR_CONTINUE;
 
-        switch (check_nla()) {
+        switch (check_nla(level)) {
         case l_true:
             m_use_nra_model = true;
             break;
@@ -1498,7 +1499,7 @@ namespace arith {
     }
 
 
-    lbool solver::check_nla() {
+    lbool solver::check_nla(unsigned level) {
         if (!m.inc()) {
             TRACE(arith, tout << "canceled\n";);
             return l_undef;
@@ -1509,7 +1510,7 @@ namespace arith {
         if (!m_nla->need_check())
             return l_true;
 
-        lbool r = m_nla->check();
+        lbool r = m_nla->check(level);
         switch (r) {
         case l_false:
             add_lemmas();
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index c11967869..29fa900ba 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -407,7 +407,7 @@ namespace arith {
         lbool make_feasible();
         bool  check_delayed_eqs();
         lbool check_lia();
-        lbool check_nla();
+        lbool check_nla(unsigned level);
         bool check_bv_terms();
         bool check_bv_term(app* n);
         void add_lemmas();
diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp
index 225d5d932..5ada91ac7 100644
--- a/src/sat/smt/array_internalize.cpp
+++ b/src/sat/smt/array_internalize.cpp
@@ -137,10 +137,6 @@ namespace array {
             add_equiv(eq, sub);
             break;
         }            
-        case OP_SET_HAS_SIZE:
-        case OP_SET_CARD:
-            ctx.unhandled_function(n->get_decl());
-            break;
         default:
             UNREACHABLE();
             break;
@@ -184,10 +180,6 @@ namespace array {
             break;
         case OP_SET_SUBSET:
             break;
-        case OP_SET_HAS_SIZE:
-        case OP_SET_CARD:
-            ctx.unhandled_function(n->get_decl());
-            break;
         default:
             UNREACHABLE();
             break;
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 1d9a72f79..9b620694c 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -644,6 +644,8 @@ namespace euf {
         return m_egraph.find(m.mk_false());
     }
 
+    // NB. revisit this for interleaving qsolver with theory solvers based on priorities of
+    // activities such as calling nlsat as a final check.
     sat::check_result solver::check() { 
         ++m_stats.m_final_checks;
         TRACE(euf, s().display(tout););
diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index 01e3a9254..98e79f484 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -49,7 +49,6 @@ z3_add_component(smt
     smt_value_sort.cpp
     smt2_extra_cmds.cpp
     theory_arith.cpp
-    theory_array_bapa.cpp
     theory_array_base.cpp
     theory_array.cpp
     theory_array_full.cpp
diff --git a/src/smt/smt_arith_value.cpp b/src/smt/smt_arith_value.cpp
index 068f401a0..bc512350d 100644
--- a/src/smt/smt_arith_value.cpp
+++ b/src/smt/smt_arith_value.cpp
@@ -157,10 +157,10 @@ namespace smt {
         return expr_ref(e, m);
     }    
 
-    final_check_status arith_value::final_check() {
+    final_check_status arith_value::final_check(unsigned level) {
         family_id afid = a.get_family_id();
         theory * th = m_ctx->get_theory(afid);
-        return th->final_check_eh();
+        return th->final_check_eh(level);
     }
 
 };
diff --git a/src/smt/smt_arith_value.h b/src/smt/smt_arith_value.h
index d802dcb18..09bd03d29 100644
--- a/src/smt/smt_arith_value.h
+++ b/src/smt/smt_arith_value.h
@@ -47,6 +47,6 @@ namespace smt {
         expr_ref get_lo(expr* e) const;
         expr_ref get_up(expr* e) const;
         expr_ref get_fixed(expr* e) const;
-        final_check_status final_check();
+        final_check_status final_check(unsigned );
     };
 };
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 4f73671ea..98ca809bc 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4122,16 +4122,18 @@ namespace smt {
         unsigned old_idx          = m_final_check_idx;
         unsigned num_th           = m_theory_set.size();
         unsigned range            = num_th + 1;
+        unsigned level = 1, max_level = 1;
         final_check_status result = FC_DONE;
         failure  f                = OK;
 
-        do {
+        while (true) {
             TRACE(final_check_step, tout << "processing: " << m_final_check_idx << ", result: " << result << "\n";);
             final_check_status ok;
             if (m_final_check_idx < num_th) {
                 theory * th = m_theory_set[m_final_check_idx];
                 IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"" << th->get_name() << "\")\n";);
-                ok = th->final_check_eh();
+                ok = th->final_check_eh(level);
+                max_level = std::max(max_level, th->num_final_check_levels());
                 TRACE(final_check_step, tout << "final check '" << th->get_name() << " ok: " << ok << " inconsistent " << inconsistent() << "\n";);
                 if (get_cancel_flag()) {
                     f = CANCELED;
@@ -4160,8 +4162,12 @@ namespace smt {
                 return FC_CONTINUE;
                 break;
             }
+            if (m_final_check_idx == old_idx) {
+                if (level >= max_level)
+                    break;
+                ++level;
+            }
         }
-        while (m_final_check_idx != old_idx);
 
         TRACE(final_check_step, tout << "result: " << result << "\n";);
 
diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h
index 20c7380eb..e6c361d3d 100644
--- a/src/smt/smt_theory.h
+++ b/src/smt/smt_theory.h
@@ -315,10 +315,21 @@ namespace smt {
            a truth value to all boolean variables and no inconsistency was 
            detected.
         */
-        virtual final_check_status final_check_eh() {
+        virtual final_check_status final_check_eh(unsigned level) {
             return FC_DONE;
         }
 
+        /**
+        * \brief This method signals the number of priority levels a theory supports for final checks.
+        * The first level are for the cheapest final check invocations.
+        * The levels after that are for more expensive final checks.
+        * This approach emulates a priority queue of actions taken at final check where the expensive
+        * checks are deferred.
+        */
+        virtual unsigned num_final_check_levels() const {
+            return 1;
+        }
+
         /**
            \brief Parametric theories (e.g. Arrays) should implement this method.
            See example in context::is_shared
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 3cfb870a1..f1ec345b1 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -679,7 +679,7 @@ namespace smt {
         */
         bool    m_liberal_final_check = true; 
         final_check_status final_check_core();
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         
         bool can_propagate() override;
         void propagate() override;
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 0a90495c7..44e373764 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1535,7 +1535,7 @@ namespace smt {
     }
 
     template<typename Ext>
-    final_check_status theory_arith<Ext>::final_check_eh() {
+    final_check_status theory_arith<Ext>::final_check_eh(unsigned level) {
         TRACE(arith_eq_adapter_info, m_arith_eq_adapter.display_already_processed(tout););
         TRACE(arith, display(tout););
 
diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp
index 4da9e5bca..2121848cc 100644
--- a/src/smt/theory_array.cpp
+++ b/src/smt/theory_array.cpp
@@ -359,7 +359,7 @@ namespace smt {
         SASSERT(m_find.get_num_vars() == get_num_vars());
     }
     
-    final_check_status theory_array::final_check_eh() {
+    final_check_status theory_array::final_check_eh(unsigned) {
         m_final_check_idx++;
         final_check_status r = FC_DONE;
         if (m_params.m_array_lazy_ieq) {
diff --git a/src/smt/theory_array.h b/src/smt/theory_array.h
index 9fc9dd44d..444216678 100644
--- a/src/smt/theory_array.h
+++ b/src/smt/theory_array.h
@@ -62,7 +62,7 @@ namespace smt {
         void relevant_eh(app * n) override;
         void push_scope_eh() override;
         void pop_scope_eh(unsigned num_scopes) override;
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         void reset_eh() override;
         void init_search_eh() override;
 
diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp
deleted file mode 100644
index 72aea761d..000000000
--- a/src/smt/theory_array_bapa.cpp
+++ /dev/null
@@ -1,644 +0,0 @@
-/*++
-Copyright (c) 2019 Microsoft Corporation
-
-Module Name:
-
-    theory_array_bapa.cpp
-
-Abstract:
-
-   Saturation procedure for BAPA predicates.
-   Assume there is a predicate
-
-           Size(S, n)   for S : Array(T, Bool) and n : Int
-
-   The predicate is true if S is a set of size n.
-
-
-                 Size(S, n), Size(T, m)      
-          S, T are intersecting. n != m or S != T
-D  ---------------------------------------------------------
-   Size(S, n) => Size(S\T, k1), Size(S n T, k2), n = k1 + k2
-   Size(T, m) => Size(T\S, k3), SIze(S n T, k2), m = k2 + k3   
-
-        Size(S, n)
-P  --------------------
-   Size(S, n) => n >= 0
-
-   Size(S, n), is infinite domain
-B  ------------------------------
-   Size(S, n) => default(S) = false
-
-   Size(S, n), Size(S, m)
-F  --------------------------------
-   Size(S, n), Size(S, m) =>  n = m
-
-   Fixing values during final check:
-      Size(S, n)
-V  -------------------
-   assume value(n) = n 
-   
-    Size(S, n), S[i1], ..., S[ik]
-O  -------------------------------
-   ~distinct(i1, ... ik) or n >= k
-
-                  Size(S,n)
-Ak -------------------------------------------------- 
-   S[i1] & .. & S[ik] & distinct(i1, .., ik) or n < k
-
-Q: Is this sufficient? Axiom A1 could be adjusted to add new elements i' until there are k witnesses for Size(S, k).
-This is quite bad when k is very large. Instead rely on stably infiniteness or other domain properties of the theories.
-
-When A is finite domain, or there are quantifiers there could be constraints that force domain sizes so domain sizes may have 
-to be enforced. A succinct way would be through domain comprehension assertions. 
-
-Finite domains:
-
-   Size(S, n), is finite domain
-   ----------------------------
-          S <= |A|
-
-     Size(S, n), !S[i1], .... !S[ik],  S is finite domain  
-   ----------------------------------------------------------
-   default(S) = false or ~distinct(i1,..,ik) or |A| - k <= n
-
-
-    ~Size(S, m) is negative on all occurrences, S is finite domain
-    ---------------------------------------------------------------
-                     Size(S, n) n fresh.
-
-    Model construction for infinite domains when all Size(S, m) are negative for S.
-
-Author:
-
-    Nikolaj Bjorner 2019-04-13
-
-Revision History:
-
- */
-
-#include "ast/ast_util.h"
-#include "ast/ast_pp.h"
-#include "ast/rewriter/array_rewriter.h"
-#include "smt/smt_context.h"
-#include "smt/smt_arith_value.h"
-#include "smt/theory_array_full.h"
-#include "smt/theory_array_bapa.h"
-
-#if 0
-- set of native select terms that are true
-- set of auxiliary select terms.
-- n1, n2, n3, n4.
-- a1, a2, a3, a4, a5.
-- 
-- add select terms, such that first 
-#endif
-
-namespace smt {
-    
-    class theory_array_bapa::imp {
-        struct sz_info {
-            bool                  m_is_leaf = true;               // has it been split into disjoint subsets already?
-            rational              m_size = rational::minus_one(); // set to >= integer if fixed in final check, otherwise -1
-            obj_map<enode, expr*> m_selects;
-        };
-
-        typedef std::pair<func_decl*, func_decl*> func_decls;
-
-        ast_manager&              m;
-        theory_array_full&        th;
-        arith_util                m_arith;
-        array_util                m_autil;
-        th_rewriter               m_rw;
-        arith_value               m_arith_value;
-        ast_ref_vector            m_pinned;
-        obj_map<app, sz_info*>    m_sizeof;
-        obj_map<expr, rational>   m_size_limit;
-        obj_map<sort, func_decls> m_index_skolems;
-        obj_map<sort, func_decl*> m_size_limit_sort2skolems;
-        unsigned                  m_max_set_enumeration;
-
-        context& ctx() { return th.get_context(); }
-
-        void reset() {
-            for (auto& kv : m_sizeof) {
-                dealloc(kv.m_value);
-            }
-        }
-
-        bool is_true(expr* e) { return is_true(ctx().get_literal(e)); }
-        bool is_true(enode* e) { return is_true(e->get_expr()); }
-        bool is_true(literal l) { return ctx().is_relevant(l) && ctx().get_assignment(l) == l_true; }
-        bool is_leaf(sz_info& i) const { return i.m_is_leaf; }
-        bool is_leaf(sz_info* i) const { return is_leaf(*i); }
-        enode* get_root(expr* e) { return ctx().get_enode(e)->get_root(); }
-        bool is_select(enode* n) { return th.is_select(n); }
-        app_ref mk_select(expr* a, expr* i) { expr* args[2] = { a, i }; return app_ref(m_autil.mk_select(2, args), m); }
-        literal get_literal(expr* e) { return ctx().get_literal(e); }
-        literal mk_literal(expr* e) { expr_ref _e(e, m); if (!ctx().e_internalized(e)) ctx().internalize(e, false); literal lit = get_literal(e); ctx().mark_as_relevant(lit); return lit; }
-        literal mk_eq(expr* a, expr* b) { 
-            expr_ref _a(a, m), _b(b, m); 
-            literal lit = th.mk_eq(a, b, false); 
-            ctx().mark_as_relevant(lit); 
-            return lit; 
-        }
-        void mk_th_axiom(literal l1, literal l2) {
-            literal lits[2] = { l1, l2 };
-            mk_th_axiom(2, lits);
-        }
-        void mk_th_axiom(literal l1, literal l2, literal l3) {
-            literal lits[3] = { l1, l2, l3 };
-            mk_th_axiom(3, lits);
-        }
-        void mk_th_axiom(unsigned n, literal* lits) {
-            TRACE(card, ctx().display_literals_verbose(tout, n, lits) << "\n";);
-            IF_VERBOSE(10, ctx().display_literals_verbose(verbose_stream(), n, lits) << "\n");
-            ctx().mk_th_axiom(th.get_id(), n, lits);            
-        }
-
-        void update_indices() {
-            for (auto const& kv : m_sizeof) {     
-                app* k = kv.m_key;
-                sz_info& v = *kv.m_value;
-                v.m_selects.reset();
-                if (is_true(k) && is_leaf(v)) {
-                    enode* set = get_root(k->get_arg(0));
-                    for (enode* parent : enode::parents(set)) {
-                        if (is_select(parent) && parent->get_arg(0)->get_root() == set) {
-                            if (is_true(parent)) {
-                                v.m_selects.insert(parent->get_arg(1)->get_root(), parent->get_expr());
-                            }
-                        }
-                    }                    
-                }
-            }
-        }
-
-        /**
-            F: Size(S, k1) & Size(S, k2) => k1 = k2
-         */
-        lbool ensure_functional() {
-            lbool result = l_true;
-            obj_map<enode, app*> parents;
-            for (auto const& kv : m_sizeof) {     
-                app* sz1 = kv.m_key;
-                if (!is_true(sz1)) {
-                    continue;
-                }
-                enode* r = get_root(sz1->get_arg(0));
-                app* sz2 = nullptr;
-                if (parents.find(r, sz2)) {
-                    expr* k1 = sz1->get_arg(1);
-                    expr* k2 = sz2->get_arg(1);
-                    if (get_root(k1) != get_root(k2)) {
-                        mk_th_axiom(~get_literal(sz1), ~get_literal(sz2), mk_eq(k1, k2));
-                        result = l_false;
-                    }
-                }
-                else {
-                    parents.insert(r, sz1);
-                }
-            }
-            return result;
-        }
-
-        /**
-           Enforce D
-         */
-        lbool ensure_disjoint() {
-            auto i = m_sizeof.begin(), end = m_sizeof.end();
-            for (; i != end; ++i) {
-                auto& kv = *i;
-                if (!kv.m_value->m_is_leaf) {
-                    continue;
-                }
-                for (auto j = i; ++j != end; ) {
-                    if (j->m_value->m_is_leaf && !ensure_disjoint(i->m_key, j->m_key)) {
-                        return l_false;
-                    }
-                }
-            }
-            return l_true;
-        }
-
-        bool ensure_disjoint(app* sz1, app* sz2) {
-            sz_info& i1 = *m_sizeof[sz1];
-            sz_info& i2 = *m_sizeof[sz2];
-            SASSERT(i1.m_is_leaf);
-            SASSERT(i2.m_is_leaf);
-            expr* s = sz1->get_arg(0);
-            expr* t = sz2->get_arg(0);
-            if (s->get_sort() != t->get_sort()) {
-                return true;
-            }
-            enode* r1 = get_root(s);
-            enode* r2 = get_root(t);
-            if (r1 == r2) {
-                return true;
-            }
-            if (!ctx().is_diseq(r1, r2) && ctx().assume_eq(r1, r2)) {
-                return false;
-            }
-            if (do_intersect(i1.m_selects, i2.m_selects)) {
-                add_disjoint(sz1, sz2);
-                return false;
-            }
-            return true;
-        }
-
-        bool do_intersect(obj_map<enode, expr*> const& s, obj_map<enode, expr*> const& t) const {
-            if (s.size() > t.size()) {
-                return do_intersect(t, s);
-            }
-            for (auto const& idx : s)
-                if (t.contains(idx.m_key)) 
-                    return true;
-            return false;
-        }
-
-        void add_disjoint(app* sz1, app* sz2) {
-            sz_info& i1 = *m_sizeof[sz1];
-            sz_info& i2 = *m_sizeof[sz2];
-            SASSERT(i1.m_is_leaf);
-            SASSERT(i2.m_is_leaf);
-            expr* t = sz1->get_arg(0);
-            expr* s = sz2->get_arg(0);
-            expr_ref tms = mk_subtract(t, s);
-            expr_ref smt = mk_subtract(s, t);
-            expr_ref tns = mk_intersect(t, s);
-#if 0
-            std::cout << tms << "\n";
-            std::cout << smt << "\n";
-            std::cout << tns << "\n";
-#endif
-#if 0
-            if (tns == sz1) {
-                std::cout << "SEEN " << tms << "\n";
-            }
-            if (tns == sz2) {
-                std::cout << "SEEN " << smt << "\n";                
-            }
-#endif
-            ctx().push_trail(value_trail<bool>(i1.m_is_leaf, false));
-            ctx().push_trail(value_trail<bool>(i2.m_is_leaf, false));
-            expr_ref k1(m), k2(m), k3(m);
-            expr_ref sz_tms(m), sz_tns(m), sz_smt(m);
-            k1 = m_autil.mk_card(tms);
-            k2 = m_autil.mk_card(tns);
-            k3 = m_autil.mk_card(smt);
-            sz_tms = m_autil.mk_has_size(tms, k1);
-            sz_tns = m_autil.mk_has_size(tns, k2);
-            sz_smt = m_autil.mk_has_size(smt, k3);
-            propagate(sz1, sz_tms);
-            propagate(sz1, sz_tns);
-            propagate(sz2, sz_smt);
-            propagate(sz2, sz_tns);
-            propagate(sz1, mk_eq(k1 + k2, sz1->get_arg(1)));
-            propagate(sz2, mk_eq(k3 + k2, sz2->get_arg(1)));
-        }
-
-        expr_ref mk_subtract(expr* t, expr* s) {
-            expr_ref d(m_autil.mk_setminus(t, s), m);
-            m_rw(d);
-            return d;
-        }
-
-        expr_ref mk_intersect(expr* t, expr* s) {
-            expr_ref i(m_autil.mk_intersection(t, s), m);
-            m_rw(i);
-            return i;
-        }
-
-        void propagate(expr* assumption, expr* conseq) {
-            propagate(assumption, mk_literal(conseq));
-        }
-
-        void propagate(expr* assumption, literal conseq) {
-            mk_th_axiom(~mk_literal(assumption), conseq);
-        }
-
-        /**
-           Enforce V
-         */
-        lbool ensure_values_assigned() {            
-            lbool result = l_true;
-            for (auto const& kv : m_sizeof) {
-                app* k = kv.m_key;
-                sz_info& i = *kv.m_value;
-                if (is_leaf(&i)) {
-                    rational value;
-                    expr* sz  = k->get_arg(1);
-                    if (!m_arith_value.get_value(sz, value)) {
-                        return l_undef;
-                    }  
-                    literal lit = mk_eq(sz, m_arith.mk_int(value));
-                    if (lit != true_literal && is_true(lit)) {
-                        ctx().push_trail(value_trail<rational>(i.m_size, value));
-                        continue;
-                    }
-                    ctx().set_true_first_flag(lit.var());
-                    result = l_false;
-                }
-            }
-            return result;
-        }
-
-        /**
-           Enforce Ak,
-        */
-        lbool ensure_non_empty() {
-            for (auto const& kv : m_sizeof) {
-                sz_info& i = *kv.m_value;
-                app* set_sz = kv.m_key;
-                if (is_true(set_sz) && is_leaf(i) && i.m_selects.size() < i.m_size) {
-                    expr* set = set_sz->get_arg(0);
-                    expr_ref le(m_arith.mk_le(set_sz->get_arg(1), m_arith.mk_int(0)), m);
-                    literal le_lit = mk_literal(le);
-                    literal sz_lit = mk_literal(set_sz);
-                    for (unsigned k = i.m_selects.size(); rational(k) < i.m_size; ++k) {
-                        expr_ref idx = mk_index_skolem(set_sz, set, k);
-                        app_ref sel(mk_select(set, idx), m);
-                        mk_th_axiom(~sz_lit, le_lit, mk_literal(sel));
-                        TRACE(card, tout << idx << " " << sel << " " << i.m_size << "\n";);
-                    }
-                    return l_false;
-                }
-            }
-            return l_true;
-        }
-
-        // create skolem function that is injective on integers (ensures uniqueness).
-        expr_ref mk_index_skolem(app* sz, expr* a, unsigned n) {
-            func_decls fg;
-            sort* s = a->get_sort();
-            if (!m_index_skolems.find(s, fg)) {
-                sort* idx_sort = get_array_domain(s, 0);
-                sort* dom1[2] = { s, m_arith.mk_int() };
-                sort* dom2[1] = { idx_sort };
-                func_decl* f = m.mk_fresh_func_decl("to-index",   "", 2, dom1, idx_sort);
-                func_decl* g = m.mk_fresh_func_decl("from-index", "", 1, dom2, m_arith.mk_int());
-                fg = std::make_pair(f, g);
-                m_index_skolems.insert(s, fg);
-                m_pinned.push_back(f);
-                m_pinned.push_back(g);
-                m_pinned.push_back(s);
-            }
-            expr_ref nV(m_arith.mk_int(n), m);
-            expr_ref result(m.mk_app(fg.first, a, nV), m);   
-            expr_ref le(m_arith.mk_le(sz->get_arg(1), nV), m);
-            expr_ref fr(m.mk_app(fg.second, result), m);
-            // set-has-size(a, k) => k <= n or g(f(a,n)) = n 
-            mk_th_axiom(~mk_literal(sz), mk_literal(le), mk_eq(nV, fr));
-            return result;
-        }
-
-
-        /**
-           Enforce O
-        */
-        lbool ensure_no_overflow() {
-            for (auto const& kv : m_sizeof) {
-                if (is_true(kv.m_key) && is_leaf(kv.m_value)) {
-                    lbool r = ensure_no_overflow(kv.m_key, *kv.m_value);
-                    if (r != l_true) return r;
-                }
-            }
-            return l_true;
-        }
-
-        lbool ensure_no_overflow(app* sz, sz_info& info) {
-            SASSERT(!info.m_size.is_neg());
-            if (info.m_size < info.m_selects.size()) {
-                for (auto i = info.m_selects.begin(), e = info.m_selects.end(); i != e; ++i) {
-                    for (auto j = i; ++j != e; ) {
-                        if (ctx().assume_eq(i->m_key, j->m_key)) {
-                            return l_false;
-                        }
-                    } 
-                }                
-                // if all is exhausted, then add axiom: set-has-size(s, n) & s[indices] & all-diff(indices) => n >= |indices|
-                literal_vector lits;
-                lits.push_back(~mk_literal(sz));
-                for (auto const& kv : info.m_selects) {
-                    lits.push_back(~mk_literal(kv.m_value));
-                }
-                if (info.m_selects.size() > 1) {
-                    ptr_vector<expr> args;
-                    for (auto const& kv : info.m_selects) {
-                        args.push_back(kv.m_key->get_expr());
-                    }
-                    if (info.m_selects.size() == 2) {
-                        lits.push_back(mk_eq(args[0], args[1]));
-                    }
-                    else {
-                        expr_ref diff(m.mk_distinct_expanded(args.size(), args.data()), m);
-                        lits.push_back(~mk_literal(diff));
-                    }
-                }
-                expr_ref ge(m_arith.mk_ge(sz->get_arg(1), m_arith.mk_int(info.m_selects.size())), m);
-                lits.push_back(mk_literal(ge));
-                mk_th_axiom(lits.size(), lits.data());
-                return l_false;
-            }
-            return l_true;
-        }
-
-        class remove_sz : public trail {
-            ast_manager& m;
-            obj_map<app, sz_info*> & m_table;
-            app*                     m_obj;
-        public:
-            remove_sz(ast_manager& m, obj_map<app, sz_info*>& tab, app* t): m(m), m_table(tab), m_obj(t) { }
-            void undo() override { m.dec_ref(m_obj); dealloc(m_table[m_obj]); m_table.remove(m_obj); }
-        };
-
-        std::ostream& display(std::ostream& out) {
-            for (auto const& kv : m_sizeof) {
-                display(out << mk_pp(kv.m_key, m) << ": ", *kv.m_value);
-            }
-            return out;
-        }
-
-        std::ostream& display(std::ostream& out, sz_info& sz) {
-            return out << (sz.m_is_leaf ? "leaf": "") << " size: " << sz.m_size << " selects: " << sz.m_selects.size() << "\n";
-        }
-        
-    public:
-        imp(theory_array_full& th):
-            m(th.get_manager()),
-            th(th),
-            m_arith(m),
-            m_autil(m),
-            m_rw(m),
-            m_arith_value(m),
-            m_pinned(m)
-        {
-            context& ctx = th.get_context();
-            m_arith_value.init(&ctx);
-            m_max_set_enumeration = 4;
-        }
-
-        ~imp() {
-            reset();
-        }
-
-        void internalize_term(app* term) {
-            if (th.is_set_has_size(term)) {
-                internalize_size(term);
-            }
-            else if (th.is_set_card(term)) {
-                internalize_card(term);
-            }
-        }
-
-        /**
-         *  Size(S, n) => n >= 0, default(S) = false
-         */
-        void internalize_size(app* term) {
-            SASSERT(ctx().e_internalized(term));
-            literal lit = mk_literal(term);
-            expr* s = term->get_arg(0);
-            expr* n = term->get_arg(1);
-            mk_th_axiom(~lit, mk_literal(m_arith.mk_ge(n, m_arith.mk_int(0))));
-            sort_size const& sz = s->get_sort()->get_num_elements();
-            if (sz.is_infinite()) {
-                mk_th_axiom(~lit, mk_eq(th.mk_default(s), m.mk_false()));
-            }
-            else {
-                warning_msg("correct handling of finite domains is TBD");
-                // add upper bound on size of set.
-                // add case where default(S) = true, and add negative elements.
-            }
-            m_sizeof.insert(term, alloc(sz_info));
-            m_size_limit.insert(s, rational(2));
-            assert_size_limit(s, n);
-            m.inc_ref(term);
-            ctx().push_trail(remove_sz(m, m_sizeof, term));
-        }
-
-        /**
-           \brief whenever there is a cardinality function, it includes an axiom
-           that entails the set is finite.
-         */
-        void internalize_card(app* term) {
-            SASSERT(ctx().e_internalized(term));
-            app_ref has_size(m_autil.mk_has_size(term->get_arg(0), term), m);
-            literal lit = mk_literal(has_size);
-            ctx().assign(lit, nullptr);
-        }
-
-        lbool trace_call(char const* msg, lbool r) {
-            if (r != l_true) {
-                IF_VERBOSE(2, verbose_stream() << msg << "\n");
-            }
-            return r;
-        }
-
-        final_check_status final_check() {            
-            final_check_status st = m_arith_value.final_check();
-            if (st != FC_DONE) return st;
-            lbool r = trace_call("ensure_functional", ensure_functional());
-            if (r == l_true) update_indices();
-            if (r == l_true) r = trace_call("ensure_disjoint", ensure_disjoint());
-            if (r == l_true) r = trace_call("ensure_values_assigned", ensure_values_assigned());
-            if (r == l_true) r = trace_call("ensure_non_empty", ensure_non_empty());
-            if (r == l_true) r = trace_call("ensure_no_overflow", ensure_no_overflow());
-            CTRACE(card, r != l_true, display(tout););
-            switch (r) {
-            case l_true:
-                return FC_DONE;
-            case l_false:
-                return FC_CONTINUE;
-            case l_undef:
-                return FC_GIVEUP;
-            }
-            return FC_GIVEUP;
-        }
-
-        void init_model() {
-            for (auto const& kv : m_sizeof) {
-                sz_info& i = *kv.m_value;
-                app* sz = kv.m_key;
-                if (is_true(sz) && is_leaf(i) && rational(i.m_selects.size()) != i.m_size) {
-                    warning_msg("models for BAPA is TBD");
-                    break;
-                }
-            }
-        }
-
-        bool should_research(expr_ref_vector & unsat_core) {
-            expr* set, *sz;
-            for (auto & e : unsat_core) {
-                if (is_app(e) && is_size_limit(to_app(e), set, sz)) {
-                    inc_size_limit(set, sz);
-                    return true;
-                }
-            }
-            return false;
-        }
-
-        void inc_size_limit(expr* set, expr* sz) {
-            IF_VERBOSE(2, verbose_stream() << "inc value " << mk_pp(set, m) << "\n");
-            m_size_limit[set] *= rational(2);
-            assert_size_limit(set, sz);
-        }
-        
-        bool is_size_limit(app* e, expr*& set, expr*& sz) {
-            func_decl* d = nullptr;
-            if (e->get_num_args() > 0 && m_size_limit_sort2skolems.find(e->get_arg(0)->get_sort(), d) && d == e->get_decl()) {
-                set = e->get_arg(0);
-                sz  = e->get_arg(1);
-                return true;
-            }
-            else {
-                return false;
-            }
-        }
-
-        // has-size(s,n) & size-limit(s, n, k)  => n <= k
-
-        app_ref mk_size_limit(expr* set, expr* sz) {
-            func_decl* sk = nullptr;
-            sort* s = set->get_sort();
-            if (!m_size_limit_sort2skolems.find(s, sk)) {
-                sort* dom[3] = { s, m_arith.mk_int(), m_arith.mk_int() };
-                sk = m.mk_fresh_func_decl("value-limit", "", 3, dom, m.mk_bool_sort());
-                m_pinned.push_back(sk);                    
-                m_size_limit_sort2skolems.insert(s, sk);
-            }             
-            return app_ref(m.mk_app(sk, set, sz, m_arith.mk_int(m_size_limit[set])), m);            
-        }
-
-        void assert_size_limit(expr* set, expr* sz) {
-            app_ref set_sz(m_autil.mk_has_size(set, sz), m);
-            app_ref lim(m_arith.mk_int(m_size_limit[set]), m);
-            app_ref size_limit = mk_size_limit(set, sz);
-            mk_th_axiom(~mk_literal(set_sz), ~mk_literal(size_limit), mk_literal(m_arith.mk_le(sz, lim)));
-        }
-
-        void add_theory_assumptions(expr_ref_vector & assumptions) {
-            for (auto const& kv : m_sizeof) {
-                expr* set = kv.m_key->get_arg(0);
-                expr* sz =  kv.m_key->get_arg(1);
-                assumptions.push_back(mk_size_limit(set, sz));
-            }            
-            TRACE(card, tout << "ASSUMPTIONS: " << assumptions << "\n";);
-        }
-    
-    };
-
-    theory_array_bapa::theory_array_bapa(theory_array_full& th) { m_imp = alloc(imp, th);  }
-
-    theory_array_bapa::~theory_array_bapa() { dealloc(m_imp); }
-
-    void theory_array_bapa::internalize_term(app* term) { m_imp->internalize_term(term); }
-
-    final_check_status theory_array_bapa::final_check() { return m_imp->final_check(); }
-
-    void theory_array_bapa::init_model() { m_imp->init_model(); }
-
-    bool theory_array_bapa::should_research(expr_ref_vector & unsat_core) { return m_imp->should_research(unsat_core); }
-
-    void theory_array_bapa::add_theory_assumptions(expr_ref_vector & assumptions) { m_imp->add_theory_assumptions(assumptions); }
-
-}
diff --git a/src/smt/theory_array_bapa.h b/src/smt/theory_array_bapa.h
deleted file mode 100644
index 98fcdd148..000000000
--- a/src/smt/theory_array_bapa.h
+++ /dev/null
@@ -1,43 +0,0 @@
-/*++
-Copyright (c) 2019 Microsoft Corporation
-
-Module Name:
-
-    theory_array_bapa.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Nikolaj Bjorner 2019-04-13
-
-Revision History:
-
---*/
-#pragma once
-
-#include "ast/ast.h"
-#include "smt/smt_theory.h"
-
-namespace smt {
-
-    class theory_array_full;
-
-    class theory_array_bapa {
-        class imp;
-        imp* m_imp;
-    public:
-        theory_array_bapa(theory_array_full& th);
-        ~theory_array_bapa();
-        void internalize_term(app* term);
-        final_check_status final_check();
-        void init_model();
-        bool should_research(expr_ref_vector & unsat_core);
-        void add_theory_assumptions(expr_ref_vector & assumptions);
-    };
-
-};
-
-
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index 9d1775a3b..6e04c0290 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -681,7 +681,6 @@ namespace smt {
         collect_defaults();
         collect_selects();
         propagate_selects();
-        if (m_bapa) m_bapa->init_model();
     }
 
     /**
@@ -699,7 +698,7 @@ namespace smt {
             if (!ctx.is_relevant(n))
                 continue;
             
-            if (is_store(n) || is_const(n) || is_default(n) || is_set_has_size(n))
+            if (is_store(n) || is_const(n) || is_default(n))
                 return false;
         }
         return true;
diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h
index 58d143ff1..9a6a6a173 100644
--- a/src/smt/theory_array_base.h
+++ b/src/smt/theory_array_base.h
@@ -19,14 +19,12 @@ Revision History:
 #pragma once
 
 #include "smt/smt_theory.h"
-#include "smt/theory_array_bapa.h"
 #include "ast/array_decl_plugin.h"
 #include "model/array_factory.h"
 
 namespace smt {
 
     class theory_array_base : public theory {
-        friend class theory_array_bapa;
     protected:
         bool m_found_unsupported_op;
         unsigned m_array_weak_head;
@@ -47,8 +45,6 @@ namespace smt {
         bool is_as_array(app const * n) const { return n->is_app_of(get_id(), OP_AS_ARRAY); }
         bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); }
         bool is_array_sort(app const* n) const { return is_array_sort(n->get_sort()); }
-        bool is_set_has_size(app const* n) const { return n->is_app_of(get_id(), OP_SET_HAS_SIZE); }
-        bool is_set_card(app const* n) const { return n->is_app_of(get_id(), OP_SET_CARD); }
 
         bool is_store(enode const * n) const { return is_store(n->get_expr()); }
         bool is_map(enode const* n) const { return is_map(n->get_expr()); }
@@ -57,8 +53,6 @@ namespace smt {
         bool is_as_array(enode const * n) const { return is_as_array(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_expr()); }
-        bool is_set_has_size(enode const* n) const { return is_set_has_size(n->get_expr()); }
-        bool is_set_carde(enode const* n) const { return is_set_card(n->get_expr()); }
         bool is_select_arg(enode* r);
 
         app * mk_select(unsigned num_args, expr * const * args);
@@ -74,7 +68,6 @@ namespace smt {
         enode_pair_vector                   m_axiom2_todo;
         enode_pair_vector                   m_extensionality_todo;
         enode_pair_vector                   m_congruent_todo;
-        scoped_ptr<theory_array_bapa>       m_bapa;
 
         void assert_axiom(unsigned num_lits, literal * lits);
         void assert_axiom(literal l1, literal l2);
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index f92f98169..941112a4b 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -271,7 +271,7 @@ namespace smt {
             return theory_array::internalize_term(n);
         }
 
-        if (!is_const(n) && !is_default(n)  && !is_map(n) && !is_as_array(n) && !is_set_has_size(n) && !is_set_card(n)) {
+        if (!is_const(n) && !is_default(n)  && !is_map(n) && !is_as_array(n)) {
             if (!is_array_ext(n))
                 found_unsupported_op(n);
             return false;
@@ -295,12 +295,6 @@ namespace smt {
                 mk_var(arg0);
             }
         }
-        else if (is_set_has_size(n) || is_set_card(n)) {
-            if (!m_bapa) {
-                m_bapa = alloc(theory_array_bapa, *this);
-            }
-            m_bapa->internalize_term(n);
-        }
 
         enode* node = ctx.get_enode(n);
         if (!is_attached_to_var(node)) {
@@ -449,11 +443,10 @@ namespace smt {
     }
 
     bool theory_array_full::should_research(expr_ref_vector & unsat_core) {
-        return m_bapa && m_bapa->should_research(unsat_core);
+        return false;
     }
 
     void theory_array_full::add_theory_assumptions(expr_ref_vector & assumptions) {
-        if (m_bapa) m_bapa->add_theory_assumptions(assumptions);
     }
        
     //
@@ -814,9 +807,6 @@ namespace smt {
                 }
             }
         }
-        if (r == FC_DONE && m_bapa) {
-            r = m_bapa->final_check();
-        }
         bool should_giveup = m_found_unsupported_op || has_propagate_up_trail() || has_non_beta_as_array();
         if (r == FC_DONE && should_giveup)
             r = FC_GIVEUP;
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 7b0afd7e1..f1749df4f 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1450,7 +1450,7 @@ namespace smt {
                                    << num_scopes << " = " << (ctx.get_scope_level() - num_scopes) << "\n"););
     }
 
-    final_check_status theory_bv::final_check_eh() {
+    final_check_status theory_bv::final_check_eh(unsigned level) {
         SASSERT(check_invariant());
         if (m_approximates_large_bvs) {
             return FC_GIVEUP;
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index f46a9ce70..5ba10442d 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -244,7 +244,7 @@ namespace smt {
         void relevant_eh(app * n) override;
         void push_scope_eh() override;
         void pop_scope_eh(unsigned num_scopes) override;
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         void reset_eh() override;
         bool include_func_interp(func_decl* f) override;
         svector<theory_var>   m_merge_aux[2]; //!< auxiliary vector used in merge_zero_one_bits
diff --git a/src/smt/theory_char.h b/src/smt/theory_char.h
index 8be817cda..a4078a74e 100644
--- a/src/smt/theory_char.h
+++ b/src/smt/theory_char.h
@@ -75,7 +75,7 @@ namespace smt {
         bool internalize_atom(app * atom, bool gate_ctx) override;
         bool internalize_term(app * term) override;
         void display(std::ostream& out) const override {}
-        final_check_status final_check_eh() override { return final_check() ? FC_DONE : FC_CONTINUE; }
+        final_check_status final_check_eh(unsigned) override { return final_check() ? FC_DONE : FC_CONTINUE; }
         void init_model(model_generator & mg) override;
         model_value_proc * mk_value(enode * n, model_generator & mg) override;
         void collect_statistics(::statistics& st) const override;
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index d541781ea..b4a3ed4db 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -476,7 +476,7 @@ namespace smt {
         SASSERT(m_find.get_num_vars() == get_num_vars());
     }
 
-    final_check_status theory_datatype::final_check_eh() {
+    final_check_status theory_datatype::final_check_eh(unsigned level) {
         force_push();
         int num_vars = get_num_vars();
         final_check_status r = FC_DONE;
diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h
index 8a61ce5bd..dfc06ae69 100644
--- a/src/smt/theory_datatype.h
+++ b/src/smt/theory_datatype.h
@@ -126,7 +126,7 @@ namespace smt {
         void relevant_eh(app * n) override;
         void push_scope_eh() override;
         void pop_scope_eh(unsigned num_scopes) override;
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         void reset_eh() override;
         void restart_eh() override { m_util.reset(); }
         bool is_shared(theory_var v) const override;
diff --git a/src/smt/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h
index 45ec93c08..8c2d62aa9 100644
--- a/src/smt/theory_dense_diff_logic.h
+++ b/src/smt/theory_dense_diff_logic.h
@@ -230,7 +230,7 @@ namespace smt {
         
         void restart_eh() override;
         void init_search_eh() override;
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         
         bool can_propagate() override;
         void propagate() override;
diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h
index 96ac78d99..5c351528e 100644
--- a/src/smt/theory_dense_diff_logic_def.h
+++ b/src/smt/theory_dense_diff_logic_def.h
@@ -387,7 +387,7 @@ namespace smt {
     }
 
     template<typename Ext>
-    final_check_status theory_dense_diff_logic<Ext>::final_check_eh() {
+    final_check_status theory_dense_diff_logic<Ext>::final_check_eh(unsigned level) {
         init_model();
         if (assume_eqs(m_var_value_table))
             return FC_CONTINUE;
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 9a818bc10..720cdb9bb 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -269,7 +269,7 @@ namespace smt {
             m_arith_eq_adapter.init_search_eh();
         }
 
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
 
         bool is_shared(theory_var v) const override {
             return false;
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 18ac30fbc..30251092c 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -368,7 +368,7 @@ void theory_diff_logic<Ext>::pop_scope_eh(unsigned num_scopes) {
 }
 
 template<typename Ext>
-final_check_status theory_diff_logic<Ext>::final_check_eh() {
+final_check_status theory_diff_logic<Ext>::final_check_eh(unsigned level) {
 
     if (can_propagate()) {
         propagate_core();
diff --git a/src/smt/theory_dummy.cpp b/src/smt/theory_dummy.cpp
index 097d7f1ad..7f8af5a9d 100644
--- a/src/smt/theory_dummy.cpp
+++ b/src/smt/theory_dummy.cpp
@@ -62,7 +62,7 @@ namespace smt {
         theory::reset_eh();
     }
 
-    final_check_status theory_dummy::final_check_eh() {
+    final_check_status theory_dummy::final_check_eh(unsigned) {
         return m_theory_exprs ? FC_GIVEUP : FC_DONE;
     }
 
diff --git a/src/smt/theory_dummy.h b/src/smt/theory_dummy.h
index 817d1fda1..de77f292d 100644
--- a/src/smt/theory_dummy.h
+++ b/src/smt/theory_dummy.h
@@ -38,7 +38,7 @@ namespace smt {
         bool use_diseqs() const override;
         void new_diseq_eh(theory_var v1, theory_var v2) override;
         void reset_eh() override;
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         bool build_models() const override {
             return false;
         }
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index f7be2be55..48885d80c 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -501,7 +501,7 @@ namespace smt {
         theory::reset_eh();
     }
 
-    final_check_status theory_fpa::final_check_eh() {
+    final_check_status theory_fpa::final_check_eh(unsigned level) {
         TRACE(t_fpa, tout << "final_check_eh\n";);
         SASSERT(m_converter.m_extra_assertions.empty());
         return FC_DONE;
diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h
index 262a239dd..badce4e2a 100644
--- a/src/smt/theory_fpa.h
+++ b/src/smt/theory_fpa.h
@@ -89,7 +89,7 @@ namespace smt {
         bool                      m_is_initialized;
         obj_hashtable<func_decl>  m_is_added_to_model;
 
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         bool internalize_atom(app * atom, bool gate_ctx) override;
         bool internalize_term(app * term) override;
         void apply_sort_cnstr(enode * n, sort * s) override;
diff --git a/src/smt/theory_intblast.cpp b/src/smt/theory_intblast.cpp
index c6c94958e..d238ae60d 100644
--- a/src/smt/theory_intblast.cpp
+++ b/src/smt/theory_intblast.cpp
@@ -38,7 +38,7 @@ namespace smt {
     
     theory_intblast::~theory_intblast() {}
         
-    final_check_status theory_intblast::final_check_eh() {
+    final_check_status theory_intblast::final_check_eh(unsigned) {
         for (auto e : m_translator.bv2int()) {
             auto* n = ctx.get_enode(e);
             auto* r1 = n->get_arg(0)->get_root();
diff --git a/src/smt/theory_intblast.h b/src/smt/theory_intblast.h
index b822593b7..1a2e2c78d 100644
--- a/src/smt/theory_intblast.h
+++ b/src/smt/theory_intblast.h
@@ -54,7 +54,7 @@ namespace smt {
 
         char const* get_name() const override { return "bv-intblast"; }
         smt::theory* mk_fresh(context* new_ctx) override { return alloc(theory_intblast, *new_ctx); }
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         void display(std::ostream& out) const override {}
         bool can_propagate() override;
         void propagate() override;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 2c58400ba..3ec930433 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1630,7 +1630,7 @@ public:
         return FC_GIVEUP;
     }
     
-    final_check_status final_check_eh() {
+    final_check_status final_check_eh(unsigned level) {
         if (propagate_core())
             return FC_CONTINUE;
         m_model_is_initialized = false;
@@ -1658,7 +1658,7 @@ public:
                 break;
             }
 
-            switch (check_nla()) {
+            switch (check_nla(level)) {
             case FC_DONE:
                 break;
             case FC_CONTINUE:
@@ -2047,11 +2047,11 @@ public:
         ctx().set_true_first_flag(lit.var());
     }
     
-    final_check_status check_nla_continue() {
+    final_check_status check_nla_continue(unsigned level) {
 #if Z3DEBUG
         flet f(lp().validate_blocker(), true);
 #endif
-        lbool r = m_nla->check();
+        lbool r = m_nla->check(level);
         switch (r) {
         case l_false:
             add_lemmas();
@@ -2063,7 +2063,7 @@ public:
         }
     }
 
-    final_check_status check_nla() {
+    final_check_status check_nla(unsigned level) {
         // TODO - enable or remove if found useful internals are corrected:
         // lp::lar_solver::scoped_auxiliary _sa(lp()); // new atoms are auxilairy and are not used in nra_solver
         if (!m.inc()) {
@@ -2075,7 +2075,7 @@ public:
             return FC_DONE;        
         if (!m_nla->need_check()) 
             return FC_DONE;
-        return check_nla_continue();
+        return check_nla_continue(level);
     }
 
     /**
@@ -3900,6 +3900,7 @@ public:
     }
 
     theory_lra::inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) {
+        unsigned level = 2;
         lp::impq term_max;
         lp::lp_status st;
         lpvar vi = 0;
@@ -3926,7 +3927,7 @@ public:
                 lp().restore_x();
             }
             if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) {
-                switch (check_nla()) {
+                switch (check_nla(level)) {
                 case FC_DONE:
                     st = lp::lp_status::FEASIBLE;
                     break;
@@ -4286,8 +4287,8 @@ void theory_lra::relevant_eh(app* e) {
 void theory_lra::init_search_eh() {
     m_imp->init_search_eh();
 }
-final_check_status theory_lra::final_check_eh() {
-    return m_imp->final_check_eh();
+final_check_status theory_lra::final_check_eh(unsigned level) {
+    return m_imp->final_check_eh(level);
 }
 bool theory_lra::is_shared(theory_var v) const {
     return m_imp->is_shared(v);
diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h
index 1624bab0a..8804d52eb 100644
--- a/src/smt/theory_lra.h
+++ b/src/smt/theory_lra.h
@@ -63,7 +63,11 @@ namespace smt {
 
         void init_search_eh() override;
 
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
+
+        unsigned num_final_check_levels() const override {
+            return 2;
+        }
 
         bool is_shared(theory_var v) const override;
     
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 32670bd63..196f370c4 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -985,7 +985,7 @@ namespace smt {
         UNREACHABLE();
     }
     
-    final_check_status theory_pb::final_check_eh() {
+    final_check_status theory_pb::final_check_eh(unsigned level) {
         TRACE(pb, display(tout););
         DEBUG_CODE(validate_final_check(););
         return FC_DONE;
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index 353f4aeeb..96e1c96bd 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -417,7 +417,7 @@ namespace smt {
         void new_diseq_eh(theory_var v1, theory_var v2) override { }
         bool use_diseqs() const override { return false; }
         bool build_models() const override { return false; }
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         void reset_eh() override;
         void assign_eh(bool_var v, bool is_true) override;
         void init_search_eh() override;
diff --git a/src/smt/theory_polymorphism.h b/src/smt/theory_polymorphism.h
index 4c64a0a9c..8fd88c69b 100644
--- a/src/smt/theory_polymorphism.h
+++ b/src/smt/theory_polymorphism.h
@@ -66,7 +66,7 @@ namespace smt {
             ctx.internalize_assertions();
         }
 
-        final_check_status final_check_eh() override {
+        final_check_status final_check_eh(unsigned) override {
             if (m_inst.pending()) 
                 ctx.assign(~mk_literal(m_assumption), nullptr);
             return FC_DONE;
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index 4247dcb2a..9f5d54d43 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -405,7 +405,7 @@ namespace smt {
         ctx.mk_th_axiom(get_id(), clause);
     }
     
-    final_check_status theory_recfun::final_check_eh() {
+    final_check_status theory_recfun::final_check_eh(unsigned level) {
         if (can_propagate()) {
             TRACEFN("final\n");
             propagate();
diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h
index 7ca25f917..25e77a469 100644
--- a/src/smt/theory_recfun.h
+++ b/src/smt/theory_recfun.h
@@ -92,7 +92,7 @@ namespace smt {
         void reset_eh() override;
         void relevant_eh(app * n) override;
         char const * get_name() const override;
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         void assign_eh(bool_var v, bool is_true) override;
         void push_scope_eh() override;
         void pop_scope_eh(unsigned num_scopes) override;
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 2a70f25d8..36caebf0a 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -318,7 +318,7 @@ struct scoped_enable_trace {
     }
 };
 
-final_check_status theory_seq::final_check_eh() {
+final_check_status theory_seq::final_check_eh(unsigned level) {
     if (!m_has_seq) {
         return FC_DONE;
     }
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index a6539bded..093cd04b4 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -379,7 +379,7 @@ namespace smt {
         obj_hashtable<expr>            m_fixed;            // string variables that are fixed length.
         obj_hashtable<expr>            m_is_digit;         // expressions that have been constrained to be digits
 
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         bool internalize_atom(app* atom, bool) override;
         bool internalize_term(app*) override;
         void internalize_eq_eh(app * atom, bool_var v) override;
diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h
index 5562ba01b..9571f46b7 100644
--- a/src/smt/theory_seq_empty.h
+++ b/src/smt/theory_seq_empty.h
@@ -27,7 +27,7 @@ namespace smt {
 
     class theory_seq_empty : public theory {
         bool m_used;
-        final_check_status final_check_eh() override { return m_used?FC_GIVEUP:FC_DONE; }
+        final_check_status final_check_eh(unsigned) override { return m_used?FC_GIVEUP:FC_DONE; }
         bool internalize_atom(app*, bool) override { if (!m_used) { get_context().push_trail(value_trail<bool>(m_used)); m_used = true; } return false; }
         bool internalize_term(app*) override { return internalize_atom(nullptr,false);  }
         void new_eq_eh(theory_var, theory_var) override { }
diff --git a/src/smt/theory_sls.cpp b/src/smt/theory_sls.cpp
index 0ce329046..8551661c2 100644
--- a/src/smt/theory_sls.cpp
+++ b/src/smt/theory_sls.cpp
@@ -241,7 +241,7 @@ namespace smt {
         }
     }
 
-    final_check_status theory_sls::final_check_eh() {
+    final_check_status theory_sls::final_check_eh(unsigned) {
         if (!m_smt_plugin)
             return FC_DONE;
         ++m_after_resolve_decide_count;
diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h
index b0407cbdb..e8d9b22b4 100644
--- a/src/smt/theory_sls.h
+++ b/src/smt/theory_sls.h
@@ -118,7 +118,7 @@ namespace smt {
         void new_eq_eh(theory_var v1, theory_var v2) override {}
         void new_diseq_eh(theory_var v1, theory_var v2) override {}
         void restart_eh() override;
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
 
         // sls::smt_context interface
         ast_manager& get_manager() override { return m; }
diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp
index 9daf3ab2e..aec069a02 100644
--- a/src/smt/theory_special_relations.cpp
+++ b/src/smt/theory_special_relations.cpp
@@ -186,7 +186,7 @@ namespace smt {
         }
     }
 
-    final_check_status theory_special_relations::final_check_eh() {
+    final_check_status theory_special_relations::final_check_eh(unsigned) {
         TRACE(special_relations, tout << "\n";);
         for (auto const& kv : m_relations) {
             lbool r = final_check(*kv.m_value);
diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h
index 65ce17907..085ecfe74 100644
--- a/src/smt/theory_special_relations.h
+++ b/src/smt/theory_special_relations.h
@@ -187,7 +187,7 @@ namespace smt {
         void new_diseq_eh(theory_var v1, theory_var v2) override {}
         bool use_diseqs() const override { return false; }
         bool build_models() const override { return true; }
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         void reset_eh() override;
         void assign_eh(bool_var v, bool is_true) override;
         void init_search_eh() override {}
diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index d8adbdb70..a2eaeb9a8 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -157,7 +157,7 @@ theory * theory_user_propagator::mk_fresh(context * new_ctx) {
     return th;
 }
 
-final_check_status theory_user_propagator::final_check_eh() {
+final_check_status theory_user_propagator::final_check_eh(unsigned level) {
     if (!(bool)m_final_eh)
         return FC_DONE;
     force_push();
diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h
index 5e8d3878c..439ffdb7e 100644
--- a/src/smt/theory_user_propagator.h
+++ b/src/smt/theory_user_propagator.h
@@ -152,7 +152,7 @@ namespace smt {
         void new_diseq_eh(theory_var v1, theory_var v2) override { if (m_diseq_eh) force_push(), m_diseq_eh(m_user_context, this, var2expr(v1), var2expr(v2)); }
         bool use_diseqs() const override { return ((bool)m_diseq_eh); }
         bool build_models() const override { return false; }
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned) override;
         void reset_eh() override {}
         void assign_eh(bool_var v, bool is_true) override { }
         void init_search_eh() override {}
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index 99344eb31..a917910e9 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -245,7 +245,7 @@ namespace smt {
             m_arith_eq_adapter.init_search_eh();
         }
 
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned level) override;
 
         bool is_shared(th_var v) const override {
             return false;
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index 5f056784f..9086f13aa 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -394,7 +394,7 @@ namespace smt {
     }
     
     template<typename Ext>
-    final_check_status theory_utvpi<Ext>::final_check_eh() {
+    final_check_status theory_utvpi<Ext>::final_check_eh(unsigned level) {
         SASSERT(is_consistent());
         if (can_propagate()) {
             propagate();
diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp
index 13e69da5d..fdc1ebfb2 100644
--- a/src/smt/theory_wmaxsat.cpp
+++ b/src/smt/theory_wmaxsat.cpp
@@ -176,7 +176,7 @@ namespace smt {
         }
     }
 
-    final_check_status theory_wmaxsat::final_check_eh() {
+    final_check_status theory_wmaxsat::final_check_eh(unsigned level) {
         if (m_normalize) normalize();
         TRACE(opt, tout << "cost: " << m_zcost << " min cost: " << m_zmin_cost << "\n";);
         return FC_DONE;
diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h
index 9cac6b96b..65461eb70 100644
--- a/src/smt/theory_wmaxsat.h
+++ b/src/smt/theory_wmaxsat.h
@@ -83,7 +83,7 @@ namespace smt {
 
         void init_search_eh() override;
         void assign_eh(bool_var v, bool is_true) override;
-        final_check_status final_check_eh() override;
+        final_check_status final_check_eh(unsigned level) override;
         bool use_diseqs() const override {
             return false;
         }