diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 6c1f068b5..424398be0 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -996,6 +996,10 @@ extern "C" {
             case PR_IFF_FALSE: return Z3_OP_PR_IFF_FALSE;
             case PR_COMMUTATIVITY: return Z3_OP_PR_COMMUTATIVITY;
             case PR_DEF_AXIOM: return Z3_OP_PR_DEF_AXIOM;
+            case PR_ASSUMPTION_ADD: return Z3_OP_PR_ASSUMPTION_ADD;
+            case PR_LEMMA_ADD: return Z3_OP_PR_LEMMA_ADD;
+            case PR_REDUNDANT_DEL: return Z3_OP_PR_REDUNDANT_DEL;
+            case PR_CLAUSE_TRAIL: return Z3_OP_PR_CLAUSE_TRAIL;
             case PR_DEF_INTRO: return Z3_OP_PR_DEF_INTRO;
             case PR_APPLY_DEF: return Z3_OP_PR_APPLY_DEF;
             case PR_IFF_OEQ: return Z3_OP_PR_IFF_OEQ;
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 6834a68da..3a666ec37 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -644,6 +644,18 @@ typedef enum
           unfolding the Boolean connectives in the axioms a small
           bounded number of steps (=3).
 
+   - Z3_OP_PR_ASSUMPTION_ADD
+     Clausal proof adding axiom
+
+   - Z3_OP_PR_LEMMA_ADD
+     Clausal proof lemma addition
+
+   - Z3_OP_PR_REDUNDANT_DEL
+     Clausal proof lemma deletion
+
+   - Z3_OP_PR_CLAUSE_TRAIL,
+     Clausal proof trail of additions and deletions
+
    - Z3_OP_PR_DEF_INTRO: Introduces a name for a formula/term.
        Suppose e is an expression with free variables x, and def-intro
        introduces the name n(x). The possible cases are:
@@ -1143,6 +1155,10 @@ typedef enum {
     Z3_OP_PR_IFF_FALSE,
     Z3_OP_PR_COMMUTATIVITY,
     Z3_OP_PR_DEF_AXIOM,
+    Z3_OP_PR_ASSUMPTION_ADD, 
+    Z3_OP_PR_LEMMA_ADD, 
+    Z3_OP_PR_REDUNDANT_DEL, 
+    Z3_OP_PR_CLAUSE_TRAIL,
     Z3_OP_PR_DEF_INTRO,
     Z3_OP_PR_APPLY_DEF,
     Z3_OP_PR_IFF_OEQ,
diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp
index 158396e5e..a458a3674 100644
--- a/src/ast/rewriter/array_rewriter.cpp
+++ b/src/ast/rewriter/array_rewriter.cpp
@@ -352,6 +352,11 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
         return BR_REWRITE3;        
     }
 
+    if (m().is_not(f) && m_util.is_map(args[0]) && m().is_not(m_util.get_map_func_decl(args[0]))) {
+        result = to_app(args[0])->get_arg(0);
+        return BR_DONE;
+    }
+
     if (m().is_and(f)) {
         ast_mark mark;
         ptr_buffer<expr> es;
@@ -373,16 +378,48 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
             }
         }
         es.shrink(j);
+        j = 0;
         for (expr* e : es) {
-            if (m().is_not(e, e) && mark.is_marked(e)) {
-                sort_ref s = get_map_array_sort(f, num_args, args);
-                result = m_util.mk_const_array(s, m().mk_false());
-                return BR_DONE;
+            if (m_util.is_map(e) && m().is_not(m_util.get_map_func_decl(e))) {
+                expr * arg = to_app(e)->get_arg(0);
+                if (mark.is_marked(arg)) {
+                    sort_ref s = get_map_array_sort(f, num_args, args);
+                    result = m_util.mk_const_array(s, m().mk_false());
+                    return BR_DONE;
+                }
+                // a & (!a & b & c) -> a & !(b & c)
+                if (m_util.is_map(arg) && m().is_and(m_util.get_map_func_decl(arg))) {
+                    unsigned k = 0;
+                    ptr_buffer<expr> gs;
+                    bool and_change = false;
+                    gs.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
+                    for (unsigned i = 0; i < gs.size(); ++i) {
+                        expr* g = gs[i];
+                        if (mark.is_marked(g)) {
+                            change = true;
+                            and_change = true;
+                        }
+                        else if (m_util.is_map(g) && m().is_and(m_util.get_map_func_decl(g))) {
+                            gs.append(to_app(g)->get_num_args(), to_app(g)->get_args());
+                        }
+                        else {
+                            gs[k++] = gs[i];
+                        }                        
+                    }
+                    gs.shrink(k);
+                    if (and_change) {
+                        std::sort(gs.begin(), gs.end(), [](expr* a, expr* b) { return a->get_id() < b->get_id(); });
+                        expr* arg = m_util.mk_map_assoc(f, gs.size(), gs.c_ptr());
+                        es[j] = m_util.mk_map(m().mk_not_decl(), 1, &arg);                          
+                    }
+                }
             }
+            ++j;
         }        
         if (change) {
+            std::sort(es.begin(), es.end(), [](expr* a, expr* b) { return a->get_id() < b->get_id(); });
             result = m_util.mk_map_assoc(f, es.size(), es.c_ptr());
-            return BR_DONE;
+            return BR_REWRITE2;
         }
     }
 
