diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index cf4bcd87c..ce1cc2103 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -8480,7 +8480,13 @@ def fpToReal(x):
     return ArithRef(Z3_mk_fpa_to_real(x.ctx_ref(), x.ast), x.ctx)
 
 def fpToIEEEBV(x):
-    """Create a Z3 floating-point conversion expression, from floating-point expression to IEEE bit-vector.
+    """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
+    
+    The size of the resulting bit-vector is automatically determined. 
+    
+    Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion 
+    knows only one NaN and it will always produce the same bit-vector represenatation of 
+    that NaN.
 
     >>> x = FP('x', FPSort(8, 24))
     >>> y = fpToIEEEBV(x)
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index b579d698e..a30c0d32c 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -902,6 +902,7 @@ template<typename Cfg>
 void bit_blaster_tpl<Cfg>::mk_shl(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
     numeral k;
     if (is_numeral(sz, b_bits, k)) {
+        if (k > numeral(sz)) k = numeral(sz);
         unsigned n = static_cast<unsigned>(k.get_int64());
         if (n >= sz) n = sz;
         unsigned pos; 
@@ -947,6 +948,7 @@ template<typename Cfg>
 void bit_blaster_tpl<Cfg>::mk_lshr(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
     numeral k;
     if (is_numeral(sz, b_bits, k)) {
+        if (k > numeral(sz)) k = numeral(sz);
         unsigned n   = static_cast<unsigned>(k.get_int64()); 
         unsigned pos = 0;
         for (unsigned i = n; i < sz; pos++, i++)
@@ -989,6 +991,7 @@ template<typename Cfg>
 void bit_blaster_tpl<Cfg>::mk_ashr(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
     numeral k;
     if (is_numeral(sz, b_bits, k)) {
+        if (k > numeral(sz)) k = numeral(sz);
         unsigned n   = static_cast<unsigned>(k.get_int64()); 
         unsigned pos = 0;
         for (unsigned i = n; i < sz; pos++, i++)
diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
index 693066ee1..6d9f98f39 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -282,7 +282,7 @@ class fix_dl_var_tactic : public tactic {
                 expr_ref   new_curr(m);
                 proof_ref  new_pr(m);
                 unsigned size = g->size();
-                for (unsigned idx = 0; idx < size; idx++) {
+                for (unsigned idx = 0; !g->inconsistent() && idx < size; idx++) {
                     expr * curr = g->form(idx);
                     m_rw(curr, new_curr, new_pr);
                     if (produce_proofs) {