diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 7ed93ab37..b018d62c5 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -507,6 +507,8 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
         s == "QF_AUFLIRA" ||
         s == "QF_AUFNIA" ||
         s == "QF_AUFNIRA" ||
+        s == "QF_ANIA" ||
+        s == "QF_LIRA" ||
         s == "QF_UFLIA" ||
         s == "QF_UFLRA" ||
         s == "QF_UFIDL" ||
@@ -518,6 +520,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
         s == "QF_UFNIA" ||
         s == "QF_UFNIRA" ||
         s == "QF_BVRE" ||
+        s == "ALIA" ||
         s == "AUFLIA" ||
         s == "AUFLIRA" ||
         s == "AUFNIA" ||
@@ -526,9 +529,12 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
         s == "UFLRA" ||
         s == "UFNRA" ||
         s == "UFNIRA" ||
+        s == "NIA" ||
+        s == "NRA" ||
         s == "UFNIA" ||
         s == "LIA" ||
         s == "LRA" ||
+        s == "UFIDL" ||
         s == "QF_FP" ||
         s == "QF_FPBV" ||
         s == "QF_BVFP" ||
@@ -583,10 +589,12 @@ bool cmd_context::logic_has_array_core(symbol const & s) const {
     return
         s == "QF_AX" ||
         s == "QF_AUFLIA" ||
+        s == "QF_ANIA" ||
         s == "QF_ALIA" ||
         s == "QF_AUFLIRA" ||
         s == "QF_AUFNIA" ||
         s == "QF_AUFNIRA" ||
+        s == "ALIA" ||
         s == "AUFLIA" ||
         s == "AUFLIRA" ||
         s == "AUFNIA" ||
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 818e12fd1..3aa02c0b6 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -288,11 +288,13 @@ namespace smt {
     }
 
     void conflict_resolution::process_antecedent(literal antecedent, unsigned & num_marks) {
-        TRACE("conflict", tout << "processing antecedent: "; m_ctx.display_literal(tout, antecedent); tout << "\n";);
         bool_var var = antecedent.var();
         unsigned lvl = m_ctx.get_assign_level(var);
         SASSERT(var < static_cast<int>(m_ctx.get_num_bool_vars()));
-        
+        TRACE("conflict", tout << "processing antecedent (level " << lvl << "):"; 
+              m_ctx.display_literal(tout, antecedent); 
+              m_ctx.display_detailed_literal(tout << " ", antecedent); tout << "\n";);
+
         if (!m_ctx.is_marked(var) && lvl > m_ctx.get_base_level()) {
             m_ctx.set_mark(var);
             m_ctx.inc_bvar_activity(var);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index b75aea2ca..c55243cfd 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -285,7 +285,9 @@ namespace smt {
     }
     
     void context::assign_core(literal l, b_justification j, bool decision) {
-        TRACE("assign_core", tout << "assigning: " << l << " "; display_literal(tout, l); tout << "\n";);
+        TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";              
+              display_literal(tout, l); tout << " level: " << m_scope_lvl << "\n";
+              display(tout, j););
         SASSERT(l.var() < static_cast<int>(m_b_internalized_stack.size()));
         m_assigned_literals.push_back(l);
         m_assignment[l.index()]    = l_true;
@@ -1722,7 +1724,7 @@ namespace smt {
     }
 
     bool context::propagate() {
-        TRACE("propagate", tout << "propagating...\n";);
+        TRACE("propagate", tout << "propagating... " << m_qhead << ":" << m_assigned_literals.size() << "\n";);
         while (true) {
             if (inconsistent())
                 return false;
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 7f13efa9f..8fb3504ad 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1237,6 +1237,8 @@ namespace smt {
 
         void display_profile(std::ostream & out) const;
 
+        void display(std::ostream& out, b_justification j) const;
+
         // -----------------------------------
         //
         // Debugging support
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 3dca6a70b..a9602b478 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -27,19 +27,19 @@ namespace smt {
 
     std::ostream& context::display_last_failure(std::ostream& out) const {
         switch(m_last_search_failure) {
-        case OK: 
+        case OK:
             return out << "OK";
-        case UNKNOWN: 
+        case UNKNOWN:
             return out << "UNKNOWN";
         case TIMEOUT:
             return out << "TIMEOUT";
-        case MEMOUT: 
+        case MEMOUT:
             return out << "MEMOUT";
-        case CANCELED: 
+        case CANCELED:
             return out << "CANCELED";
-        case NUM_CONFLICTS: 
+        case NUM_CONFLICTS:
             return out << "NUM_CONFLICTS";
-        case THEORY: 
+        case THEORY:
             if (!m_incomplete_theories.empty()) {
                 ptr_vector<theory>::const_iterator it  = m_incomplete_theories.begin();
                 ptr_vector<theory>::const_iterator end = m_incomplete_theories.end();
@@ -52,7 +52,7 @@ namespace smt {
                 out << "THEORY";
             }
             return out;
-        case QUANTIFIERS: 
+        case QUANTIFIERS:
             return out << "QUANTIFIERS";
         }
         UNREACHABLE();
@@ -78,18 +78,18 @@ namespace smt {
             r += "))";
             break;
         }
-        case QUANTIFIERS: r = "(incomplete quantifiers)"; break;    
+        case QUANTIFIERS: r = "(incomplete quantifiers)"; break;
         case UNKNOWN: r = "incomplete"; break;
         }
         return r;
     }
-    
+
     void context::display_asserted_formulas(std::ostream & out) const {
         m_asserted_formulas.display_ll(out, get_pp_visited());
     }
 
     void context::display_literal(std::ostream & out, literal l) const {
-        l.display_compact(out, m_bool_var2expr.c_ptr());      
+        l.display_compact(out, m_bool_var2expr.c_ptr());
     }
 
     void context::display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const {
@@ -97,7 +97,7 @@ namespace smt {
     }
 
     void context::display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const {
-        display_verbose(out, m_manager, num_lits, lits, m_bool_var2expr.c_ptr());
+        display_verbose(out, m_manager, num_lits, lits, m_bool_var2expr.c_ptr(), "\n");
     }
 
     void context::display_literal_info(std::ostream & out, literal l) const {
@@ -151,16 +151,16 @@ namespace smt {
         for (unsigned i = 0; i < num_lits; i++) {
             literal l = cls->get_literal(i);
             display_literal(out, l);
-            out << ", val: " << get_assignment(l) << ", lvl: " << get_assign_level(l) 
-                << ", ilvl: " << get_intern_level(l.var()) << ", var: " << l.var() << "\n" 
+            out << ", val: " << get_assignment(l) << ", lvl: " << get_assign_level(l)
+                << ", ilvl: " << get_intern_level(l.var()) << ", var: " << l.var() << "\n"
                 << mk_pp(bool_var2expr(l.var()), m_manager) << "\n\n";
         }
     }
-    
+
     void context::display_clause(std::ostream & out, clause const * cls) const {
         cls->display_compact(out, m_manager, m_bool_var2expr.c_ptr());
     }
-    
+
     void context::display_clauses(std::ostream & out, ptr_vector<clause> const & v) const {
         ptr_vector<clause>::const_iterator it  = v.begin();
         ptr_vector<clause>::const_iterator end = v.end();
@@ -201,12 +201,13 @@ namespace smt {
         if (!m_assigned_literals.empty()) {
             out << "current assignment:\n";
             literal_vector::const_iterator it  = m_assigned_literals.begin();
-            literal_vector::const_iterator end = m_assigned_literals.end();        
+            literal_vector::const_iterator end = m_assigned_literals.end();
             for (; it != end; ++it) {
                 display_literal(out, *it);
-                out << " ";
+                out << ": ";
+                display_verbose(out, m_manager, 1, &*it, m_bool_var2expr.c_ptr());
+                out << "\n";
             }
-            out << "\n";
         }
     }
 
@@ -216,7 +217,7 @@ namespace smt {
         pp.set_status("unknown");
         pp.set_logic(logic);
         literal_vector::const_iterator it  = m_assigned_literals.begin();
-        literal_vector::const_iterator end = m_assigned_literals.end(); 
+        literal_vector::const_iterator end = m_assigned_literals.end();
         for (; it != end; ++it) {
             expr_ref n(m_manager);
             literal2expr(*it, n);
@@ -301,7 +302,7 @@ namespace smt {
             th->display(out);
         }
     }
-    
+
     void context::display(std::ostream & out) const {
         get_pp_visited().reset();
         out << "Logical context:\n";
@@ -336,16 +337,16 @@ namespace smt {
 
     void context::display_eq_detail(std::ostream & out, enode * n) const {
         SASSERT(n->is_eq());
-        out << "#" << n->get_owner_id() 
-            << ", root: #" << n->get_root()->get_owner_id() 
+        out << "#" << n->get_owner_id()
+            << ", root: #" << n->get_root()->get_owner_id()
             << ", cg: #" << n->m_cg->get_owner_id()
-            << ", val: " << get_assignment(enode2bool_var(n)) 
-            << ", lhs: #" << n->get_arg(0)->get_owner_id() 
-            << ", rhs: #" << n->get_arg(1)->get_owner_id() 
-            << ", lhs->root: #" << n->get_arg(0)->get_root()->get_owner_id() 
-            << ", rhs->root: #" << n->get_arg(1)->get_root()->get_owner_id() 
+            << ", val: " << get_assignment(enode2bool_var(n))
+            << ", lhs: #" << n->get_arg(0)->get_owner_id()
+            << ", rhs: #" << n->get_arg(1)->get_owner_id()
+            << ", lhs->root: #" << n->get_arg(0)->get_root()->get_owner_id()
+            << ", rhs->root: #" << n->get_arg(1)->get_root()->get_owner_id()
             << ", is_marked: " << n->is_marked()
-            << ", is_relevant: " << is_relevant(n) 
+            << ", is_relevant: " << is_relevant(n)
             << ", iscope_lvl: " << n->get_iscope_lvl() << "\n";
     }
 
@@ -354,7 +355,7 @@ namespace smt {
         enode_vector::iterator end = n->end_parents();
         for (; it != end; ++it) {
             enode * parent = *it;
-            if (parent->is_eq()) 
+            if (parent->is_eq())
                 display_eq_detail(out, parent);
         }
     }
@@ -447,7 +448,7 @@ namespace smt {
         g_lemma_id++;
     }
 
-    void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, 
+    void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
                                                unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
                                                literal consequent, const char * logic) const {
         ast_smt_pp pp(m_manager);
@@ -471,7 +472,7 @@ namespace smt {
         pp.display_smt2(out, n);
     }
 
-    void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, 
+    void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
                                                unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
                                                literal consequent, const char * logic) const {
         char buffer[BUFFER_SZ];
@@ -533,7 +534,7 @@ namespace smt {
             n->display_lbls(out);
         }
     }
-    
+
     void context::display_decl2enodes(std::ostream & out) const {
         out << "decl2enodes:\n";
         vector<enode_vector>::const_iterator it1  = m_decl2enodes.begin();
@@ -544,7 +545,7 @@ namespace smt {
                 out << "id " << id << " ->";
                 enode_vector::const_iterator it2  = v.begin();
                 enode_vector::const_iterator end2 = v.end();
-                for (; it2 != end2; ++it2) 
+                for (; it2 != end2; ++it2)
                     out << " #" << (*it2)->get_owner_id();
                 out << "\n";
             }
@@ -567,7 +568,7 @@ namespace smt {
                 out << std::right;
                 if (lit_internalized(n))
                     out << get_assignment(n);
-                else 
+                else
                     out << "l_undef";
             }
             if (e_internalized(n)) {
@@ -576,20 +577,13 @@ namespace smt {
             }
             out << "\n";
             if (is_app(n)) {
-                for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) 
+                for (unsigned i = 0; i < to_app(n)->get_num_args(); i++)
                     todo.push_back(to_app(n)->get_arg(i));
             }
         }
     }
-    
-    void context::trace_assign(literal l, b_justification j, bool decision) const {
-        SASSERT(m_manager.has_trace_stream());
-        std::ostream & out = m_manager.trace_stream();
-        out << "[assign] ";
-        display_literal(out, l);
-        if (decision)
-            out << " decision";
-        out << " ";
+
+    void context::display(std::ostream& out, b_justification j) const {
         switch (j.get_kind()) {
         case b_justification::AXIOM:
             out << "axiom";
@@ -597,8 +591,6 @@ namespace smt {
         case b_justification::BIN_CLAUSE: {
             literal l2 = j.get_literal();
             out << "bin-clause ";
-            display_literal(out, l);
-            out << " ";
             display_literal(out, l2);
             break;
         }
@@ -618,5 +610,16 @@ namespace smt {
         out << "\n";
     }
 
+    void context::trace_assign(literal l, b_justification j, bool decision) const {
+        SASSERT(m_manager.has_trace_stream());
+        std::ostream & out = m_manager.trace_stream();
+        out << "[assign] ";
+        display_literal(out, l);
+        if (decision)
+            out << " decision";
+        out << " ";
+        display(out, j);
+    }
+
 };
 
diff --git a/src/smt/smt_literal.cpp b/src/smt/smt_literal.cpp
index 05bf4d04b..d510027f0 100644
--- a/src/smt/smt_literal.cpp
+++ b/src/smt/smt_literal.cpp
@@ -69,10 +69,10 @@ namespace smt {
         }
     }
 
-    void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map) {
+    void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep) {
         for (unsigned i = 0; i < num_lits; i++) {
             if (i > 0)
-                out << " ";
+                out << sep;
             lits[i].display(out, m, bool_var2expr_map);
         }
     }
diff --git a/src/smt/smt_literal.h b/src/smt/smt_literal.h
index 0d8a62f20..3dbd6911e 100644
--- a/src/smt/smt_literal.h
+++ b/src/smt/smt_literal.h
@@ -103,7 +103,7 @@ namespace smt {
 
     void display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map);
 
-    void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map);
+    void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = " ");
 
     template<typename T>
     void neg_literals(unsigned num_lits, literal const * lits, T & result) {
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 661e7ab5b..1e0c7c5f4 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -218,7 +218,7 @@ namespace smt {
         typedef svector<enode_pair> eq_vector;
 
         // keep track of coefficients used for bounds for proof generation.
-        class antecedents {
+        class antecedents_t {
             literal_vector    m_lits;
             eq_vector         m_eqs;
             vector<numeral>   m_lit_coeffs;
@@ -233,16 +233,38 @@ namespace smt {
             void init();
 
         public:
-            antecedents(): m_init(false) {}
+            antecedents_t(): m_init(false) {}
             void reset();
-            literal_vector& lits() { return m_lits; }
-            eq_vector& eqs() { return m_eqs; }
+            literal_vector const& lits() const { return m_lits; }
+            eq_vector const& eqs() const { return m_eqs; }
             void push_lit(literal l, numeral const& r, bool proofs_enabled);
             void push_eq(enode_pair const& p, numeral const& r, bool proofs_enabled);
+            void append(unsigned sz, literal const* ls) { m_lits.append(sz, ls); }
+            void append(unsigned sz, enode_pair const* ps) { m_eqs.append(sz, ps); }
             unsigned num_params() const { return empty()?0:m_eq_coeffs.size() + m_lit_coeffs.size() + 1; }
             numeral const* lit_coeffs() const { return m_lit_coeffs.c_ptr(); }
             numeral const* eq_coeffs() const { return m_eq_coeffs.c_ptr(); }
             parameter* params(char const* name);
+            std::ostream& display(theory_arith& th, std::ostream& out) const;
+        };
+
+        class antecedents {
+            theory_arith& th;
+            antecedents_t&  a;
+        public:
+            antecedents(theory_arith& th);
+            ~antecedents();  
+            literal_vector const& lits() const { return a.lits(); }
+            eq_vector const& eqs() const { return a.eqs(); }
+            void push_lit(literal l, numeral const& r, bool e) { a.push_lit(l, r, e); }
+            void push_eq(enode_pair const& p, numeral const& r, bool e) { a.push_eq(p, r, e); }
+            void append(unsigned sz, literal const* ls) { a.append(sz, ls); }
+            void append(unsigned sz, enode_pair const* ps) { a.append(sz, ps); }
+            unsigned num_params() const { return a.num_params(); }
+            numeral const* lit_coeffs() const { return a.lit_coeffs(); }
+            numeral const* eq_coeffs() const { return a.eq_coeffs(); }
+            parameter* params(char const* name) { return a.params(name); }
+            std::ostream& display(std::ostream& out) const { return a.display(th, out); }
         };
 
         class gomory_cut_justification;
@@ -324,11 +346,14 @@ namespace smt {
         public:
             derived_bound(theory_var v, inf_numeral const & val, bound_kind k):bound(v, val, k, false) {}
             virtual ~derived_bound() {}
+            literal_vector const& lits() const { return m_lits; }
+            eq_vector const& eqs() const { return m_eqs; }
             virtual bool has_justification() const { return true; }
             virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled); 
             virtual void push_lit(literal l, numeral const&) { m_lits.push_back(l); }
             virtual void push_eq(enode_pair const& p, numeral const&) { m_eqs.push_back(p); }
             virtual void display(theory_arith const& th, std::ostream& out) const;
+            
         };
     
         class justified_derived_bound : public derived_bound {
@@ -460,8 +485,8 @@ namespace smt {
 
         svector<scope>          m_scopes;
         literal_vector          m_tmp_literal_vector2;
-        antecedents             m_tmp_antecedents;
-        antecedents             m_tmp_antecedents2;
+        antecedents_t           m_antecedents[3];
+        unsigned                m_antecedents_index;
 
         struct var_value_hash;
         friend struct var_value_hash;
@@ -506,6 +531,8 @@ namespace smt {
         bool relax_bounds() const { return m_params.m_arith_stronger_lemmas; }
         bool skip_big_coeffs() const { return m_params.m_arith_skip_rows_with_big_coeffs; }
         bool dump_lemmas() const { return m_params.m_arith_dump_lemmas; }
+        void dump_lemmas(literal l, antecedents const& ante);
+        void dump_lemmas(literal l, derived_bound const& ante);
         bool process_atoms() const;
         unsigned get_num_conflicts() const { return m_num_conflicts; }
         var_kind get_var_kind(theory_var v) const { return m_data[v].kind(); }
@@ -750,7 +777,7 @@ namespace smt {
         void explain_bound(row const & r, int idx, bool lower, inf_numeral & delta, 
                            antecedents & antecedents);
         void mk_implied_bound(row const & r, unsigned idx, bool lower, theory_var v, bound_kind kind, inf_numeral const & k);
-        void assign_bound_literal(literal l, row const & r, unsigned idx, bool lower, inf_numeral & delta, antecedents& antecedents);
+        void assign_bound_literal(literal l, row const & r, unsigned idx, bool lower, inf_numeral & delta);
         void propagate_bounds();
 
         // -----------------------------------
@@ -836,7 +863,9 @@ namespace smt {
         // Justification
         //
         // -----------------------------------
-        void set_conflict(unsigned num_literals, literal const * lits, unsigned num_eqs, enode_pair const * eqs, antecedents& antecedents, bool is_lia, char const* proof_rule);
+        void set_conflict(unsigned num_literals, literal const * lits, unsigned num_eqs, enode_pair const * eqs, antecedents& antecedents, char const* proof_rule);
+        void set_conflict(antecedents const& ante, antecedents& bounds, char const* proof_rule);
+        void set_conflict(derived_bound const& ante, antecedents& bounds, char const* proof_rule);
         void collect_fixed_var_justifications(row const & r, antecedents& antecedents) const;
         
         // -----------------------------------
@@ -989,7 +1018,7 @@ namespace smt {
         gb_result compute_grobner(svector<theory_var> const & nl_cluster);
         bool max_min_nl_vars();
         final_check_status process_non_linear();
-        antecedents&            get_antecedents();
+        
 
         // -----------------------------------
         //
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 581fbb4df..e2a2d48a6 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -316,7 +316,7 @@ namespace smt {
     // -----------------------------------
 
     template<typename Ext>
-    void theory_arith<Ext>::antecedents::init() {
+    void theory_arith<Ext>::antecedents_t::init() {
         if (!m_init && !empty()) {
             m_params.push_back(parameter(symbol("unknown-arith")));
             for (unsigned i = 0; i < m_lits.size(); i++) {
@@ -330,7 +330,7 @@ namespace smt {
     }
 
     template<typename Ext>
-    void theory_arith<Ext>::antecedents::reset() { 
+    void theory_arith<Ext>::antecedents_t::reset() { 
         m_init = false; 
         m_eq_coeffs.reset();
         m_lit_coeffs.reset();
@@ -340,7 +340,7 @@ namespace smt {
     }
 
     template<typename Ext>
-    void theory_arith<Ext>::antecedents::push_lit(literal l, numeral const& r, bool proofs_enabled) { 
+    void theory_arith<Ext>::antecedents_t::push_lit(literal l, numeral const& r, bool proofs_enabled) { 
         m_lits.push_back(l);
         if (proofs_enabled) {
             m_lit_coeffs.push_back(r); 
@@ -348,7 +348,7 @@ namespace smt {
     }
 
     template<typename Ext>
-    void theory_arith<Ext>::antecedents::push_eq(enode_pair const& p, numeral const& r, bool proofs_enabled) { 
+    void theory_arith<Ext>::antecedents_t::push_eq(enode_pair const& p, numeral const& r, bool proofs_enabled) { 
         m_eqs.push_back(p);
         if (proofs_enabled) {
             m_eq_coeffs.push_back(r); 
@@ -356,7 +356,7 @@ namespace smt {
     }
 
     template<typename Ext>
-    parameter * theory_arith<Ext>::antecedents::params(char const* name) {
+    parameter * theory_arith<Ext>::antecedents_t::params(char const* name) {
         if (empty()) return 0;
         init();
         m_params[0] = parameter(symbol(name));
@@ -740,8 +740,8 @@ namespace smt {
             }
         }
         else {
-            a.lits().append(m_lits.size(), m_lits.c_ptr());
-            a.eqs().append(m_eqs.size(), m_eqs.c_ptr());
+            a.append(m_lits.size(), m_lits.c_ptr());
+            a.append(m_eqs.size(), m_eqs.c_ptr());
         }
     }
 
@@ -804,8 +804,7 @@ namespace smt {
     */
     template<typename Ext>
     void theory_arith<Ext>::accumulate_justification(bound & b, derived_bound& new_bound, numeral const& coeff, literal_idx_set & lits, eq_set & eqs) {
-        antecedents& ante = m_tmp_antecedents;
-        ante.reset();
+        antecedents ante(*this);
         b.push_justification(ante, coeff, proofs_enabled());
         unsigned num_lits = ante.lits().size();
         for (unsigned i = 0; i < num_lits; ++i) {
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 8b2f9b780..96fe2d1f8 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -349,7 +349,6 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::mk_axiom(expr * ante, expr * conseq) {
         ast_manager & m = get_manager();
-        TRACE("arith_axiom", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n";);
         context & ctx   = get_context();
         simplifier & s  = ctx.get_simplifier();
         expr_ref s_ante(m), s_conseq(m);
@@ -371,6 +370,9 @@ namespace smt {
         literal l_conseq = ctx.get_literal(s_conseq);
         if (negated) l_conseq.neg();
 
+        TRACE("arith_axiom", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n";
+              tout << s_ante << "\n" << s_conseq << "\n";);
+
         literal lits[2] = {l_ante, l_conseq};
         ctx.mk_th_axiom(get_id(), 2, lits);
         if (ctx.relevancy()) {
@@ -394,12 +396,12 @@ namespace smt {
     void theory_arith<Ext>::mk_div_axiom(expr * p, expr * q) {
         if (!m_util.is_zero(q)) {
             ast_manager & m    = get_manager();
+            expr_ref div(m), zero(m), eqz(m), eq(m);
             TRACE("div_axiom_bug", tout << "expanding div_axiom for: " << mk_pp(p, m) << " / " << mk_pp(q, m) << "\n";); 
-            expr * div         = m_util.mk_div(p, q);
-            expr * zero        = m_util.mk_numeral(rational(0), false);
-            expr_ref eqz(m), eq(m);
-            eqz                = m.mk_eq(q, zero);
-            eq                 = m.mk_eq(m_util.mk_mul(q, div), p);
+            div         = m_util.mk_div(p, q);
+            zero        = m_util.mk_numeral(rational(0), false);
+            eqz         = m.mk_eq(q, zero);
+            eq          = m.mk_eq(m_util.mk_mul(q, div), p);
             TRACE("div_axiom_bug", tout << "eqz: " << mk_pp(eqz, m) << "\neq: " << mk_pp(eq, m) << "\n";);
             mk_axiom(eqz, eq);
         }
@@ -410,15 +412,21 @@ namespace smt {
         if (!m_util.is_zero(divisor)) {
             // if divisor is zero, then idiv and mod are uninterpreted functions.
             ast_manager & m = get_manager();
-            expr * div         = m_util.mk_idiv(dividend, divisor);
-            expr * mod         = m_util.mk_mod(dividend, divisor);
-            expr * zero        = m_util.mk_numeral(rational(0), true);
-            expr * abs_divisor = m.mk_ite(m_util.mk_lt(divisor, zero), m_util.mk_sub(zero, divisor), divisor);
+            expr_ref div(m), mod(m), zero(m), abs_divisor(m);
             expr_ref eqz(m), eq(m), lower(m), upper(m);
-            eqz                = m.mk_eq(divisor, zero);
-            eq                 = m.mk_eq(m_util.mk_add(m_util.mk_mul(divisor, div), mod), dividend);
-            lower              = m_util.mk_le(zero, mod);
-            upper              = m_util.mk_lt(mod, abs_divisor);
+            div         = m_util.mk_idiv(dividend, divisor);
+            mod         = m_util.mk_mod(dividend, divisor);
+            zero        = m_util.mk_numeral(rational(0), true);
+            abs_divisor = m.mk_ite(m_util.mk_lt(divisor, zero), m_util.mk_sub(zero, divisor), divisor);
+            eqz         = m.mk_eq(divisor, zero);
+            eq          = m.mk_eq(m_util.mk_add(m_util.mk_mul(divisor, div), mod), dividend);
+            lower       = m_util.mk_le(zero, mod);
+            upper       = m_util.mk_lt(mod, abs_divisor);
+            TRACE("div_axiom_bug", 
+                  tout << "eqz:   " << mk_pp(eqz, m) << "\neq: " << mk_pp(eq, m) << "\n";
+                  tout << "lower: " << mk_pp(lower, m) << "\n";
+                  tout << "upper: " << mk_pp(upper, m) << "\n";);
+
             mk_axiom(eqz, eq);
             mk_axiom(eqz, lower);
             mk_axiom(eqz, upper);
@@ -814,6 +822,7 @@ namespace smt {
     void theory_arith<Ext>::mk_bound_axioms(atom * a1) {
         theory_var v = a1->get_var();
         atoms & occs = m_var_occs[v];
+        //SASSERT(v != 15);
         TRACE("mk_bound_axioms", tout << "add bound axioms for v" << v << " " << a1 << "\n";);
         if (!get_context().is_searching()) {
             //
@@ -937,6 +946,8 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::flush_bound_axioms() {
+        CTRACE("arith", !m_new_atoms.empty(), tout << "flush bound axioms\n";);
+
         while (!m_new_atoms.empty()) {
             ptr_vector<atom> atoms;            
             atoms.push_back(m_new_atoms.back());
@@ -950,6 +961,10 @@ namespace smt {
                     --i;
                 }
             }            
+            TRACE("arith", 
+                  for (unsigned i = 0; i < atoms.size(); ++i) {
+                      atoms[i]->display(*this, tout);
+                  });
             ptr_vector<atom> occs(m_var_occs[v]);
 
             std::sort(atoms.begin(), atoms.end(), compare_atoms());
@@ -1140,7 +1155,7 @@ namespace smt {
     
     template<typename Ext>
     void theory_arith<Ext>::assign_eh(bool_var v, bool is_true) {
-        TRACE("arith", tout << "v" << v << " " << is_true << "\n";);
+        TRACE("arith", tout << "p" << v << " := " << (is_true?"true":"false") << "\n";);
         atom * a = get_bv2a(v);
         if (!a) return;
         SASSERT(get_context().get_assignment(a->get_bool_var()) != l_undef);
@@ -1299,28 +1314,6 @@ namespace smt {
     final_check_status theory_arith<Ext>::final_check_eh() {
         TRACE("arith_eq_adapter_info", m_arith_eq_adapter.display_already_processed(tout););
         TRACE("arith_final_check", display(tout););
-#if 0
-        if (true /*m_params.m_smtlib_dump_lemmas*/) {
-            literal_buffer tmp;
-
-            for (unsigned i = 0; i < m_asserted_qhead; i++) {
-                bound * b = m_asserted_bounds[i];
-                if (b->is_atom()) {
-                    atom* a = static_cast<atom*>(b);
-                    bool_var bv = a->get_bool_var();
-                    lbool is_true = get_context().get_assignment(bv);
-                    if (is_true == l_true) {
-                        tmp.push_back(literal(bv));
-                    }
-                    else if (is_true == l_false) {
-                        tmp.push_back(~literal(bv));
-                    }                    
-                }
-            }
-                       
-            get_context().display_lemma_as_smt_problem(tmp.size(), tmp.c_ptr(), false_literal, "QF_LIA");
-        }
-#endif
 
         if (!propagate_core()) 
             return FC_CONTINUE; 
@@ -1530,6 +1523,7 @@ namespace smt {
         m_branch_cut_counter(0),
         m_eager_gcd(m_params.m_arith_eager_gcd),
         m_final_check_idx(0),
+        m_antecedents_index(0),
         m_var_value_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
         m_liberal_final_check(true),
         m_changed_assignment(false),
@@ -2207,15 +2201,15 @@ namespace smt {
             }
         }
 
-        TRACE("sign_row_conflict", tout << "v" << x_i << " is_below: " << is_below << " delta: " << delta << "\n"; display_var(tout, x_i);
-              tout << "is_below_lower: " << below_lower(x_i) << ", is_above_upper: " << above_upper(x_i) << "\n";);
-        antecedents& ante = get_antecedents();
+        antecedents ante(*this);
         explain_bound(r, idx, !is_below, delta, ante);
         b->push_justification(ante, numeral(1), coeffs_enabled());
        
+        TRACE("sign_row_conflict", tout << "v" << x_i << " is_below: " << is_below << " delta: " << delta << "\n"; display_var(tout, x_i);
+              tout << "is_below_lower: " << below_lower(x_i) << ", is_above_upper: " << above_upper(x_i) << "\n";
+              ante.display(tout););
 
-        set_conflict(ante.lits().size(), ante.lits().c_ptr(), 
-                     ante.eqs().size(), ante.eqs().c_ptr(), ante, is_int(x_i), "farkas");
+        set_conflict(ante, ante, "farkas");
         // display_bounds_in_smtlib();
     }
 
@@ -2353,11 +2347,11 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::sign_bound_conflict(bound * b1, bound * b2) {
         SASSERT(b1->get_var() == b2->get_var());
-        antecedents& ante = get_antecedents();
+        antecedents ante(*this);
         b1->push_justification(ante, numeral(1), coeffs_enabled());
         b2->push_justification(ante, numeral(1), coeffs_enabled());
 
-        set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, is_int(b1->get_var()), "farkas");
+        set_conflict(ante, ante, "farkas");
         TRACE("arith_conflict", tout << "bound conflict v" << b1->get_var() << "\n";
               tout << "bounds: " << b1 << " " << b2 << "\n";);
     }
@@ -2595,7 +2589,6 @@ namespace smt {
         if (!relax_bounds() && (!ante.lits().empty() || !ante.eqs().empty()))
             return;
         context & ctx = get_context();
-        ante.reset();   // !!!!TBD: should equality ante also be reset here!!!!
         row_entry const & entry = r[idx];
         numeral           coeff = entry.m_coeff; 
         if (relax_bounds()) {
@@ -2700,7 +2693,6 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::mk_implied_bound(row const & r, unsigned idx, bool is_lower, theory_var v, bound_kind kind, inf_numeral const & k) {
         atoms const & as                 = m_var_occs[v];
-        antecedents& ante                = get_antecedents();
         inf_numeral const & epsilon      = get_epsilon(v);
         inf_numeral delta;
         typename atoms::const_iterator     it  = as.begin();
@@ -2721,7 +2713,7 @@ namespace smt {
                         }
                         TRACE("propagate_bounds", tout << "v" << v << " >= " << k << ", v" << v << " >= " << k2 << ", delta: " << delta << "\n"; 
                               display_row(tout, r););
-                        assign_bound_literal(l, r, idx, is_lower, delta, ante);
+                        assign_bound_literal(l, r, idx, is_lower, delta);
                     }
                     // v <= k  k <  k2  |-  v < k2  |- not v >= k2
                     if (kind == B_UPPER && k <  k2) {
@@ -2737,7 +2729,7 @@ namespace smt {
                         if (delta.is_nonneg()) {
                             TRACE("propagate_bounds", tout << "v" << v << " <= " << k << ", not v" << v << " >= " << k2 << ", delta: " << delta << "\n"; 
                                   display_row(tout, r););
-                            assign_bound_literal(~l, r, idx, is_lower, delta, ante);
+                            assign_bound_literal(~l, r, idx, is_lower, delta);
                         }
                     }
                 }
@@ -2752,7 +2744,7 @@ namespace smt {
                         if (delta.is_nonneg()) {
                             TRACE("propagate_bounds", tout << "v" << v << " >= " << k << ", not v" << v << " <= " << k2 << ", delta: " << delta << "\n"; 
                                   display_row(tout, r););
-                            assign_bound_literal(~l, r, idx, is_lower, delta, ante);
+                            assign_bound_literal(~l, r, idx, is_lower, delta);
                         }
                     }
                     // v <= k  k <= k2 |-  v <= k2 
@@ -2763,7 +2755,7 @@ namespace smt {
                         }
                         TRACE("propagate_bounds", tout << "v" << v << " <= " << k << ", v" << v << " <= " << k2 << ", delta: " << delta << "\n"; 
                               display_row(tout, r););
-                        assign_bound_literal(l, r, idx, is_lower, delta, ante);
+                        assign_bound_literal(l, r, idx, is_lower, delta);
                     }
                 }
             }
@@ -2771,28 +2763,34 @@ namespace smt {
     }
 
     template<typename Ext>
-    void theory_arith<Ext>::assign_bound_literal(literal l, row const & r, unsigned idx, bool is_lower, inf_numeral & delta, antecedents& ante) {
+    void theory_arith<Ext>::dump_lemmas(literal l, antecedents const& ante) {
+        context & ctx = get_context();
+        if (dump_lemmas()) {
+            TRACE("arith", ante.display(tout) << " --> "; ctx.display_detailed_literal(tout, l); tout << "\n";);
+            ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(), 
+                                             ante.eqs().size(), ante.eqs().c_ptr(), l, 0);
+        }
+    }
+
+    template<typename Ext>
+    void theory_arith<Ext>::dump_lemmas(literal l, derived_bound const& ante) {
+        context & ctx = get_context();
+        if (dump_lemmas()) {
+            ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(), 
+                                             ante.eqs().size(), ante.eqs().c_ptr(), l, 0);
+        }
+    }
+
+    template<typename Ext>
+    void theory_arith<Ext>::assign_bound_literal(literal l, row const & r, unsigned idx, bool is_lower, inf_numeral & delta) {
         m_stats.m_bound_props++;
         context & ctx = get_context();
+        antecedents ante(*this);
         explain_bound(r, idx, is_lower, delta, ante);
-        if (dump_lemmas()) {
-            char const * logic = is_int(r.get_base_var()) ? "QF_LIA" : "QF_LRA";
-            ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(), 
-                                             ante.eqs().size(), ante.eqs().c_ptr(), l, logic);
-        }
+        dump_lemmas(l, ante);
+        
         TRACE("propagate_bounds", 
-              literal_vector::const_iterator it  = ante.lits().begin();
-              literal_vector::const_iterator end = ante.lits().end();
-              for (; it != end; ++it) {
-                  ctx.display_detailed_literal(tout, *it);
-                  tout << " ";
-              }
-              eq_vector::const_iterator it2  = ante.eqs().begin();
-              eq_vector::const_iterator end2 = ante.eqs().end();
-              for (; it2 != end2; ++it2) {
-                  tout << "#" << it2->first->get_owner_id() << "=#" << it2->second->get_owner_id() << " ";
-              }
-              tout << " --> ";
+              ante.display(tout) << " --> ";
               ctx.display_detailed_literal(tout, l); 
               tout << "\n";);
         if (ante.lits().size() < small_lemma_size() && ante.eqs().empty()) {
@@ -2874,19 +2872,26 @@ namespace smt {
     // Justification
     //
     // -----------------------------------
+
+    template<typename Ext>
+    void theory_arith<Ext>::set_conflict(antecedents const& ante, antecedents& bounds, char const* proof_rule) {
+        dump_lemmas(false_literal, ante);
+        set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), bounds, proof_rule);
+    }
+
+    template<typename Ext>
+    void theory_arith<Ext>::set_conflict(derived_bound const& ante, antecedents& bounds, char const* proof_rule) {
+        dump_lemmas(false_literal, ante);
+        set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), bounds, proof_rule);
+    }
     
     template<typename Ext>
-        void theory_arith<Ext>::set_conflict(unsigned num_literals, literal const * lits, unsigned num_eqs, enode_pair const * eqs, 
-                                             antecedents& bounds, bool is_lia, char const* proof_rule) {
+    void theory_arith<Ext>::set_conflict(unsigned num_literals, literal const * lits, unsigned num_eqs, enode_pair const * eqs, 
+                                         antecedents& bounds, char const* proof_rule) {
         SASSERT(num_literals != 0 || num_eqs != 0);
         context & ctx = get_context();
         m_stats.m_conflicts++;
         m_num_conflicts++;
-        if (dump_lemmas()) {
-            char const * logic = is_lia ? "QF_LIA" : "QF_LRA";
-            ctx.display_lemma_as_smt_problem(num_literals, lits, num_eqs, eqs, false_literal, logic);
-        }
-        region & r    = ctx.get_region();
         TRACE("arith_conflict", 
               for (unsigned i = 0; i < num_literals; i++) {
                   ctx.display_detailed_literal(tout, lits[i]);
@@ -2908,7 +2913,7 @@ namespace smt {
         record_conflict(num_literals, lits, num_eqs, eqs, bounds.num_params(), bounds.params(proof_rule));
         ctx.set_conflict(
             ctx.mk_justification(
-                ext_theory_conflict_justification(get_id(), r, num_literals, lits, num_eqs, eqs, 
+                ext_theory_conflict_justification(get_id(), ctx.get_region(), num_literals, lits, num_eqs, eqs, 
                                                   bounds.num_params(), bounds.params(proof_rule))));
     }
 
@@ -3320,11 +3325,20 @@ namespace smt {
     */
 
     template<typename Ext>
-    typename theory_arith<Ext>::antecedents& theory_arith<Ext>::get_antecedents() { 
-        m_tmp_antecedents.reset(); 
-        return m_tmp_antecedents; 
+    theory_arith<Ext>::antecedents::antecedents(theory_arith& th):
+        th(th),
+        a(th.m_antecedents[th.m_antecedents_index]) {
+        SASSERT(th.m_antecedents_index < 3);
+        a.reset();
+        ++th.m_antecedents_index;
     }
 
+    template<typename Ext>
+    theory_arith<Ext>::antecedents::~antecedents() {
+        --th.m_antecedents_index;
+    }
+
+
 };
 
 #endif /* THEORY_ARITH_CORE_H_ */
diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h
index 80b13050d..7e61b968e 100644
--- a/src/smt/theory_arith_eq.h
+++ b/src/smt/theory_arith_eq.h
@@ -52,7 +52,7 @@ namespace smt {
                 // contain invalid (key -> value) pairs. So, we must check whether v2 is really equal to val (previous test) AND it has
                 // the same sort of v. The following test was missing in a previous version of Z3. 
                 if (!is_equal(v, v2) && is_int(v) == is_int(v2)) {
-                    antecedents& ante = get_antecedents();
+                    antecedents ante(*this);
 
                     //
                     // v <= k <= v2  => v <= v2
@@ -241,7 +241,7 @@ namespace smt {
                     is_int(x) == is_int(x2) &&
                     !is_equal(x, x2)) {
 
-                    antecedents& ante = get_antecedents(); 
+                    antecedents ante(*this);
                     collect_fixed_var_justifications(r, ante);
 
                     //
@@ -256,7 +256,7 @@ namespace smt {
 
             if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int(x) == is_int(y)) {
                 // found equality x = y
-                antecedents& ante = get_antecedents(); 
+                antecedents ante(*this);
                 collect_fixed_var_justifications(r, ante);
                 TRACE("propagate_cheap_eq", tout << "propagate eq using x-y=0 row:\n"; display_row_info(tout, r););
                 m_stats.m_offset_eqs++;
@@ -296,7 +296,7 @@ namespace smt {
                     if (new_eq) {
                         if (!is_equal(x, x2) && is_int(x) == is_int(x2)) {
                             SASSERT(y == y2 && k == k2);
-                            antecedents& ante = get_antecedents();                             
+                            antecedents ante(*this);
                             collect_fixed_var_justifications(r, ante);
                             collect_fixed_var_justifications(r2, ante);
                             TRACE("propagate_cheap_eq", tout << "propagate eq two rows:\n"; 
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index d0493b274..30ae6feac 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -201,12 +201,13 @@ namespace smt {
         SASSERT(is_int(v));
         SASSERT(!get_value(v).is_int());
         m_stats.m_branches++;
-        TRACE("arith_branching", tout << "branching v" << v << " = " << get_value(v) << "\n";
+        TRACE("arith_int", tout << "branching v" << v << " = " << get_value(v) << "\n";
               display_var(tout, v););
         numeral k     = ceil(get_value(v));
         rational _k   = k.to_rational();
-        expr * bound  = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(_k, true));
-        TRACE("arith_branching", tout << mk_bounded_pp(bound, get_manager()) << "\n";);
+        expr_ref bound(get_manager());
+        bound  = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(_k, true));
+        TRACE("arith_int", tout << mk_bounded_pp(bound, get_manager()) << "\n";);
         context & ctx = get_context();
         ctx.internalize(bound, true);
         ctx.mark_as_relevant(bound);
@@ -452,11 +453,11 @@ namespace smt {
         expr_ref pol(m);
         pol = m_util.mk_add(_args.size(), _args.c_ptr());
         result = m_util.mk_ge(pol, m_util.mk_numeral(k, all_int));
-        TRACE("arith_mk_polynomial", tout << "before simplification:\n" << mk_pp(pol, m) << "\n";);
+        TRACE("arith_mk_polynomial", tout << "before simplification:\n" << result << "\n";);
         simplifier & s = get_context().get_simplifier();
         proof_ref pr(m);
         s(result, result, pr);
-        TRACE("arith_mk_polynomial", tout << "after simplification:\n" << mk_pp(pol, m) << "\n";);
+        TRACE("arith_mk_polynomial", tout << "after simplification:\n" << result << "\n";);
         SASSERT(is_well_sorted(get_manager(), result));
     }
 
@@ -498,7 +499,7 @@ namespace smt {
 
         TRACE("gomory_cut", tout << "applying cut at:\n"; display_row_info(tout, r););
         
-        antecedents& ante = get_antecedents();
+        antecedents ante(*this);
 
         m_stats.m_gomory_cuts++;
 
@@ -508,6 +509,8 @@ namespace smt {
         
         numeral f_0  = Ext::fractional_part(m_value[x_i]);
         numeral one_minus_f_0 = numeral(1) - f_0; 
+        SASSERT(!f_0.is_zero());
+        SASSERT(!one_minus_f_0.is_zero());
         
         numeral lcm_den(1);
         unsigned num_ints = 0;
@@ -521,36 +524,30 @@ namespace smt {
                 a_ij.neg();  // make the used format compatible with the format used in: Integrating Simplex with DPLL(T)
                 if (is_real(x_j)) {
                     numeral new_a_ij;
-                    TRACE("gomory_cut_detail", tout << a_ij << "*v" << x_j << "\n";);
                     if (at_lower(x_j)) {
                         if (a_ij.is_pos()) {
                             new_a_ij  =  a_ij / one_minus_f_0;
                         }
                         else {
-                            TRUSTME(!f_0.is_zero());
                             new_a_ij  =  a_ij / f_0;
                             new_a_ij.neg();
                         }
-                        // k += new_a_ij * lower_bound(x_j).get_rational();
                         k.addmul(new_a_ij, lower_bound(x_j).get_rational());
                         lower(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
                     }
                     else {
                         SASSERT(at_upper(x_j));
                         if (a_ij.is_pos()) {
-                            TRUSTME(!f_0.is_zero());
                             new_a_ij =   a_ij / f_0; 
                             new_a_ij.neg(); // the upper terms are inverted.
                         }
                         else {
-                            // new_a_ij = - a_ij / one_minus_f_0
-                            // new_a_ij.neg() // the upper terms are inverted
-                            new_a_ij =   a_ij / one_minus_f_0;  
+                            new_a_ij =   a_ij / one_minus_f_0; 
                         }
-                        // k += new_a_ij * upper_bound(x_j).get_rational();
                         k.addmul(new_a_ij, upper_bound(x_j).get_rational());
                         upper(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
                     }
+                    TRACE("gomory_cut_detail", tout << a_ij << "*v" << x_j << " k: " << k << "\n";);
                     pol.push_back(row_entry(new_a_ij, x_j));
                 }
                 else {
@@ -572,7 +569,6 @@ namespace smt {
                             else {
                                 new_a_ij = (numeral(1) - f_j) / f_0;
                             }
-                            // k += new_a_ij * lower_bound(x_j).get_rational();
                             k.addmul(new_a_ij, lower_bound(x_j).get_rational());
                             lower(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
                         }
@@ -585,11 +581,10 @@ namespace smt {
                                 new_a_ij = (numeral(1) - f_j) / one_minus_f_0;
                             }
                             new_a_ij.neg(); // the upper terms are inverted
-                            // k += new_a_ij * upper_bound(x_j).get_rational();
                             k.addmul(new_a_ij, upper_bound(x_j).get_rational());
                             upper(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
                         }
-                        TRACE("gomory_cut_detail", tout << "new_a_ij: " << new_a_ij << "\n";);
+                        TRACE("gomory_cut_detail", tout << "new_a_ij: " << new_a_ij << " k: " << k << "\n";);
                         pol.push_back(row_entry(new_a_ij, x_j));
                         lcm_den = lcm(lcm_den, denominator(new_a_ij));
                     }
@@ -603,7 +598,7 @@ namespace smt {
         if (pol.empty()) {
             SASSERT(k.is_pos());
             // conflict 0 >= k where k is positive
-            set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, true, "gomory-cut");
+            set_conflict(ante, ante, "gomory-cut");
             return true;
         }
         else if (pol.size() == 1) {
@@ -639,18 +634,19 @@ namespace smt {
                 }
                 TRACE("gomory_cut_detail", tout << "after *lcm\n";
                       for (unsigned i = 0; i < pol.size(); i++) {
-                          tout << pol[i].m_coeff << " " << pol[i].m_var << "\n";
+                          tout << pol[i].m_coeff << " * v" << pol[i].m_var << "\n";
                       }
                       tout << "k: " << k << "\n";);
             }
             mk_polynomial_ge(pol.size(), pol.c_ptr(), k.to_rational(), bound);            
         }
-        TRACE("gomory_cut", tout << "new cut:\n" << mk_pp(bound, get_manager()) << "\n";);
+        TRACE("gomory_cut", tout << "new cut:\n" << bound << "\n"; ante.display(tout););
         literal l     = null_literal;
         context & ctx = get_context();
         ctx.internalize(bound, true);
         l = ctx.get_literal(bound);
         ctx.mark_as_relevant(l);
+        dump_lemmas(l, ante);
         ctx.assign(l, ctx.mk_justification(
                        gomory_cut_justification(
                            get_id(), ctx.get_region(), 
@@ -721,7 +717,7 @@ namespace smt {
 
         if (!(consts / gcds).is_int()) {
             TRACE("gcd_test", tout << "row failed the GCD test:\n"; display_row_info(tout, r););
-            antecedents& ante = get_antecedents();
+            antecedents ante(*this);
             collect_fixed_var_justifications(r, ante);
             context & ctx         = get_context();
             ctx.set_conflict(
@@ -754,7 +750,7 @@ namespace smt {
         numeral l(consts);
         numeral u(consts);
 
-        antecedents& ante = get_antecedents();
+        antecedents ante(*this);
 
 
         typename vector<row_entry>::const_iterator it  = r.begin_entries();
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 33efb4fcc..982aa963f 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -1910,11 +1910,10 @@ namespace smt {
     */
     template<typename Ext>
     void theory_arith<Ext>::set_conflict(v_dependency * d) {
-        bool is_lia = false; // TODO: fix it, but this is only used for debugging.
-        antecedents& ante = get_antecedents();
+        antecedents ante(*this);
         derived_bound  b(null_theory_var, inf_numeral(0), B_LOWER);
         dependency2new_bound(d, b);
-        set_conflict(b.m_lits.size(), b.m_lits.c_ptr(), b.m_eqs.size(), b.m_eqs.c_ptr(), ante, is_lia, "arith_nl");
+        set_conflict(b, ante, "arith_nl");
         TRACE("non_linear", 
               for (unsigned i = 0; i < b.m_lits.size(); ++i) {
                   tout << b.m_lits[i] << " ";
diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h
index db0a9dd39..ea4581925 100644
--- a/src/smt/theory_arith_pp.h
+++ b/src/smt/theory_arith_pp.h
@@ -399,6 +399,18 @@ namespace smt {
         out << "\n";
     }
 
+    template<typename Ext>
+    std::ostream& theory_arith<Ext>::antecedents_t::display(theory_arith& th, std::ostream & out) const {
+        th.get_context().display_literals_verbose(out, lits().size(), lits().c_ptr());
+        if (!lits().empty()) out << "\n";
+        ast_manager& m = th.get_manager();
+        for (unsigned i = 0; i < m_eqs.size(); ++i) {
+            out << mk_pp(m_eqs[i].first->get_owner(), m) << " ";
+            out << mk_pp(m_eqs[i].second->get_owner(), m) << "\n";            
+        }
+        return out;
+    }
+
     template<typename Ext>
     void theory_arith<Ext>::display_deps(std::ostream & out, v_dependency* dep) {
         ptr_vector<void> bounds;
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index 5c36a2d82..cf06b27be 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -204,7 +204,7 @@ struct scoped_timer::imp {
             throw default_exception("failed to destroy pthread attributes object");
 #elif defined(_LINUX_) || defined(_FREEBSD_)
     // Linux & FreeBSD
-    timer_delete(m_timerid);
+        timer_delete(m_timerid);
 #else
     // Other Platforms
 #endif