@@ -408,7 +445,7 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
         }
         es.shrink(j);
         for (expr* e : es) {
-            if (m().is_not(e, e) && mark.is_marked(e)) {
+            if (m_util.is_map(e) && m().is_not(m_util.get_map_func_decl(e)) && mark.is_marked(to_app(e)->get_arg(0))) {
                 sort_ref s = get_map_array_sort(f, num_args, args);
                 result = m_util.mk_const_array(s, m().mk_true());
                 return BR_DONE;
@@ -416,7 +453,7 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
         }        
         if (change) {
             result = m_util.mk_map_assoc(f, es.size(), es.c_ptr());
-            return BR_DONE;
+            return BR_REWRITE1;
         }
     }
 
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 8ba830287..9a3675356 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -174,14 +174,16 @@ public:
 };
 
 ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
-    if (!ctx.produce_proofs())
-        throw cmd_exception("proof construction is not enabled, use command (set-option :produce-proofs true)");
-    if (!ctx.has_manager() ||
-        ctx.cs_state() != cmd_context::css_unsat)
+    if (!ctx.has_manager())
         throw cmd_exception("proof is not available");
+
+    if (ctx.ignore_check())
+        return;
     expr_ref pr(ctx.m());
     pr = ctx.get_check_sat_result()->get_proof();
