diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp
index 387b2e5a7..709ae5da3 100644
--- a/src/sat/smt/polysat_internalize.cpp
+++ b/src/sat/smt/polysat_internalize.cpp
@@ -289,9 +289,7 @@ namespace polysat {
         unsigned sz = bv.get_bv_size(e);
         unsigned arg_sz = bv.get_bv_size(arg);
         unsigned sz2 = sz - arg_sz;
-
         var2pdd(expr2enode(e)->get_th_var(get_id()));
-
         if (arg_sz == sz) 
             add_clause(eq_internalize(e, arg), false);            
         else {
@@ -299,7 +297,7 @@ namespace polysat {
             // arg < 0 ==> e = concat(arg, 1...1)
             // arg >= 0 ==> e = concat(arg, 0...0)
             add_clause(lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(rational::power_of_two(sz2) - 1, sz2))), false);
-            add_clause(~lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz - arg_sz))), false);
+            add_clause(~lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), false);
         }
     }
 
@@ -313,7 +311,7 @@ namespace polysat {
             add_clause(eq_internalize(e, arg), false);
         else 
             // e = concat(arg, 0...0)
-            add_clause(eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz - arg_sz))), false);        
+            add_clause(eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), false);        
     }
 
     void solver::internalize_div_rem(app* e, bool is_div) {