diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index c56066827..532affef7 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1076,7 +1076,6 @@ void cmd_context::reset(bool finalize) {
     reset_macros();
     reset_func_decls();
     restore_assertions(0);
-    restore_assumptions(0);
     if (m_solver)
         m_solver->reset();
     m_pp_env = 0;
@@ -1108,6 +1107,8 @@ void cmd_context::assert_expr(expr * t) {
     m_check_sat_result = 0;
     m().inc_ref(t);
     m_assertions.push_back(t);
+    if (m_produce_unsat_cores)
+        m_assertion_names.push_back(0);
     if (m_solver)
         m_solver->assert_expr(t);
 }
@@ -1119,11 +1120,14 @@ void cmd_context::assert_expr(symbol const & name, expr * t) {
         assert_expr(t);
         return;
     }
-    app * proxy  = m().mk_const(name, m().mk_bool_sort());
-    expr * new_t = m().mk_implies(proxy, t);
-    m().inc_ref(proxy);
-    m_assumptions.push_back(proxy);
-    assert_expr(new_t);
+    m_check_sat_result = 0;
+    m().inc_ref(t);
+    m_assertions.push_back(t);
+    expr * ans  = m().mk_const(name, m().mk_bool_sort());
+    m().inc_ref(ans);
+    m_assertion_names.push_back(ans);
+    if (m_solver)
+        m_solver->assert_expr(t, ans);
 }
 
 void cmd_context::push() {
@@ -1137,7 +1141,6 @@ void cmd_context::push() {
     s.m_macros_stack_lim       = m_macros_stack.size();
     s.m_aux_pdecls_lim         = m_aux_pdecls.size();
     s.m_assertions_lim         = m_assertions.size();
-    s.m_assumptions_lim        = m_assumptions.size();
     if (m_solver) 
         m_solver->push();
 }
@@ -1200,29 +1203,25 @@ void cmd_context::restore_aux_pdecls(unsigned old_sz) {
     m_aux_pdecls.shrink(old_sz);
 }
 
+static void restore(ast_manager & m, ptr_vector<expr> & c, unsigned old_sz) {
+    ptr_vector<expr>::iterator it  = c.begin() + old_sz;
+    ptr_vector<expr>::iterator end = c.end();
+    for (; it != end; ++it) {
+        m.dec_ref(*it);
+    }
+    c.shrink(old_sz);
+}
+
 void cmd_context::restore_assertions(unsigned old_sz) {
     SASSERT(old_sz <= m_assertions.size());
     SASSERT(!m_interactive_mode || m_assertions.size() == m_assertion_strings.size());
-    ptr_vector<expr>::iterator it  = m_assertions.begin() + old_sz;
-    ptr_vector<expr>::iterator end = m_assertions.end();
-    for (; it != end; ++it) {
-        m().dec_ref(*it);
-    }
-    m_assertions.shrink(old_sz);
+    restore(m(), m_assertions, old_sz);
+    if (m_produce_unsat_cores)
+        restore(m(), m_assertion_names, old_sz);
     if (m_interactive_mode)
         m_assertion_strings.shrink(old_sz);
 }
 
-void cmd_context::restore_assumptions(unsigned old_sz) {
-    SASSERT(old_sz <= m_assumptions.size());
-    ptr_vector<expr>::iterator it  = m_assumptions.begin() + old_sz;
-    ptr_vector<expr>::iterator end = m_assumptions.end();
-    for (; it != end; ++it) {
-        m().dec_ref(*it);
-    }
-    m_assumptions.shrink(old_sz);
-}
-
 void cmd_context::pop(unsigned n) {
     m_check_sat_result = 0;
     if (n == 0)
@@ -1240,7 +1239,6 @@ void cmd_context::pop(unsigned n) {
     restore_macros(s.m_macros_stack_lim);
     restore_aux_pdecls(s.m_aux_pdecls_lim);
     restore_assertions(s.m_assertions_lim);
-    restore_assumptions(s.m_assumptions_lim);
     m_scopes.shrink(new_lvl);
 }
 
@@ -1266,11 +1264,9 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         scoped_watch sw(*this);
         cancel_eh<solver> eh(*m_solver);
         scoped_ctrl_c ctrlc(eh);
-        unsigned old_sz = m_assumptions.size();
-        m_assumptions.append(num_assumptions, assumptions);
         lbool r;
         try {
-            r = m_solver->check_sat(m_assumptions.size(), m_assumptions.c_ptr());
+            r = m_solver->check_sat(num_assumptions, assumptions);
         }
         catch (z3_error & ex) {
             throw ex;
@@ -1278,7 +1274,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         catch (z3_exception & ex) {
             throw cmd_exception(ex.msg());
         }
-        m_assumptions.shrink(old_sz);
         m_solver->set_status(r);
         display_sat_result(r);
         validate_check_sat_result(r);
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 9296f0735..73e212da1 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -175,16 +175,15 @@ protected:
     ptr_vector<pdecl>            m_aux_pdecls;
     ptr_vector<expr>             m_assertions;
     vector<std::string>          m_assertion_strings;
-    ptr_vector<expr>             m_assumptions; // for unsat-core extraction
+    ptr_vector<expr>             m_assertion_names; // named assertions are represented using boolean variables.
 
     struct scope {
         unsigned m_func_decls_stack_lim;
         unsigned m_psort_decls_stack_lim;
         unsigned m_macros_stack_lim;
         unsigned m_aux_pdecls_lim;
-        // only m_assertions_lim and m_assumptions_lim are relevant when m_global_decls = true
+        // only m_assertions_lim is relevant when m_global_decls = true
         unsigned m_assertions_lim;
-        unsigned m_assumptions_lim;
     };
 
     svector<scope>               m_scopes;
@@ -225,7 +224,6 @@ protected:
     void restore_macros(unsigned old_sz);
     void restore_aux_pdecls(unsigned old_sz);
     void restore_assertions(unsigned old_sz);
-    void restore_assumptions(unsigned old_sz);
 
     void erase_func_decl_core(symbol const & s, func_decl * f);
     void erase_psort_decl_core(symbol const & s);
@@ -369,8 +367,8 @@ public:
     ptr_vector<expr>::const_iterator begin_assertions() const { return m_assertions.begin(); }
     ptr_vector<expr>::const_iterator end_assertions() const { return m_assertions.end(); }
 
-    ptr_vector<expr>::const_iterator begin_assumptions() const { return m_assumptions.begin(); }
-    ptr_vector<expr>::const_iterator end_assumptions() const { return m_assumptions.end(); }
+    ptr_vector<expr>::const_iterator begin_assertion_names() const { return m_assertion_names.begin(); }
+    ptr_vector<expr>::const_iterator end_assertion_names() const { return m_assertion_names.end(); }
 
     /**
        \brief Hack: consume assertions if there are no scopes.
@@ -380,7 +378,6 @@ public:
         if (num_scopes() > 0)
             return false;
         restore_assertions(0);
-        restore_assumptions(0);
         return true;
     }
 
diff --git a/src/cmd_context/cmd_context_to_goal.cpp b/src/cmd_context/cmd_context_to_goal.cpp
index 21f8445d5..26cb2766b 100644
--- a/src/cmd_context/cmd_context_to_goal.cpp
+++ b/src/cmd_context/cmd_context_to_goal.cpp
@@ -27,20 +27,22 @@ void assert_exprs_from(cmd_context const & ctx, goal & t) {
         throw cmd_exception("Frontend does not support simultaneous generation of proofs and unsat cores");
     ast_manager & m = t.m();
     bool proofs_enabled = t.proofs_enabled();
-    ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
-    ptr_vector<expr>::const_iterator end = ctx.end_assertions();
-    for (; it != end; ++it) {
-        t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : 0, 0);
-    }
     if (ctx.produce_unsat_cores()) {
-        SASSERT(!ctx.produce_proofs());
-        it  = ctx.begin_assumptions();
-        end = ctx.end_assumptions();
-        for (; it != end; ++it) {
-            t.assert_expr(*it, 0, m.mk_leaf(*it));
+        ptr_vector<expr>::const_iterator it   = ctx.begin_assertions();
+        ptr_vector<expr>::const_iterator end  = ctx.end_assertions();
+        ptr_vector<expr>::const_iterator it2  = ctx.begin_assertion_names();
+        ptr_vector<expr>::const_iterator end2 = ctx.end_assertion_names();
+        SASSERT(end - it == end2 - it2);
+        for (; it != end; ++it, ++it2) {
+            t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : 0, m.mk_leaf(*it2));
         }
     }
     else {
-        SASSERT(ctx.begin_assumptions() == ctx.end_assumptions());
+        ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
+        ptr_vector<expr>::const_iterator end = ctx.end_assertions();
+        for (; it != end; ++it) {
+            t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : 0, 0);
+        }
+        SASSERT(ctx.begin_assertion_names() == ctx.end_assertion_names());
     }
 }
diff --git a/src/parsers/smt/smtlib_solver.cpp b/src/parsers/smt/smtlib_solver.cpp
index 77c2455dc..dd54de350 100644
--- a/src/parsers/smt/smtlib_solver.cpp
+++ b/src/parsers/smt/smtlib_solver.cpp
@@ -83,7 +83,7 @@ namespace smtlib {
             benchmark.add_formula(m_ast_manager.mk_true());
         }
         m_ctx = alloc(cmd_context, &m_params, true, &m_ast_manager, benchmark.get_logic());
-        m_ctx->set_solver(mk_smt_strategic_solver(*m_ctx));
+        m_ctx->set_solver(mk_smt_strategic_solver(false));
         theory::expr_iterator fit  = benchmark.begin_formulas();
         theory::expr_iterator fend = benchmark.end_formulas();
         for (; fit != fend; ++fit)
diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
index 6711158fd..08b070183 100644
--- a/src/shell/smtlib_frontend.cpp
+++ b/src/shell/smtlib_frontend.cpp
@@ -106,7 +106,7 @@ unsigned read_smtlib2_commands(char const* file_name, front_end_params& front_en
         ctx.set_solver(s);
     }
     else {
-        solver * s = mk_smt_strategic_solver(ctx);
+        solver * s = mk_smt_strategic_solver(false);
         ctx.set_solver(s);
     }
     install_dl_cmds(ctx);
diff --git a/src/smt/ni_solver.cpp b/src/smt/ni_solver.cpp
deleted file mode 100644
index 692e1b042..000000000
--- a/src/smt/ni_solver.cpp
+++ /dev/null
@@ -1,225 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
-    ni_solver.cpp
-
-Abstract:
-    Wrappers for smt::kernel that are non-incremental & (quasi-incremental).
-
-Author:
-
-    Leonardo (leonardo) 2011-03-30
-
-Notes:
-
---*/
-#include"ni_solver.h"
-#include"smt_kernel.h"
-#include"cmd_context.h"
-#include"solver_na2as.h"
-
-class ni_smt_solver : public solver_na2as {
-protected:
-    cmd_context &       m_cmd_ctx;
-    smt::kernel *       m_context;
-    progress_callback * m_callback;
-public:
-    ni_smt_solver(cmd_context & ctx):m_cmd_ctx(ctx), m_context(0), m_callback(0) {}
-
-    virtual ~ni_smt_solver() {
-        if (m_context != 0)
-            dealloc(m_context);
-    }
-
-    virtual void init_core(ast_manager & m, symbol const & logic) {
-        // do nothing
-    }
-
-    virtual void collect_statistics(statistics & st) const {
-        if (m_context == 0) {
-            return;
-        }
-        else {
-            m_context->collect_statistics(st);
-        }
-    }
-
-    virtual void reset_core() {
-        if (m_context != 0) {
-            #pragma omp critical (ni_solver) 
-            {
-                dealloc(m_context);
-                m_context = 0;
-            }
-        }
-    }
-
-    virtual void assert_expr(expr * t) {
-        // do nothing
-    }
-
-    virtual void push_core() {
-        // do nothing
-    }
-
-    virtual void pop_core(unsigned n) {
-        // do nothing
-    }
-
-    void assert_exprs() {
-        ptr_vector<expr>::const_iterator it  = m_cmd_ctx.begin_assertions();
-        ptr_vector<expr>::const_iterator end = m_cmd_ctx.end_assertions();
-        for (; it != end; ++it) {
-            m_context->assert_expr(*it);
-        }
-    }
-
-    void init_solver() {
-        reset_core();
-        #pragma omp critical (ni_solver)
-        {
-            m_context = alloc(smt::kernel, m_cmd_ctx.m(), m_cmd_ctx.params());
-        }
-        if (m_cmd_ctx.has_logic())
-            m_context->set_logic(m_cmd_ctx.get_logic());
-        if (m_callback)
-            m_context->set_progress_callback(m_callback);
-        assert_exprs();
-    }
-
-    virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
-        // erase current solver, and create a new one.
-        init_solver();
-
-        if (num_assumptions == 0) {
-            return m_context->setup_and_check();
-        }
-        else {
-            return m_context->check(num_assumptions, assumptions); 
-        }
-    }
-
-    virtual void get_unsat_core(ptr_vector<expr> & r) {
-        SASSERT(m_context);
-        unsigned sz = m_context->get_unsat_core_size();
-        for (unsigned i = 0; i < sz; i++)
-            r.push_back(m_context->get_unsat_core_expr(i));
-    }
-
-    virtual void get_model(model_ref & m) {
-        SASSERT(m_context);
-        m_context->get_model(m);
-    }
-
-    virtual proof * get_proof() {
-        SASSERT(m_context);
-        return m_context->get_proof();
-    }
-
-    virtual std::string reason_unknown() const {
-        SASSERT(m_context);
-        return m_context->last_failure_as_string();
-    }
-
-    virtual void get_labels(svector<symbol> & r) {
-        SASSERT(m_context);
-        buffer<symbol> tmp;
-        m_context->get_relevant_labels(0, tmp);
-        r.append(tmp.size(), tmp.c_ptr());
-    }
-
-    virtual void set_cancel(bool f) {
-        #pragma omp critical (ni_solver)
-        {
-            if (m_context)
-                m_context->set_cancel(f);
-        }
-    }
-
-    virtual void set_progress_callback(progress_callback * callback) {
-        m_callback = callback;
-        if (m_context)
-            m_context->set_progress_callback(callback);
-    }
-
-
-    virtual void collect_param_descrs(param_descrs & r) {
-        smt::kernel::collect_param_descrs(r);
-    }
-
-};
-
-solver * mk_non_incremental_smt_solver(cmd_context & ctx) {
-    return alloc(ni_smt_solver, ctx);
-}
-
-class qi_smt_solver : public ni_smt_solver {
-    bool            m_inc_mode;   
-public:
-    qi_smt_solver(cmd_context & ctx):ni_smt_solver(ctx), m_inc_mode(false) {}
-    
-    virtual ~qi_smt_solver() {}
-
-    virtual void init_core(ast_manager & m, symbol const & logic) {
-        if (m_inc_mode) {
-            init_solver();
-            m_inc_mode = true;
-        }
-    }
-
-    virtual void reset_core() {
-        ni_smt_solver::reset_core();
-        m_inc_mode = false;
-    }
-
-    void switch_to_inc() {
-        if (!m_inc_mode) {
-            init_solver();
-            m_inc_mode = true;
-        }
-        SASSERT(m_inc_mode);
-    }
-
-    virtual void assert_expr(expr * t) {
-        if (m_context != 0 && !m_inc_mode) {
-            // solver was already created to solve a check_sat query...
-            switch_to_inc();
-        }
-        if (m_inc_mode) {
-            SASSERT(m_context);
-            m_context->assert_expr(t);
-        }
-    }
-
-    virtual void push_core() {
-        switch_to_inc();
-        SASSERT(m_context);
-        m_context->push();
-        SASSERT(m_inc_mode);
-    }
-
-    virtual void pop_core(unsigned n) {
-        switch_to_inc();
-        SASSERT(m_context);
-        m_context->pop(n);
-        SASSERT(m_inc_mode);
-    }
-
-    virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
-        if (!m_inc_mode) {
-            lbool r = ni_smt_solver::check_sat_core(num_assumptions, assumptions);
-            SASSERT(!m_inc_mode);
-            return r;
-        }
-        else {
-            return m_context->check(num_assumptions, assumptions); 
-        }
-    }
-};
-
-
-solver * mk_quasi_incremental_smt_solver(cmd_context & ctx) {
-    return alloc(qi_smt_solver, ctx);
-}
diff --git a/src/smt/ni_solver.h b/src/smt/ni_solver.h
deleted file mode 100644
index c78707319..000000000
--- a/src/smt/ni_solver.h
+++ /dev/null
@@ -1,30 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
-    ni_solver.h
-
-Abstract:
-    Wrappers for smt::context that are non-incremental & (quasi-incremental).
-
-Author:
-
-    Leonardo (leonardo) 2011-03-30
-
-Notes:
-
---*/
-#ifndef _NI_SOLVER_H_
-#define _NI_SOLVER_H_
-
-#include"solver.h"
-class cmd_context;
-
-// Creates a solver that restarts from scratch for every call to check_sat
-solver * mk_non_incremental_smt_solver(cmd_context & ctx);
-
-// Creates a solver that restarts from scratch for the first call to check_sat, and then moves to incremental behavior.
-solver * mk_quasi_incremental_smt_solver(cmd_context & ctx);
-
-#endif
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 5ca7d2dad..081649971 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -24,10 +24,11 @@ Notes:
 namespace smt {
 
     class solver : public solver_na2as {
-        front_end_params * m_params;
-        smt::kernel *     m_context;
+        front_end_params *  m_params;
+        smt::kernel *       m_context;
+        progress_callback * m_callback;
     public:
-        solver():m_params(0), m_context(0) {}
+        solver():m_params(0), m_context(0), m_callback(0) {}
 
         virtual ~solver() {
             if (m_context != 0)
@@ -63,6 +64,8 @@ namespace smt {
 #pragma omp critical (solver)
             {
                 m_context = alloc(smt::kernel, m, *m_params);
+                if (m_callback)
+                    m_context->set_progress_callback(m_callback);
             }
             if (logic != symbol::null)
                 m_context->set_logic(logic);
@@ -145,8 +148,9 @@ namespace smt {
         }
 
         virtual void set_progress_callback(progress_callback * callback) {
-            SASSERT(m_context);
-            m_context->set_progress_callback(callback);
+            m_callback = callback;
+            if (m_context)
+                m_context->set_progress_callback(callback);
         }
 
         virtual unsigned get_num_assertions() const {
diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp
index e9d5eba3e..f6d7414a5 100644
--- a/src/solver/solver_na2as.cpp
+++ b/src/solver/solver_na2as.cpp
@@ -20,6 +20,7 @@ Notes:
 
 --*/
 #include"solver_na2as.h"
+#include"ast_smt2_pp.h"
 
 solver_na2as::solver_na2as() {
     m_manager = 0;
@@ -31,6 +32,9 @@ solver_na2as::~solver_na2as() {
 
 void solver_na2as::assert_expr(expr * t, expr * a) {
     SASSERT(m_manager != 0);
+    SASSERT(is_uninterp_const(a));
+    SASSERT(m_manager->is_bool(a));
+    TRACE("solver_na2as", tout << "asserting\n" << mk_ismt2_pp(t, *m_manager) << "\n" << mk_ismt2_pp(a, *m_manager) << "\n";);
     m_manager->inc_ref(a);
     m_assumptions.push_back(a);
     expr_ref new_t(*m_manager);
diff --git a/src/solver/strategic_solver.cpp b/src/solver/strategic_solver.cpp
index 84de62820..94414bcb1 100644
--- a/src/solver/strategic_solver.cpp
+++ b/src/solver/strategic_solver.cpp
@@ -268,10 +268,15 @@ lbool strategic_solver_core::check_sat_with_assumptions(unsigned num_assumptions
     }
     init_inc_solver();
     m_use_inc_solver_results = true;
+    TRACE("solver_na2as", tout << "invoking inc_solver with " << num_assumptions << " assumptions\n";);
     return m_inc_solver->check_sat(num_assumptions, assumptions);
 }
 
 lbool strategic_solver_core::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
+    TRACE("solver_na2as", tout << "assumptions at strategic_solver_core:\n";
+          for (unsigned i = 0; i < num_assumptions; i++) {
+              tout << mk_ismt2_pp(assumptions[i], m()) << "\n";
+          });
     reset_results();
     m_check_sat_executed = true;
     if (num_assumptions > 0 || // assumptions were provided
@@ -355,6 +360,7 @@ void strategic_solver_core::set_cancel(bool f) {
 }
 
 void strategic_solver_core::get_unsat_core(ptr_vector<expr> & r) {
+    TRACE("solver_na2as", tout << "get_unsat_core, m_use_inc_solver_results: " << m_use_inc_solver_results << "\n";);
     if (m_use_inc_solver_results) {
         SASSERT(m_inc_solver);
         m_inc_solver->get_unsat_core(r); 
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 00c0afaa5..1cf43a45c 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -18,7 +18,6 @@ Notes:
 
 --*/
 #include"cmd_context.h"
-#include"ni_solver.h"
 #include"strategic_solver_cmd.h"
 #include"qfbv_tactic.h"
 #include"qflia_tactic.h"
@@ -80,13 +79,6 @@ static void init(strategic_solver_core * s) {
     s->set_tactic_for(symbol("QF_FPA"),    alloc(qffpa_fct));
 }
 
-solver * mk_smt_strategic_solver(cmd_context & ctx) {
-    strategic_solver_cmd * s = alloc(strategic_solver_cmd, ctx);
-    s->set_inc_solver(mk_quasi_incremental_smt_solver(ctx));
-    init(s);
-    return s;
-}
-
 solver * mk_smt_strategic_solver(bool force_tactic) {
     strategic_solver * s = alloc(strategic_solver);
     s->force_tactic(force_tactic);
diff --git a/src/tactic/portfolio/smt_strategic_solver.h b/src/tactic/portfolio/smt_strategic_solver.h
index f3cc2e0e0..060721e09 100644
--- a/src/tactic/portfolio/smt_strategic_solver.h
+++ b/src/tactic/portfolio/smt_strategic_solver.h
@@ -20,9 +20,7 @@ Notes:
 #ifndef _SMT_STRATEGIC_SOLVER_H_
 #define _SMT_STRATEGIC_SOLVER_H_
 
-class cmd_context;
-// Create a strategic solver for the SMT 2.0 frontend.
-solver * mk_smt_strategic_solver(cmd_context & ctx);
+class solver;
 // Create a strategic solver for the Z3 API
 solver * mk_smt_strategic_solver(bool force_tactic=false);