diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp
index d5fc9af0c..590cfb438 100644
--- a/src/ast/ast_ll_pp.cpp
+++ b/src/ast/ast_ll_pp.cpp
@@ -42,11 +42,7 @@ class ll_printer {
     }
 
     void display_name(func_decl * decl) {
-        symbol n = decl->get_name();
-        if (decl->is_skolem() && n.is_numerical())
-            m_out << "z3.sk." << n.get_num();
-        else 
-            m_out << n;
+        m_out << decl->get_name();
     }
 
     bool process_numeral(expr * n) {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index a9d572e22..2555fc2d8 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -695,8 +695,10 @@ class theory_lra::imp {
         if (!_has_var) {
             svector<lpvar> vars;
             for (expr* n : *t) {
+                if (is_app(n)) VERIFY(internalize_term(to_app(n)));
                 SASSERT(ctx().e_internalized(n));
-                vars.push_back(register_theory_var_in_lar_solver(mk_var(n)));        
+                theory_var v = mk_var(n);
+                vars.push_back(register_theory_var_in_lar_solver(v));
             }
             TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n" << vars << "\n";);
             m_solver->register_existing_terms();            
@@ -769,8 +771,8 @@ class theory_lra::imp {
         enode* e = get_enode(n);
         theory_var v;
         if (!th.is_attached_to_var(e)) {
-            TRACE("arith", tout << "fresh var: " << mk_pp(n, m) << "\n";);
             v = th.mk_var(e);
+            TRACE("arith", tout << "fresh var: v" << v << " " << mk_pp(n, m) << "\n";);
             SASSERT(m_bounds.size() <= static_cast<unsigned>(v) || m_bounds[v].empty());
             if (m_bounds.size() <= static_cast<unsigned>(v)) {
                 m_bounds.push_back(lp_bounds());
@@ -875,13 +877,15 @@ class theory_lra::imp {
         theory_var z = internalize_linearized_def(term, st);      
         lpvar vi = register_theory_var_in_lar_solver(z);
         add_def_constraint(lp().add_var_bound(vi, lp::LE, rational::zero()));
-        // if (is_infeasible()) {
+        if (is_infeasible()) {
+            IF_VERBOSE(0, verbose_stream() << "infeasible\n";);
         //     process_conflict(); // exit here?
-        // }
+        }
         add_def_constraint(lp().add_var_bound(vi, lp::GE, rational::zero()));
-        // if (is_infeasible()) {
-        //     process_conflict();
-        // }
+        if (is_infeasible()) {
+            IF_VERBOSE(0, verbose_stream() << "infeasible\n";);
+        //     process_conflict(); // exit here?
+        }
         TRACE("arith", 
               {
                   expr*  o1 = get_enode(v1)->get_owner();
@@ -969,7 +973,7 @@ class theory_lra::imp {
             }
             theory_var v = mk_var(term);
             lpvar vi = get_lpvar(v);
-            TRACE("arith", tout << mk_bounded_pp(term, m) << " v" << v << " vi " << vi << "\n";);
+            TRACE("arith", tout << mk_bounded_pp(term, m) << " v" << v << " j" << vi << "\n";);
             if (vi == UINT_MAX) {
                 rational const& offset = st.offset();
                 if (!offset.is_zero()) {
@@ -981,6 +985,9 @@ class theory_lra::imp {
                 TRACE("arith_verbose", tout << "v" << v << " := " << mk_pp(term, m) << " slack: " << vi << " scopes: " << m_scopes.size() << "\n";
                       lp().print_term(lp().get_term(vi), tout) << "\n";);
             }
+            else {                
+                SASSERT(lp::tv::is_term(vi));
+            }
             rational val;
             if (a.is_numeral(term, val)) {
                 m_fixed_var_table.insert(value_sort_pair(val, is_int(v)), v);