-    if (pr == 0)
+    if (!pr && !ctx.produce_proofs())
+        throw cmd_exception("proof construction is not enabled, use command (set-option :produce-proofs true)");
+    if (!pr) 
         throw cmd_exception("proof is not available");
     if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) {
         throw cmd_exception("proof is not well sorted");
@@ -209,6 +211,8 @@ ATOMIC_CMD(get_proof_graph_cmd, "get-proof-graph", "retrieve proof and print it
         ctx.cs_state() != cmd_context::css_unsat)
         throw cmd_exception("proof is not available");
     proof_ref pr(ctx.m());
+    if (ctx.ignore_check())
+        return;
     pr = ctx.get_check_sat_result()->get_proof();
     if (pr == 0)
         throw cmd_exception("proof is not available");
@@ -238,6 +242,8 @@ static void print_core(cmd_context& ctx) {
 }
 
 ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", {
+        if (ctx.ignore_check())
+            return;
         if (!ctx.produce_unsat_cores())
             throw cmd_exception("unsat core construction is not enabled, use command (set-option :produce-unsat-cores true)");
         if (!ctx.has_manager() ||
@@ -247,6 +253,8 @@ ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", {
     });
 
 ATOMIC_CMD(get_unsat_assumptions_cmd, "get-unsat-assumptions", "retrieve subset of assumptions sufficient for unsatisfiability", {
+        if (ctx.ignore_check())
+            return;
         if (!ctx.produce_unsat_assumptions())
             throw cmd_exception("unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)");
         if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat) {
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index c2d93fa2a..39c2f43d6 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -128,16 +128,14 @@ void goal::push_back(expr * f, proof * pr, expr_dependency * d) {
         m().del(m_dependencies);
         m_inconsistent = true;
         m().push_back(m_forms, m().mk_false());
-        if (proofs_enabled())
-            m().push_back(m_proofs, saved_pr);
+        m().push_back(m_proofs, saved_pr);
         if (unsat_core_enabled())
             m().push_back(m_dependencies, saved_d);
     }
     else {
         SASSERT(!m_inconsistent);
         m().push_back(m_forms, f);
-        if (proofs_enabled())
-            m().push_back(m_proofs, pr);
+        m().push_back(m_proofs, pr);
         if (unsat_core_enabled())
             m().push_back(m_dependencies, d);
     }
@@ -248,11 +246,12 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) {
     expr_ref _f(f, m());
     proof_ref _pr(pr, m());
     expr_dependency_ref _d(d, m());
-    SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
-    if (m_inconsistent)
+    if (m_inconsistent) {
         return;
-    if (proofs_enabled())
+    }
+    if (pr) {
         slow_process(f, pr, d);
+    }
     else {
         expr_ref fr(f, m());
         quick_process(false, fr, d);
@@ -278,11 +277,9 @@ void goal::get_formulas(expr_ref_vector & result) const {
 }
 
 void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
-    // KLM: don't know why this assertion is no longer true
-    // SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
     if (m_inconsistent)
         return;
-    if (proofs_enabled()) {
+    if (pr) {
         expr_ref out_f(m());
         proof_ref out_pr(m());
         slow_process(true, f, pr, d, out_f, out_pr);
@@ -455,9 +452,8 @@ void goal::shrink(unsigned j) {
     unsigned sz = size();
     for (unsigned i = j; i < sz; i++)
         m().pop_back(m_forms);
-    if (proofs_enabled()) 
-        for (unsigned i = j; i < sz; i++)
-            m().pop_back(m_proofs);
+    for (unsigned i = j; i < sz; i++)
+        m().pop_back(m_proofs);
     if (unsat_core_enabled()) 
         for (unsigned i = j; i < sz; i++)
             m().pop_back(m_dependencies);
@@ -478,8 +474,7 @@ void goal::elim_true() {
             continue;
         }
         m().set(m_forms, j, f);
-        if (proofs_enabled())
-            m().set(m_proofs, j, m().get(m_proofs, i));
+        m().set(m_proofs, j, m().get(m_proofs, i));
         if (unsat_core_enabled())
             m().set(m_dependencies, j, m().get(m_dependencies, i));
         j++;
@@ -565,8 +560,7 @@ void goal::elim_redundancies() {
             continue;
         }
         m().set(m_forms, j, f);
-        if (proofs_enabled())
-            m().set(m_proofs, j, pr(i));
+        m().set(m_proofs, j, pr(i));
         if (unsat_core_enabled())
             m().set(m_dependencies, j, dep(i));
         j++;
@@ -596,8 +590,7 @@ goal * goal::translate(ast_translation & translator) const {
     unsigned sz = m().size(m_forms);
     for (unsigned i = 0; i < sz; i++) {
         res->m().push_back(res->m_forms, translator(m().get(m_forms, i)));
-        if (res->proofs_enabled())
-            res->m().push_back(res->m_proofs, translator(m().get(m_proofs, i)));
+        res->m().push_back(res->m_proofs, translator(m().get(m_proofs, i)));
         if (res->unsat_core_enabled())
             res->m().push_back(res->m_dependencies, dep_translator(m().get(m_dependencies, i)));
     }
diff --git a/src/tactic/goal.h b/src/tactic/goal.h
index 33f9298ab..c0ad029e1 100644
--- a/src/tactic/goal.h
+++ b/src/tactic/goal.h
@@ -121,7 +121,7 @@ public:
     unsigned num_exprs() const;
   
     expr * form(unsigned i) const { return m().get(m_forms, i); }
-    proof * pr(unsigned i) const { return proofs_enabled() ? static_cast<proof*>(m().get(m_proofs, i)) : nullptr; }
+    proof * pr(unsigned i) const { return m().size(m_proofs) > i ? static_cast<proof*>(m().get(m_proofs, i)) : nullptr; }
     expr_dependency * dep(unsigned i) const { return unsat_core_enabled() ? m().get(m_dependencies, i) : nullptr; }
 
     void update(unsigned i, expr * f, proof * pr = nullptr, expr_dependency * dep = nullptr);
diff --git a/src/util/uint_set.h b/src/util/uint_set.h
index 202df1039..ebef623aa 100644
--- a/src/util/uint_set.h
+++ b/src/util/uint_set.h
@@ -364,6 +364,11 @@ public:
         SASSERT(!contains(x));
     }
 
+    unsigned elem_at(unsigned index) {
+        SASSERT(index < m_size);
+        return m_elems[index];
+    }
+
     bool contains(unsigned x) const { return x < m_index.size() && m_index[x] < m_size && m_elems[m_index[x]] == x; }
     void reset() { m_size = 0; }
     bool empty() const { return m_size == 0; }    
@@ -372,8 +377,13 @@ public:
     typedef  unsigned_vector::const_iterator iterator;
     iterator begin() const { return m_elems.begin(); }
     iterator end() const { return m_elems.begin() + m_size; }
-
+    
 };
 
+inline std::ostream& operator<<(std::ostream& out, indexed_uint_set const& s) {
+    for (unsigned i : s) out << i << " ";
+    return out;
+}
+
 #endif /* UINT_SET_H_ */