diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index 4d7da4d7f..67c1b757f 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -538,6 +538,8 @@ namespace seq {
         expr_ref t_eq_empty = mk_eq_empty(t);
         expr_ref xsy        = mk_concat(x, s, y);
 
+        verbose_stream() << s << " " << t << "\n";
+        //        add_clause(~mk_eq(t, s), i_eq_0);
         add_clause(cnt, i_eq_m1);
         add_clause(~t_eq_empty, s_eq_empty, i_eq_m1);
         add_clause(~s_eq_empty, mk_eq(i, mk_len(t)));
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index 0c83ea5bf..dbb5dbae2 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -31,7 +31,7 @@ namespace lp {
         lra.remove_fixed_vars_from_base();
         lp_assert(lia.is_feasible());
         for (unsigned j : lra.r_basis()) 
-            if (!lra.get_value(j).is_int())
+            if (!lra.get_value(j).is_int() && lra.column_is_int(j))
                 patch_basic_column(j);
         if (!lia.has_inf_int()) {
             lia.settings().stats().m_patches_success++;