diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index c1d903631..490a5a90e 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -510,6 +510,9 @@ namespace smt {
 #else
         strm << "lemma_" << (++m_lemma_id) << ".smt2";
 #endif
+        if (m_lemma_id == 1303) {
+            verbose_stream() << "lemma\n";
+        }
         return strm.str();
     }
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 0271bcf44..d5c0b6610 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -354,6 +354,7 @@ class theory_lra::imp {
         
         enode* e = mk_enode(n);
         theory_var v = e->get_th_var(get_id());
+        TRACE("add_bug", tout << mk_pp(n, m) << " - v" << v << "\n");
         if (v == null_theory_var) 
             v = internalize_linearized_def(n, st);        
         return v;
@@ -372,8 +373,10 @@ class theory_lra::imp {
             }
         }
 
-        if (a.is_extended_numeral(arg, val)) 
-            st.add(internalize_numeral(arg, val), sign);        
+        if (a.is_extended_numeral(arg, val)) {
+            st.add(internalize_numeral(arg, val), sign);
+            return;
+        }
         else if (a.is_mul(arg, arg1, arg2)) {
             if (a.is_extended_numeral(arg2, val)) 
                 std::swap(arg1, arg2);
@@ -386,8 +389,7 @@ class theory_lra::imp {
                 return;
             }
         }
-        else 
-            st.add(internalize_term_core(arg), sign);
+        st.add(internalize_term_core(arg), sign);
     }
 
     theory_var internalize_numeral(app* n, rational const& val) {
@@ -508,7 +510,7 @@ class theory_lra::imp {
             return mk_var(n);
         ctx().internalize(n->get_arg(0), false);
         ctx().internalize(n->get_arg(1), false);
-        enode* e = mk_enode(n);
+        mk_enode(n);
         return mk_var(n);
     }
 
@@ -2852,9 +2854,9 @@ public:
             CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
             updt_unassigned_bounds(v, -1);
             TRACE("arith",
-                  ctx().display_literals_verbose(tout, m_core);
+                  ctx().display_literals_smt2(tout, m_core);
                   tout << "\n --> ";
-                  ctx().display_literal_verbose(tout, lit);
+                  ctx().display_literal_smt2(tout, lit);
                   tout << "\n";
                   display_evidence(tout, m_explanation);
                   lp().print_implied_bound(be, tout);
diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp
index ddddfbc00..b6370f153 100644
--- a/src/smt/theory_special_relations.cpp
+++ b/src/smt/theory_special_relations.cpp
@@ -888,9 +888,14 @@ namespace smt {
 
         func_decl* memf, *nextf, *connectedf;
 
+        std::string member, next, connected_sym;
+        unsigned index = r.decl()->get_parameter(0).get_int();
+        member = "member" + std::to_string(index);
+        next = "next" + std::to_string(index);
+        connected_sym = "connected" + std::to_string(index);
         {
             sort* dom[2] = { s, listS };
-            recfun::promise_def mem = p.ensure_def(symbol("member"), 2, dom, m.mk_bool_sort(), true);
+            recfun::promise_def mem = p.ensure_def(symbol(member), 2, dom, m.mk_bool_sort(), true);
             memf = mem.get_def()->get_decl();
             
             var_ref xV(m.mk_var(1, s), m);
@@ -913,7 +918,7 @@ namespace smt {
 
         {
             sort* dom[5] = { s, s, listS, listS, tup };
-            recfun::promise_def nxt = p.ensure_def(symbol("next"), 5, dom, tup, true);
+            recfun::promise_def nxt = p.ensure_def(symbol(next), 5, dom, tup, true);
             nextf = nxt.get_def()->get_decl();
             
             expr_ref next_body(m);
@@ -934,7 +939,7 @@ namespace smt {
 
         {
             sort* dom[3] = { listS, s, listS };
-            recfun::promise_def connected = p.ensure_def(symbol("connected"), 3, dom, m.mk_bool_sort(), true);
+            recfun::promise_def connected = p.ensure_def(symbol(connected_sym), 3, dom, m.mk_bool_sort(), true);
             connectedf = connected.get_def()->get_decl();
             var_ref AV(m.mk_var(2, listS), m);
             var_ref dstV(m.mk_var(1, s), m);