diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 43d3820f3..6144447e3 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -314,6 +314,7 @@ namespace smt {
             }
         }
 
+
         void found_not_handled(expr* n) {
             m_not_handled = n;
             if (is_app(n) && is_underspecified(to_app(n))) {
@@ -419,9 +420,6 @@ namespace smt {
                     if (is_app(n)) {
                         internalize_args(to_app(n));
                     }
-                    if (a.is_int(n)) {
-                        found_not_handled(n);
-                    }
                     theory_var v = mk_var(n);
                     coeffs[vars.size()] = coeffs[index];
                     vars.push_back(v);
@@ -1189,6 +1187,7 @@ namespace smt {
                 case l_false:
                     return FC_CONTINUE;
                 case l_undef:
+                    TRACE("arith", tout << "check-lia giveup\n";);
                     st = FC_GIVEUP;
                     break;
                 }
@@ -1199,23 +1198,27 @@ namespace smt {
                 case l_false:
                     return FC_CONTINUE;
                 case l_undef:
+                    TRACE("arith", tout << "check-nra giveup\n";);
                     st = FC_GIVEUP;
                     break;
                 }
-                if (m_not_handled != 0) {                    
+                if (m_not_handled != 0) {            
+                    TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";);        
                     st = FC_GIVEUP;
                 }
-
+                
                 return st;
             case l_false:
                 set_conflict();
                 return FC_CONTINUE;
             case l_undef:
+                TRACE("arith", tout << "check feasiable is undef\n";);
                 return m.canceled() ? FC_CONTINUE : FC_GIVEUP;
             default:
                 UNREACHABLE();
                 break;
             }
+            TRACE("arith", tout << "default giveup\n";);
             return FC_GIVEUP;
         }
 
@@ -1268,10 +1271,12 @@ namespace smt {
                 set_conflict1();
                 return l_false;
             case lean::lia_move::give_up:
+                TRACE("arith", tout << "lia giveup\n";);
                 return l_undef;
             default:
                 UNREACHABLE();
             }
+            UNREACHABLE();
             return l_undef;
         }
 
@@ -1294,6 +1299,8 @@ namespace smt {
                     return l_false;
                 }
                 break;
+            case l_undef:
+                TRACE("arith", tout << "nra-undef\n";);
             default:
                 break;
             }