From 026265f9a3709c7bf9443c75f3e6b419bc762d4a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 3 Jul 2018 08:55:26 -0700
Subject: [PATCH 1/6] fix memory leak in proof production in theory_pb

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.cpp                  |   6 +
 src/ast/ast.h                    |   6 +-
 src/ast/ast_util.cpp             |  72 +++---
 src/ast/proofs/proof_checker.cpp | 382 +++++++++++++++----------------
 src/ast/proofs/proof_checker.h   |  38 +--
 src/smt/theory_pb.cpp            |   6 +-
 6 files changed, 243 insertions(+), 267 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 0ea2f3cd5..ce3cad403 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1371,6 +1371,12 @@ void ast_manager::update_fresh_id(ast_manager const& m) {
     m_fresh_id = std::max(m_fresh_id, m.m_fresh_id);
 }
 
+void ast_manager::inc_ref(ast * n) {
+    if (n) {
+        n->inc_ref();
+    }
+}
+
 void ast_manager::init() {
     m_int_real_coercions = true;
     m_debug_ref_count = false;
diff --git a/src/ast/ast.h b/src/ast/ast.h
index aa8669def..c4efe4ad3 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1622,11 +1622,7 @@ public:
 
     void debug_ref_count() { m_debug_ref_count = true; }
 
-    void inc_ref(ast * n) {
-        if (n) {
-            n->inc_ref();
-        }
-    }
+    void inc_ref(ast * n);
     
     void dec_ref(ast* n) {
         if (n) {
diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp
index 42c0d698b..601eee58e 100644
--- a/src/ast/ast_util.cpp
+++ b/src/ast/ast_util.cpp
@@ -128,11 +128,9 @@ bool is_clause(ast_manager & m, expr * n) {
     if (is_literal(m, n))
         return true;
     if (m.is_or(n)) {
-        unsigned num_args = to_app(n)->get_num_args();
-        for (unsigned i = 0; i < num_args; i++) {
-            if (!is_literal(m, to_app(n)->get_arg(i)))
-                return false;
-        }
+        for (expr* arg : *to_app(n))
+            if (!is_literal(m, arg))
+                return false;        
         return true;
     }
     return false;
@@ -211,8 +209,8 @@ expr_ref push_not(const expr_ref& e) {
             return expr_ref(m.mk_false(), m);
         }
         expr_ref_vector args(m);
-        for (unsigned i = 0; i < a->get_num_args(); ++i) {
-            args.push_back(push_not(expr_ref(a->get_arg(i), m)));
+        for (expr* arg : *a) {
+            args.push_back(push_not(expr_ref(arg, m)));
         }
         return mk_or(args);
     }
@@ -221,8 +219,8 @@ expr_ref push_not(const expr_ref& e) {
             return expr_ref(m.mk_true(), m);
         }
         expr_ref_vector args(m);
-        for (unsigned i = 0; i < a->get_num_args(); ++i) {
-            args.push_back(push_not(expr_ref(a->get_arg(i), m)));
+        for (expr* arg : *a) {
+            args.push_back(push_not(expr_ref(arg, m)));
         }
         return mk_and(args);
     }
@@ -260,44 +258,38 @@ void flatten_and(expr_ref_vector& result) {
     ast_manager& m = result.get_manager();
     expr* e1, *e2, *e3;
     for (unsigned i = 0; i < result.size(); ++i) {
-        if (m.is_and(result[i].get())) {
-            app* a = to_app(result[i].get());
-            unsigned num_args = a->get_num_args();
-            for (unsigned j = 0; j < num_args; ++j) {
-                result.push_back(a->get_arg(j));
-            }
+        if (m.is_and(result.get(i))) {
+            app* a = to_app(result.get(i));
+            for (expr* arg : *a) result.push_back(arg);
             result[i] = result.back();
             result.pop_back();
             --i;
         }
-        else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) {
+        else if (m.is_not(result.get(i), e1) && m.is_not(e1, e2)) {
             result[i] = e2;
             --i;
         }
-        else if (m.is_not(result[i].get(), e1) && m.is_or(e1)) {
+        else if (m.is_not(result.get(i), e1) && m.is_or(e1)) {
             app* a = to_app(e1);
-            unsigned num_args = a->get_num_args();
-            for (unsigned j = 0; j < num_args; ++j) {
-                result.push_back(m.mk_not(a->get_arg(j)));
-            }
+            for (expr* arg : *a) result.push_back(m.mk_not(arg));
             result[i] = result.back();
             result.pop_back();
             --i;
         }
-        else if (m.is_not(result[i].get(), e1) && m.is_implies(e1,e2,e3)) {
+        else if (m.is_not(result.get(i), e1) && m.is_implies(e1,e2,e3)) {
             result.push_back(e2);
             result[i] = m.mk_not(e3);
             --i;
         }
-        else if (m.is_true(result[i].get()) ||
-                 (m.is_not(result[i].get(), e1) &&
+        else if (m.is_true(result.get(i)) ||
+                 (m.is_not(result.get(i), e1) &&
                   m.is_false(e1))) {
             result[i] = result.back();
             result.pop_back();
             --i;
         }
-        else if (m.is_false(result[i].get()) ||
-                 (m.is_not(result[i].get(), e1) &&
+        else if (m.is_false(result.get(i)) ||
+                 (m.is_not(result.get(i), e1) &&
                   m.is_true(e1))) {
             result.reset();
             result.push_back(m.mk_false());
@@ -323,44 +315,38 @@ void flatten_or(expr_ref_vector& result) {
     ast_manager& m = result.get_manager();
     expr* e1, *e2, *e3;
     for (unsigned i = 0; i < result.size(); ++i) {
-        if (m.is_or(result[i].get())) {
-            app* a = to_app(result[i].get());
-            unsigned num_args = a->get_num_args();
-            for (unsigned j = 0; j < num_args; ++j) {
-                result.push_back(a->get_arg(j));
-            }
+        if (m.is_or(result.get(i))) {
+            app* a = to_app(result.get(i));
+            for (expr* arg : *a) result.push_back(arg);
             result[i] = result.back();
             result.pop_back();
             --i;
         }
-        else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) {
+        else if (m.is_not(result.get(i), e1) && m.is_not(e1, e2)) {
             result[i] = e2;
             --i;
         }
-        else if (m.is_not(result[i].get(), e1) && m.is_and(e1)) {
+        else if (m.is_not(result.get(i), e1) && m.is_and(e1)) {
             app* a = to_app(e1);
-            unsigned num_args = a->get_num_args();
-            for (unsigned j = 0; j < num_args; ++j) {
-                result.push_back(m.mk_not(a->get_arg(j)));
-            }
+            for (expr* arg : *a) result.push_back(m.mk_not(arg));
             result[i] = result.back();
             result.pop_back();
             --i;
         }
-        else if (m.is_implies(result[i].get(),e2,e3)) {
+        else if (m.is_implies(result.get(i),e2,e3)) {
             result.push_back(e3);
             result[i] = m.mk_not(e2);
             --i;
         }
-        else if (m.is_false(result[i].get()) ||
-                 (m.is_not(result[i].get(), e1) &&
+        else if (m.is_false(result.get(i)) ||
+                 (m.is_not(result.get(i), e1) &&
                   m.is_true(e1))) {
             result[i] = result.back();
             result.pop_back();
             --i;
         }
-        else if (m.is_true(result[i].get()) ||
-                 (m.is_not(result[i].get(), e1) &&
+        else if (m.is_true(result.get(i)) ||
+                 (m.is_not(result.get(i), e1) &&
                   m.is_false(e1))) {
             result.reset();
             result.push_back(m.mk_true());
diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp
index b8d7b2b46..fd6ea43e1 100644
--- a/src/ast/proofs/proof_checker.cpp
+++ b/src/ast/proofs/proof_checker.cpp
@@ -140,8 +140,8 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
     proof_ref_vector proofs(m);
 
     if (match_proof(p, proofs)) {
-        for (unsigned i = 0; i < proofs.size(); ++i) {
-            add_premise(proofs[i].get());
+        for (proof* pr : proofs) {
+            add_premise(pr);
         }
     }
     switch(k) {
@@ -188,22 +188,22 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
 
 bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     decl_kind k = p->get_decl_kind();
-    expr_ref fml0(m), fml1(m), fml2(m), fml(m);
-    expr_ref t1(m), t2(m);
-    expr_ref s1(m), s2(m);
-    expr_ref u1(m), u2(m);
-    expr_ref fact(m), body1(m), body2(m);
-    expr_ref l1(m), l2(m), r1(m), r2(m);
-    func_decl_ref d1(m), d2(m), d3(m);
-    proof_ref p0(m), p1(m), p2(m);
+    expr* fml0 = nullptr, *fml1 = nullptr, *fml2 = nullptr, *fml = nullptr;
+    expr* t1 = nullptr, *t2 = nullptr;
+    expr* s1 = nullptr, *s2 = nullptr;
+    expr* u1 = nullptr, *u2 = nullptr;
+    expr* fact = nullptr, *body1 = nullptr, *body2 = nullptr;
+    expr* l1 = nullptr, *l2 = nullptr, *r1 = nullptr, *r2 = nullptr;
+    func_decl* d1 = nullptr, *d2 = nullptr, *d3 = nullptr;
+    proof* p0 = nullptr, *p1 = nullptr, *p2 = nullptr;
     proof_ref_vector proofs(m);
-    func_decl_ref f1(m), f2(m);
-    expr_ref_vector terms1(m), terms2(m), terms(m);
+    func_decl* f1 = nullptr, *f2 = nullptr;
+    ptr_vector<expr> terms1, terms2, terms;
     sort_ref_vector decls1(m), decls2(m);
 
     if (match_proof(p, proofs)) {
-        for (unsigned i = 0; i < proofs.size(); ++i) {
-            add_premise(proofs.get(i));
+        for (proof* pr : proofs) {
+            add_premise(pr);
         }
     }
 
@@ -219,11 +219,11 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     case PR_MODUS_PONENS: {
         if (match_fact(p, fact) &&
             match_proof(p, p0, p1) &&
-            match_fact(p0.get(), fml0) &&
-            match_fact(p1.get(), fml1) &&
-            (match_implies(fml1.get(), t1, t2) || match_iff(fml1.get(), t1, t2)) &&
-            (fml0.get() == t1.get()) &&
-            (fact.get() == t2.get())) {
+            match_fact(p0, fml0) &&
+            match_fact(p1, fml1) &&
+            (match_implies(fml1, t1, t2) || match_iff(fml1, t1, t2)) &&
+            (fml0 == t1) &&
+            (fact == t2)) {
             return true;
         }
         UNREACHABLE();
@@ -233,7 +233,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         if (match_fact(p, fact) &&
             match_proof(p) &&
             (match_equiv(fact, t1, t2) || match_oeq(fact, t1, t2)) &&
-            (t1.get() == t2.get())) {
+            (t1 == t2)) {
             return true;
         }
         UNREACHABLE();
@@ -242,12 +242,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     case PR_SYMMETRY: {
         if (match_fact(p, fact) &&
             match_proof(p, p1) &&
-            match_fact(p1.get(), fml) &&
-            match_binary(fact.get(), d1, l1, r1) &&
-            match_binary(fml.get(), d2, l2, r2) &&
-            SAME_OP(d1.get(), d2.get()) &&
-            l1.get() == r2.get() &&
-            r1.get() == l2.get()) {
+            match_fact(p1, fml) &&
+            match_binary(fact, d1, l1, r1) &&
+            match_binary(fml, d2, l2, r2) &&
+            SAME_OP(d1, d2) &&
+            l1 == r2 &&
+            r1 == l2) {
             // TBD d1, d2 is a symmetric predicate
             return true;
         }
@@ -257,16 +257,16 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     case PR_TRANSITIVITY: {
         if (match_fact(p, fact) &&
             match_proof(p, p1, p2) &&
-            match_fact(p1.get(), fml1) &&
-            match_fact(p2.get(), fml2) &&
-            match_binary(fact.get(), d1, t1, t2) &&
-            match_binary(fml1.get(), d2, s1, s2) &&
-            match_binary(fml2.get(), d3, u1, u2) &&
-            d1.get() == d2.get() &&
-            d2.get() == d3.get() &&
-            t1.get() == s1.get() &&
-            s2.get() == u1.get() &&
-            u2.get() == t2.get()) {
+            match_fact(p1, fml1) &&
+            match_fact(p2, fml2) &&
+            match_binary(fact, d1, t1, t2) &&
+            match_binary(fml1, d2, s1, s2) &&
+            match_binary(fml2, d3, u1, u2) &&
+            d1 == d2 &&
+            d2 == d3 &&
+            t1 == s1 &&
+            s2 == u1 &&
+            u2 == t2) {
             // TBD d1 is some transitive predicate.
             return true;
         }
@@ -275,13 +275,13 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     }
     case PR_TRANSITIVITY_STAR: {
         if (match_fact(p, fact) &&
-            match_binary(fact.get(), d1, t1, t2)) {
+            match_binary(fact, d1, t1, t2)) {
             u_map<bool> vertices;
             // TBD check that d1 is transitive, symmetric.
-            for (unsigned i = 0; i < proofs.size(); ++i) {
-                if (match_fact(proofs[i].get(), fml) &&
-                    match_binary(fml.get(), d2, s1, s2) &&
-                    d1.get() == d2.get()) {
+            for (proof* pr : proofs) {
+                if (match_fact(pr, fml) &&
+                    match_binary(fml, d2, s1, s2) &&
+                    d1 == d2) {
                     unsigned id1 = s1->get_id();
                     unsigned id2 = s2->get_id();
 #define INSERT(_id) if (vertices.contains(_id)) vertices.remove(_id); else vertices.insert(_id, true);
@@ -304,24 +304,24 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     case PR_MONOTONICITY: {
         TRACE("proof_checker", tout << mk_bounded_pp(p, m, 3) << "\n";);
         if (match_fact(p, fact) &&
-            match_binary(fact.get(), d1, t1, t2) &&
-            match_app(t1.get(), f1, terms1) &&
-            match_app(t2.get(), f2, terms2) &&
-            f1.get() == f2.get() &&
+            match_binary(fact, d1, t1, t2) &&
+            match_app(t1, f1, terms1) &&
+            match_app(t2, f2, terms2) &&
+            f1 == f2 &&
             terms1.size() == terms2.size()) {
             // TBD: d1 is monotone.
             for (unsigned i = 0; i < terms1.size(); ++i) {
-                expr* term1 = terms1[i].get();
-                expr* term2 = terms2[i].get();
+                expr* term1 = terms1[i];
+                expr* term2 = terms2[i];
                 if (term1 != term2) {
                     bool found = false;
-                    for(unsigned j = 0; j < proofs.size() && !found; ++j) {
-                        found =
-                            match_fact(proofs[j].get(), fml) &&
-                            match_binary(fml.get(), d2, s1, s2) &&
-                            SAME_OP(d1.get(), d2.get()) &&
-                            s1.get() == term1 &&
-                            s2.get() == term2;
+                    for (proof* pr : proofs) {
+                        found |=
+                            match_fact(pr, fml) &&
+                            match_binary(fml, d2, s1, s2) &&
+                            SAME_OP(d1, d2) &&
+                            s1 == term1 &&
+                            s2 == term2;
                     }
                     if (!found) {
                         UNREACHABLE();
@@ -337,24 +337,24 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     case PR_QUANT_INTRO: {
         if (match_proof(p, p1) &&
             match_fact(p, fact) &&
-            match_fact(p1.get(), fml) &&
+            match_fact(p1, fml) &&
             (is_lambda(fact) || is_lambda(fml)))
             return true;
 
         if (match_proof(p, p1) &&
             match_fact(p, fact) &&
-            match_fact(p1.get(), fml) &&
-            (match_iff(fact.get(), t1, t2) || match_oeq(fact.get(), t1, t2)) &&
-            (match_iff(fml.get(), s1, s2) || match_oeq(fml.get(), s1, s2)) &&
-            m.is_oeq(fact.get()) == m.is_oeq(fml.get()) &&
-            is_quantifier(t1.get()) &&
-            is_quantifier(t2.get()) &&
-            to_quantifier(t1.get())->get_expr() == s1.get() &&
-            to_quantifier(t2.get())->get_expr() == s2.get() &&
-            to_quantifier(t1.get())->get_num_decls() == to_quantifier(t2.get())->get_num_decls() &&
-            to_quantifier(t1.get())->get_kind() == to_quantifier(t2.get())->get_kind()) {
-            quantifier* q1 = to_quantifier(t1.get());
-            quantifier* q2 = to_quantifier(t2.get());
+            match_fact(p1, fml) &&
+            (match_iff(fact, t1, t2) || match_oeq(fact, t1, t2)) &&
+            (match_iff(fml, s1, s2) || match_oeq(fml, s1, s2)) &&
+            m.is_oeq(fact) == m.is_oeq(fml) &&
+            is_quantifier(t1) &&
+            is_quantifier(t2) &&
+            to_quantifier(t1)->get_expr() == s1 &&
+            to_quantifier(t2)->get_expr() == s2 &&
+            to_quantifier(t1)->get_num_decls() == to_quantifier(t2)->get_num_decls() &&
+            to_quantifier(t1)->get_kind() == to_quantifier(t2)->get_kind()) {
+            quantifier* q1 = to_quantifier(t1);
+            quantifier* q2 = to_quantifier(t2);
             for (unsigned i = 0; i < q1->get_num_decls(); ++i) {
                 if (q1->get_decl_sort(i) != q2->get_decl_sort(i)) {
                     // term is not well-typed.
@@ -377,37 +377,33 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     case PR_DISTRIBUTIVITY: {
         if (match_fact(p, fact) &&
             match_proof(p) &&
-            match_equiv(fact.get(), t1, t2)) {
-            side_conditions.push_back(fact.get());
+            match_equiv(fact, t1, t2)) {
+            side_conditions.push_back(fact);
             return true;
         }
         UNREACHABLE();
         return false;
     }
     case PR_AND_ELIM: {
-        expr_ref_vector terms(m);
         if (match_proof(p, p1) &&
             match_fact(p, fact) &&
-            match_fact(p1.get(), fml) &&
-            match_and(fml.get(), terms)) {
-            for (unsigned i = 0; i < terms.size(); ++i) {
-                if (terms[i].get() == fact.get()) {
-                    return true;
-                }
-            }
+            match_fact(p1, fml) &&
+            match_and(fml, terms)) {
+            for (expr* t : terms) 
+                if (t == fact) return true;
         }
         UNREACHABLE();
         return false;
     }
     case PR_NOT_OR_ELIM: {
-        expr_ref_vector terms(m);
+        
         if (match_proof(p, p1) &&
             match_fact(p, fact) &&
-            match_fact(p1.get(), fml) &&
-            match_not(fml.get(), fml1) &&
-            match_or(fml1.get(), terms)) {
-            for (unsigned i = 0; i < terms.size(); ++i) {
-                if (match_negated(terms[i].get(), fact.get())) {
+            match_fact(p1, fml) &&
+            match_not(fml, fml1) &&
+            match_or(fml1, terms)) {
+            for (expr* t : terms) {
+                if (match_negated(t, fact)) {
                     return true;
                 }
             }
@@ -418,8 +414,8 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     case PR_REWRITE: {
         if (match_fact(p, fact) &&
             match_proof(p) &&
-            match_equiv(fact.get(), t1, t2)) {
-            side_conditions.push_back(fact.get());
+            match_equiv(fact, t1, t2)) {
+            side_conditions.push_back(fact);
             return true;
         }
         IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m););
@@ -427,12 +423,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     }
     case PR_REWRITE_STAR: {
         if (match_fact(p, fact) &&
-            match_equiv(fact.get(), t1, t2)) {
+            match_equiv(fact, t1, t2)) {
             expr_ref_vector rewrite_eq(m);
-            rewrite_eq.push_back(fact.get());
-            for (unsigned i = 0; i < proofs.size(); ++i) {
-                if (match_fact(proofs[i].get(), fml)) {
-                    rewrite_eq.push_back(m.mk_not(fml.get()));
+            rewrite_eq.push_back(fact);
+            for (proof* pr : proofs) {
+                if (match_fact(pr, fml)) {
+                    rewrite_eq.push_back(m.mk_not(fml));
                 }
             }
             expr_ref rewrite_cond(m);
@@ -446,8 +442,8 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     case PR_PULL_QUANT: {
         if (match_proof(p) &&
             match_fact(p, fact) &&
-            match_iff(fact.get(), t1, t2) &&
-            is_quantifier(t2.get())) {
+            match_iff(fact, t1, t2) &&
+            is_quantifier(t2)) {
             // TBD: check the enchilada.
             return true;
         }
@@ -457,16 +453,16 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     case PR_PUSH_QUANT: {
         if (match_proof(p) &&
             match_fact(p, fact) &&
-            match_iff(fact.get(), t1, t2) &&
-            is_quantifier(t1.get()) &&
-            match_and(to_quantifier(t1.get())->get_expr(), terms1) &&
-            match_and(t2.get(), terms2) &&
+            match_iff(fact, t1, t2) &&
+            is_quantifier(t1) &&
+            match_and(to_quantifier(t1)->get_expr(), terms1) &&
+            match_and(t2, terms2) &&
             terms1.size() == terms2.size()) {
-            quantifier * q1 = to_quantifier(t1.get());
+            quantifier * q1 = to_quantifier(t1);
             for (unsigned i = 0; i < terms1.size(); ++i) {
-                if (is_quantifier(terms2[i].get()) &&
-                    to_quantifier(terms2[i].get())->get_expr() == terms1[i].get() &&
-                    to_quantifier(terms2[i].get())->get_num_decls() == q1->get_num_decls()) {
+                if (is_quantifier(terms2[i]) &&
+                    to_quantifier(terms2[i])->get_expr() == terms1[i] &&
+                    to_quantifier(terms2[i])->get_num_decls() == q1->get_num_decls()) {
                     // ok.
                 }
                 else {
@@ -480,9 +476,9 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     case PR_ELIM_UNUSED_VARS: {
         if (match_proof(p) &&
             match_fact(p, fact) &&
-            match_iff(fact.get(), t1, t2)) {
+            match_iff(fact, t1, t2)) {
             // TBD:
-            // match_quantifier(t1.get(), is_forall1, decls1, body1)
+            // match_quantifier(t1, is_forall1, decls1, body1)
             // filter out decls1 that occur in body1.
             // if list is empty, then t2 could be just body1.
             // otherwise t2 is also a quantifier.
@@ -495,7 +491,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         bool is_forall = false;
         if (match_proof(p) &&
             match_fact(p, fact) &&
-            match_iff(fact.get(), t1, t2) &&
+            match_iff(fact, t1, t2) &&
             match_quantifier(t1, is_forall, decls1, body1) &&
             is_forall) {
             // TBD: check that terms are set of equalities.
@@ -516,18 +512,18 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     case PR_LEMMA: {
         if (match_proof(p, p1) &&
             match_fact(p, fact) &&
-            match_fact(p1.get(), fml) &&
-            m.is_false(fml.get())) {
+            match_fact(p1, fml) &&
+            m.is_false(fml)) {
             expr_ref_vector hypotheses(m);
             expr_ref_vector ors(m);
-            get_hypotheses(p1.get(), hypotheses);
+            get_hypotheses(p1, hypotheses);
             if (hypotheses.size() == 1 && match_negated(hypotheses.get(0), fact)) {
                 // Suppose fact is (or a b c) and hypothesis is (not (or a b c))
                 // That is, (or a b c) should be viewed as a 'quoted expression' and a unary clause,
                 // instead of a clause with three literals.
                 return true;
             }
-            get_ors(fact.get(), ors);
+            get_ors(fact, ors);
             for (unsigned i = 0; i < hypotheses.size(); ++i) {
                 bool found = false;
                 unsigned j;
@@ -537,14 +533,9 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
                 if (!found) {
                     TRACE("pr_lemma_bug",
                           tout << "i: " << i << "\n";
-                          tout << "ORs:\n";
-                          for (unsigned i = 0; i < ors.size(); i++) {
-                              tout << mk_pp(ors.get(i), m) << "\n";
-                          }
-                          tout << "HYPOTHESIS:\n";
-                          for (unsigned i = 0; i < hypotheses.size(); i++) {
-                              tout << mk_pp(hypotheses.get(i), m) << "\n";
-                          });
+                          tout << "ORs:\n" << ors << "\n";
+                          tout << "HYPOTHESIS:\n" << hypotheses << "\n";
+                          );
                     UNREACHABLE();
                     return false;
                 }
@@ -562,14 +553,14 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             proofs.size() == 2 &&
             match_fact(proofs[0].get(), fml1) &&
             match_fact(proofs[1].get(), fml2) &&
-            m.is_complement(fml1.get(), fml2.get()) &&
-            m.is_false(fact.get())) {
+            m.is_complement(fml1, fml2) &&
+            m.is_false(fact)) {
             return true;
         }
         if (match_fact(p, fact) &&
             proofs.size() > 1 &&
             match_fact(proofs.get(0), fml) &&
-            match_or(fml.get(), terms1)) {
+            match_or(fml, terms1)) {
             for (unsigned i = 1; i < proofs.size(); ++i) {
                 if (!match_fact(proofs.get(i), fml2)) {
                     return false;
@@ -588,7 +579,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
                     TRACE("pr_unit_bug",
                           tout << "Parents:\n";
                           for (unsigned i = 0; i < proofs.size(); i++) {
-                              expr_ref p(m);
+                              expr* p = nullptr;
                               match_fact(proofs.get(i), p);
                               tout << mk_pp(p, m) << "\n";
                           }
@@ -605,16 +596,15 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             }
             switch(terms1.size()) {
             case 0:
-                return m.is_false(fact.get());
+                return m.is_false(fact);
             case 1:
-                return fact.get() == terms1[0].get();
+                return fact == terms1[0];
             default: {
-                if (match_or(fact.get(), terms2)) {
-                    for (unsigned i = 0; i < terms1.size(); ++i) {
+                if (match_or(fact, terms2)) {
+                    for (expr* term1 : terms1) {
                         bool found = false;
-                        expr* term1 = terms1[i].get();
-                        for (unsigned j = 0; !found && j < terms2.size(); ++j) {
-                            found = term1 == terms2[j].get();
+                        for (expr* term2 : terms2) {
+                            found = term1 == term2;
                         }
                         if (!found) {
                             IF_VERBOSE(0, verbose_stream() << "Premise not found:" << mk_pp(term1, m) << "\n";);
@@ -624,8 +614,8 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
                     return true;
                 }
                 IF_VERBOSE(0, verbose_stream() << "Conclusion is not a disjunction:\n";
-                           verbose_stream() << mk_pp(fml.get(), m) << "\n";
-                           verbose_stream() << mk_pp(fact.get(), m) << "\n";);
+                           verbose_stream() << mk_pp(fml, m) << "\n";
+                           verbose_stream() << mk_pp(fact, m) << "\n";);
 
                 return false;
             }
@@ -639,10 +629,10 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         // iff_true(?rule(?p1, ?fml), (iff ?fml true))
         if (match_proof(p, p1) &&
             match_fact(p, fact) &&
-            match_fact(p1.get(), fml1) &&
-            match_iff(fact.get(), l1, r1) &&
-            fml1.get() == l1.get() &&
-            r1.get() == m.mk_true()) {
+            match_fact(p1, fml1) &&
+            match_iff(fact, l1, r1) &&
+            fml1 == l1 &&
+            r1 == m.mk_true()) {
             return true;
         }
         UNREACHABLE();
@@ -652,11 +642,11 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         // iff_false(?rule(?p1, (not ?fml)), (iff ?fml false))
         if (match_proof(p, p1) &&
             match_fact(p, fact) &&
-            match_fact(p1.get(), fml1) &&
-            match_iff(fact.get(), l1, r1) &&
-            match_not(fml1.get(), t1) &&
-            t1.get() == l1.get() &&
-            r1.get() == m.mk_false()) {
+            match_fact(p1, fml1) &&
+            match_iff(fact, l1, r1) &&
+            match_not(fml1, t1) &&
+            t1 == l1 &&
+            r1 == m.mk_false()) {
             return true;
         }
         UNREACHABLE();
@@ -666,12 +656,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         // commutativity(= (?c ?t1 ?t2) (?c ?t2 ?t1))
         if (match_fact(p, fact) &&
             match_proof(p) &&
-            match_equiv(fact.get(), t1, t2) &&
-            match_binary(t1.get(), d1, s1, s2) &&
-            match_binary(t2.get(), d2, u1, u2) &&
-            s1.get() == u2.get() &&
-            s2.get() == u1.get() &&
-            d1.get() == d2.get() &&
+            match_equiv(fact, t1, t2) &&
+            match_binary(t1, d1, s1, s2) &&
+            match_binary(t2, d2, u1, u2) &&
+            s1 == u2 &&
+            s2 == u1 &&
+            d1 == d2 &&
             d1->is_commutative()) {
             return true;
         }
@@ -682,7 +672,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         // axiom(?fml)
         if (match_fact(p, fact) &&
             match_proof(p) &&
-            m.is_bool(fact.get())) {
+            m.is_bool(fact)) {
             return true;
         }
         UNREACHABLE();
@@ -697,7 +687,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         //
         if (match_fact(p, fact) &&
             match_proof(p) &&
-            m.is_bool(fact.get())) {
+            m.is_bool(fact)) {
             return true;
         }
         UNREACHABLE();
@@ -705,7 +695,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     }
     case PR_APPLY_DEF: {
         if (match_fact(p, fact) &&
-            match_oeq(fact.get(), t1, t2)) {
+            match_oeq(fact, t1, t2)) {
             // TBD: must definitions be in proofs?
             return true;
         }
@@ -716,11 +706,11 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         // axiom(?rule(?p1,(iff ?t1 ?t2)), (~ ?t1 ?t2))
         if (match_fact(p, fact) &&
             match_proof(p, p1) &&
-            match_oeq(fact.get(), t1, t2) &&
-            match_fact(p1.get(), fml) &&
-            match_iff(fml.get(), s1, s2) &&
-            s1.get() == t1.get() &&
-            s2.get() == t2.get()) {
+            match_oeq(fact, t1, t2) &&
+            match_fact(p1, fml) &&
+            match_iff(fml, s1, s2) &&
+            s1 == t1 &&
+            s2 == t2) {
             return true;
         }
         UNREACHABLE();
@@ -738,12 +728,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         // (exists ?x (p ?x y)) -> (p (sk y) y)
         // (not (forall ?x (p ?x y))) -> (not (p (sk y) y))
         if (match_fact(p, fact) &&
-            match_oeq(fact.get(), t1, t2)) {
+            match_oeq(fact, t1, t2)) {
             quantifier* q = nullptr;
-            expr* e = t1.get();
+            expr* e = t1;
             bool is_forall = false;
-            if (match_not(t1.get(), s1)) {
-                e = s1.get();
+            if (match_not(t1, s1)) {
+                e = s1;
                 is_forall = true;
             }
             if (is_quantifier(e)) {
@@ -759,11 +749,11 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     case PR_MODUS_PONENS_OEQ: {
         if (match_fact(p, fact) &&
             match_proof(p, p0, p1) &&
-            match_fact(p0.get(), fml0) &&
-            match_fact(p1.get(), fml1) &&
-            match_oeq(fml1.get(), t1, t2) &&
-            fml0.get() == t1.get() &&
-            fact.get() == t2.get()) {
+            match_fact(p0, fml0) &&
+            match_fact(p1, fml1) &&
+            match_oeq(fml1, t1, t2) &&
+            fml0 == t1 &&
+            fact == t2) {
             return true;
         }
         UNREACHABLE();
@@ -910,7 +900,7 @@ void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
     }
 }
 
-bool proof_checker::match_fact(proof const* p, expr_ref& fact) const {
+bool proof_checker::match_fact(proof const* p, expr*& fact) const {
     if (m.is_proof(p) &&
         m.has_fact(p)) {
         fact = m.get_fact(p);
@@ -932,7 +922,7 @@ bool proof_checker::match_proof(proof const* p) const {
         m.get_num_parents(p) == 0;
 }
 
-bool proof_checker::match_proof(proof const* p, proof_ref& p0) const {
+bool proof_checker::match_proof(proof const* p, proof*& p0) const {
     if (m.is_proof(p) &&
         m.get_num_parents(p) == 1) {
         p0 = m.get_parent(p, 0);
@@ -941,7 +931,7 @@ bool proof_checker::match_proof(proof const* p, proof_ref& p0) const {
     return false;
 }
 
-bool proof_checker::match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const {
+bool proof_checker::match_proof(proof const* p, proof*& p0, proof*& p1) const {
     if (m.is_proof(p) &&
         m.get_num_parents(p) == 2) {
         p0 = m.get_parent(p, 0);
@@ -962,7 +952,7 @@ bool proof_checker::match_proof(proof const* p, proof_ref_vector& parents) const
 }
 
 
-bool proof_checker::match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const {
+bool proof_checker::match_binary(expr const* e, func_decl*& d, expr*& t1, expr*& t2) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_num_args() == 2) {
         d = to_app(e)->get_decl();
@@ -974,18 +964,18 @@ bool proof_checker::match_binary(expr const* e, func_decl_ref& d, expr_ref& t1,
 }
 
 
-bool proof_checker::match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const {
+bool proof_checker::match_app(expr const* e, func_decl*& d, ptr_vector<expr>& terms) const {
     if (e->get_kind() == AST_APP) {
         d = to_app(e)->get_decl();
-        for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
-            terms.push_back(to_app(e)->get_arg(i));
+        for (expr* arg : *to_app(e)) {
+            terms.push_back(arg);
         }
         return true;
     }
     return false;
 }
 
-bool proof_checker::match_quantifier(expr const* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) const {
+bool proof_checker::match_quantifier(expr const* e, bool& is_univ, sort_ref_vector& sorts, expr*& body) const {
     if (is_quantifier(e)) {
         quantifier const* q = to_quantifier(e);
         is_univ = is_forall(q);
@@ -998,7 +988,7 @@ bool proof_checker::match_quantifier(expr const* e, bool& is_univ, sort_ref_vect
     return false;
 }
 
-bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr*& t1, expr*& t2) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k &&
@@ -1010,20 +1000,19 @@ bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref&
     return false;
 }
 
-bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const {
+bool proof_checker::match_op(expr const* e, decl_kind k, ptr_vector<expr>& terms) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k) {
-        for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
-            terms.push_back(to_app(e)->get_arg(i));
-        }
+        for (expr* arg : *to_app(e)) 
+            terms.push_back(arg);
         return true;
     }
     return false;
 }
 
 
-bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t) const {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr*& t) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k &&
@@ -1034,43 +1023,43 @@ bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t) const {
     return false;
 }
 
-bool proof_checker::match_not(expr const* e, expr_ref& t) const {
+bool proof_checker::match_not(expr const* e, expr*& t) const {
     return match_op(e, OP_NOT, t);
 }
 
-bool proof_checker::match_or(expr const* e, expr_ref_vector& terms) const {
+bool proof_checker::match_or(expr const* e, ptr_vector<expr>& terms) const {
     return match_op(e, OP_OR, terms);
 }
 
-bool proof_checker::match_and(expr const* e, expr_ref_vector& terms) const {
+bool proof_checker::match_and(expr const* e, ptr_vector<expr>& terms) const {
     return match_op(e, OP_AND, terms);
 }
 
-bool proof_checker::match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const {
+bool proof_checker::match_iff(expr const* e, expr*& t1, expr*& t2) const {
     return match_op(e, OP_EQ, t1, t2) && m.is_bool(t1);
 }
 
-bool proof_checker::match_equiv(expr const* e, expr_ref& t1, expr_ref& t2) const {
+bool proof_checker::match_equiv(expr const* e, expr*& t1, expr*& t2) const {
     return match_oeq(e, t1, t2) || match_eq(e, t1, t2);
 }
 
-bool proof_checker::match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const {
+bool proof_checker::match_implies(expr const* e, expr*& t1, expr*& t2) const {
     return match_op(e, OP_IMPLIES, t1, t2);
 }
 
-bool proof_checker::match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const {
+bool proof_checker::match_eq(expr const* e, expr*& t1, expr*& t2) const {
     return match_op(e, OP_EQ, t1, t2);
 }
 
-bool proof_checker::match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const {
+bool proof_checker::match_oeq(expr const* e, expr*& t1, expr*& t2) const {
     return match_op(e, OP_OEQ, t1, t2);
 }
 
 bool proof_checker::match_negated(expr const* a, expr* b) const {
-    expr_ref t(m);
+    expr* t = nullptr;
     return
-        (match_not(a, t) && t.get() == b) ||
-        (match_not(b, t) && t.get() == a);
+        (match_not(a, t) && t == b) ||
+        (match_not(b, t) && t == a);
 }
 
 void proof_checker::get_ors(expr* e, expr_ref_vector& ors) {
@@ -1087,8 +1076,7 @@ void proof_checker::get_ors(expr* e, expr_ref_vector& ors) {
 
 void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
     ptr_vector<proof> stack;
-    expr* h = nullptr;
-    expr_ref hyp(m);
+    expr* h = nullptr, *hyp = nullptr;
 
     stack.push_back(p);
     while (!stack.empty()) {
@@ -1099,9 +1087,9 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
             continue;
         }
         if (is_hypothesis(p) && match_fact(p, hyp)) {
-            hyp = mk_atom(hyp.get());
-            m_pinned.push_back(hyp.get());
-            m_hypotheses.insert(p, hyp.get());
+            hyp = mk_atom(hyp);
+            m_pinned.push_back(hyp);
+            m_hypotheses.insert(p, hyp);
             stack.pop_back();
             continue;
         }
@@ -1142,7 +1130,7 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
     ptr_buffer<expr> todo;
     expr_mark mark;
     todo.push_back(h);
-    expr_ref a(m), b(m);
+    expr* a = nullptr, *b = nullptr;
 
     while (!todo.empty()) {
         h = todo.back();
@@ -1153,11 +1141,11 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
         }
         mark.mark(h, true);
         if (match_cons(h, a, b)) {
-            todo.push_back(a.get());
-            todo.push_back(b.get());
+            todo.push_back(a);
+            todo.push_back(b);
         }
         else if (match_atom(h, a)) {
-            ante.push_back(a.get());
+            ante.push_back(a);
         }
         else {
             SASSERT(match_nil(h));
@@ -1181,7 +1169,7 @@ bool proof_checker::match_nil(expr const* e) const {
         to_app(e)->get_decl_kind() == OP_NIL;
 }
 
-bool proof_checker::match_cons(expr const* e, expr_ref& a, expr_ref& b) const {
+bool proof_checker::match_cons(expr const* e, expr*& a, expr*& b) const {
     if (is_app(e) &&
         to_app(e)->get_family_id() == m_hyp_fid &&
         to_app(e)->get_decl_kind() == OP_CONS) {
@@ -1193,7 +1181,7 @@ bool proof_checker::match_cons(expr const* e, expr_ref& a, expr_ref& b) const {
 }
 
 
-bool proof_checker::match_atom(expr const* e, expr_ref& a) const {
+bool proof_checker::match_atom(expr const* e, expr*& a) const {
     if (is_app(e) &&
         to_app(e)->get_family_id() == m_hyp_fid &&
         to_app(e)->get_decl_kind() == OP_ATOM) {
@@ -1372,7 +1360,7 @@ bool proof_checker::check_arith_proof(proof* p) {
         dump_proof(p);
         return true;
     }
-    expr_ref fact(m);
+    expr* fact = nullptr;
     proof_ref_vector proofs(m);
 
     if (!match_fact(p, fact)) {
diff --git a/src/ast/proofs/proof_checker.h b/src/ast/proofs/proof_checker.h
index ac0e31dbd..39c776392 100644
--- a/src/ast/proofs/proof_checker.h
+++ b/src/ast/proofs/proof_checker.h
@@ -77,33 +77,33 @@ private:
     bool check1_spc(proof* p, expr_ref_vector& side_conditions);
     bool check_arith_proof(proof* p);
     bool check_arith_literal(bool is_pos, app* lit, rational const& coeff, expr_ref& sum, bool& is_strict);
-    bool match_fact(proof const* p, expr_ref& fact) const;
+    bool match_fact(proof const* p, expr*& fact) const;
     void add_premise(proof* p);
     bool match_proof(proof const* p) const;
-    bool match_proof(proof const* p, proof_ref& p0) const;
-    bool match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const;
+    bool match_proof(proof const* p, proof*& p0) const;
+    bool match_proof(proof const* p, proof*& p0, proof*& p1) const;
     bool match_proof(proof const* p, proof_ref_vector& parents) const;
-    bool match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const;
-    bool match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const;
-    bool match_op(expr const* e, decl_kind k, expr_ref& t) const;
-    bool match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const;
-    bool match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const;
-    bool match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const;
-    bool match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const;
-    bool match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const;
-    bool match_not(expr const* e, expr_ref& t) const;
-    bool match_or(expr const* e, expr_ref_vector& terms) const;
-    bool match_and(expr const* e, expr_ref_vector& terms) const;
-    bool match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const;
-    bool match_quantifier(expr const*, bool& is_univ, sort_ref_vector&, expr_ref& body) const;
+    bool match_binary(expr const* e, func_decl*& d, expr*& t1, expr*& t2) const;
+    bool match_op(expr const* e, decl_kind k, expr*& t1, expr*& t2) const;
+    bool match_op(expr const* e, decl_kind k, expr*& t) const;
+    bool match_op(expr const* e, decl_kind k, ptr_vector<expr>& terms) const;
+    bool match_iff(expr const* e, expr*& t1, expr*& t2) const;
+    bool match_implies(expr const* e, expr*& t1, expr*& t2) const;
+    bool match_eq(expr const* e, expr*& t1, expr*& t2) const;
+    bool match_oeq(expr const* e, expr*& t1, expr*& t2) const;
+    bool match_not(expr const* e, expr*& t) const;
+    bool match_or(expr const* e, ptr_vector<expr>& terms) const;
+    bool match_and(expr const* e, ptr_vector<expr>& terms) const;
+    bool match_app(expr const* e, func_decl*& d, ptr_vector<expr>& terms) const;
+    bool match_quantifier(expr const*, bool& is_univ, sort_ref_vector&, expr*& body) const;
     bool match_negated(expr const* a, expr* b) const;
-    bool match_equiv(expr const* a, expr_ref& t1, expr_ref& t2) const;
+    bool match_equiv(expr const* a, expr*& t1, expr*& t2) const;
     void get_ors(expr* e, expr_ref_vector& ors);
     void get_hypotheses(proof* p, expr_ref_vector& ante);
 
     bool match_nil(expr const* e) const;
-    bool match_cons(expr const* e, expr_ref& a, expr_ref& b) const;
-    bool match_atom(expr const* e, expr_ref& a) const;
+    bool match_cons(expr const* e, expr*& a, expr*& b) const;
+    bool match_atom(expr const* e, expr*& a) const;
     expr* mk_nil();
     expr* mk_cons(expr* a, expr* b);
     expr* mk_atom(expr* e);
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index b2f15d41e..ed0481938 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -962,11 +962,11 @@ namespace smt {
         m_stats.m_num_conflicts++;
         context& ctx = get_context();
         justification* js = 0;
-        if (proofs_enabled()) {
-            js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
-        }
         c.inc_propagations(*this);
         if (!resolve_conflict(c, lits)) {
+			if (proofs_enabled()) {
+				js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
+			}
             ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
         }
         SASSERT(ctx.inconsistent());

From ec6260342b5506ef4b2178c838b7bd4008e945c0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 3 Jul 2018 09:13:02 -0700
Subject: [PATCH 2/6] fix #1725

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_seq.cpp | 31 ++++++++++++++-----------------
 1 file changed, 14 insertions(+), 17 deletions(-)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 51d1d7119..07eb97f31 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -521,31 +521,28 @@ bool theory_seq::eq_unit(expr* const& l, expr* const &r) const {
 }
 
 // exists x, y, rs' != empty s.t.  (ls = x ++ rs' ++ y & rs = rs') || (ls = rs' ++ x && rs = y ++ rs')
+// TBD: spec comment above doesn't seem to match what this function does.
 unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector const& rs) {
     SASSERT(!ls.empty() && !rs.empty());
-    unsigned_vector res;
+    unsigned_vector result;
     expr_ref l = mk_concat(ls);
     expr_ref r = mk_concat(rs);
     expr_ref pair(m.mk_eq(l,r), m);
-    if (m_overlap.find(pair, res)) {
-        return res;
+    if (m_overlap.find(pair, result)) {
+        return result;
     }
-    unsigned_vector result;
-    for (unsigned i = 0; i < ls.size(); ++i) {
+    result.reset();
+    if (eq_unit(ls[0], rs.back())) {
+       result.push_back(1);
+    }
+    for (unsigned i = 1; i < ls.size(); ++i) {
         if (eq_unit(ls[i], rs.back())) {
-            bool same = true;
-            if (i >= 1) {
-                for (unsigned j = i - 1; rs.size() + j >= 1 + i; --j) {
-                    if (!eq_unit(ls[j], rs[rs.size()+j-i-1])) {
-                        same = false;
-                        break;
-                    }
-                }
-                if (same)
-                    result.push_back(i+1);
+            bool same = rs.size() > i;
+            for (unsigned j = 0; same && j < i; ++j) {
+                same = eq_unit(ls[j], rs[rs.size() - 1 - i + j]);        
             }
-            else 
-                result.push_back(1);
+            if (same)
+                result.push_back(i+1);
         }
     }
     m_overlap.insert(pair, result);

From e37954d87bdc55d9b8357f4445b813db6aaab878 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 3 Jul 2018 09:16:52 -0700
Subject: [PATCH 3/6] simplify code fix for #1725

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_seq.cpp | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 07eb97f31..48fd0c726 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -532,10 +532,7 @@ unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector c
         return result;
     }
     result.reset();
-    if (eq_unit(ls[0], rs.back())) {
-       result.push_back(1);
-    }
-    for (unsigned i = 1; i < ls.size(); ++i) {
+    for (unsigned i = 0; i < ls.size(); ++i) {
         if (eq_unit(ls[i], rs.back())) {
             bool same = rs.size() > i;
             for (unsigned j = 0; same && j < i; ++j) {

From cd482c683eea42bea8e6fd8a4d362b0ce9c8809b Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Tue, 3 Jul 2018 17:18:00 +0100
Subject: [PATCH 4/6] invertible tactic: fix bugs with shift

---
 src/tactic/core/reduce_invertible_tactic.cpp | 24 ++++++++++++--------
 1 file changed, 14 insertions(+), 10 deletions(-)

diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index 40e7ba816..47c002de8 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -94,8 +94,6 @@ public:
     void cleanup() override {}
 
 private:
-
-
     void checkpoint() { 
         if (m.canceled())
             throw tactic_exception(m.limit().get_cancel_msg());
@@ -148,7 +146,12 @@ private:
                 c.m_parents[arg->get_id()].set(n);
             }
         }
-        void operator()(expr*) {}
+
+        void operator()(var* v) {
+            c.m_parents.reserve(v->get_id() + 1);
+        }
+
+        void operator()(quantifier* q) {}
     };
 
     void collect_parents(goal_ref const& g) {
@@ -167,10 +170,9 @@ private:
 
     // TBD: could be made to be recursive, by walking multiple layers of parents.
     
-    bool is_invertible(expr* v, expr*& p, expr_ref& new_v, generic_model_converter_ref* mc) {
+    bool is_invertible(expr* v, expr*& p, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var = 0) {
         p = m_parents[v->get_id()].get();
-        SASSERT(p);
-
+        if (!p) return false;
         if (m_inverted.is_marked(p)) return false;
         if (mc && !is_ground(p)) return false;
 
@@ -191,11 +193,13 @@ private:
 
         expr *a, *b;
         // shift(a, b), where both a,b are single use. Set b = 0 and return a
-        // FIXME: needs to check that both variables are grounded by same quantifier
         if (m_bv.is_bv_shl(p, a, b) ||
             m_bv.is_bv_ashr(p, a, b) ||
             m_bv.is_bv_lshr(p, a, b)) {
-            if (!m_parents[(v == a ? b : a)->get_id()].get())
+            if (!m_parents[(v == a ? b : a)->get_id()].get() || is_var(a) != is_var(b))
+                return false;
+
+            if (is_var(a) && to_var(v == a ? b : a)->get_idx() >= max_var)
                 return false;
 
             if (mc) {
@@ -390,7 +394,7 @@ private:
                 new_sorts.push_back(srt);
             }
             // for each variable, collect parents,
-            // ensure they are in uniqe location and not under other quantifiers.
+            // ensure they are in unique location and not under other quantifiers.
             // if they are invertible, then produce inverting expression.
             //
             expr_safe_replace sub(m);
@@ -407,7 +411,7 @@ private:
             bool has_new_var = false;
             for (unsigned i = 0; i < vars.size(); ++i) {
                 var* v = vars[i];
-                if (!occurs_under_nested_q(v, new_body) && t.is_invertible(v, p, new_v, nullptr)) {
+                if (!occurs_under_nested_q(v, new_body) && t.is_invertible(v, p, new_v, nullptr, vars.size())) {
                     t.mark_inverted(p);
                     sub.insert(p, new_v);
                     new_sorts[i] = m.get_sort(new_v);

From 4359d518a9cfa5298bd81107f9d0ad24651c7e5c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 3 Jul 2018 09:28:22 -0700
Subject: [PATCH 5/6] thanks Nuno

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.cpp | 5 -----
 src/ast/ast.h   | 6 +++++-
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index ce3cad403..ac7ce156d 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1371,11 +1371,6 @@ void ast_manager::update_fresh_id(ast_manager const& m) {
     m_fresh_id = std::max(m_fresh_id, m.m_fresh_id);
 }
 
-void ast_manager::inc_ref(ast * n) {
-    if (n) {
-        n->inc_ref();
-    }
-}
 
 void ast_manager::init() {
     m_int_real_coercions = true;
diff --git a/src/ast/ast.h b/src/ast/ast.h
index c4efe4ad3..aa8669def 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1622,7 +1622,11 @@ public:
 
     void debug_ref_count() { m_debug_ref_count = true; }
 
-    void inc_ref(ast * n);
+    void inc_ref(ast * n) {
+        if (n) {
+            n->inc_ref();
+        }
+    }
     
     void dec_ref(ast* n) {
         if (n) {

From 72f60f5bfc8b7ca8b299b1fa1fc23e19dee264cb Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Tue, 3 Jul 2018 17:51:40 +0100
Subject: [PATCH 6/6] remove copy in generic_model_converter

---
 src/tactic/generic_model_converter.cpp | 6 ++----
 src/tactic/generic_model_converter.h   | 7 -------
 2 files changed, 2 insertions(+), 11 deletions(-)

diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp
index 0790c962a..a64a3a79d 100644
--- a/src/tactic/generic_model_converter.cpp
+++ b/src/tactic/generic_model_converter.cpp
@@ -33,10 +33,9 @@ generic_model_converter::~generic_model_converter() {
 
 void generic_model_converter::add(func_decl * d, expr* e) {
     VERIFY(e);
-    entry et(d, e, m, ADD);
     VERIFY(d->get_range() == m.get_sort(e));
-    m_first_idx.insert_if_not_there(et.m_f, m_entries.size());
-    m_entries.push_back(et);
+    m_first_idx.insert_if_not_there(d, m_entries.size());
+    m_entries.push_back(entry(d, e, m, ADD));
 }
 
 void generic_model_converter::operator()(model_ref & md) {
@@ -250,7 +249,6 @@ void generic_model_converter::get_units(obj_map<expr, bool>& units) {
 
  */
 expr_ref generic_model_converter::simplify_def(entry const& e) {
-    expr_ref result(m);
     expr_ref c(m.mk_const(e.m_f), m);
     if (m.is_bool(c) && occurs(c, e.m_def)) {
         expr_safe_replace rep(m);
diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h
index a190b8525..c67dd5eff 100644
--- a/src/tactic/generic_model_converter.h
+++ b/src/tactic/generic_model_converter.h
@@ -30,13 +30,6 @@ class generic_model_converter : public model_converter {
         instruction   m_instruction;
         entry(func_decl* f, expr* d, ast_manager& m, instruction i):
             m_f(f, m), m_def(d, m), m_instruction(i) {}
-
-        entry& operator=(entry const& other) {
-            m_f = other.m_f;
-            m_def = other.m_def;
-            m_instruction = other.m_instruction;
-            return *this;
-        }
     };
     ast_manager& m;
     std::string  m_orig;