diff --git a/src/util/bit_util.cpp b/src/util/bit_util.cpp
index 0f1fd294d..fde66b054 100644
--- a/src/util/bit_util.cpp
+++ b/src/util/bit_util.cpp
@@ -351,7 +351,7 @@ bool has_one_at_first_k_bits(unsigned sz, unsigned const * data, unsigned k) {
     }
     if (word_sz < sz) {
         unsigned bit_sz  = k % (8 * sizeof(unsigned));
-        unsigned mask    = (1 << bit_sz) - 1;
+        unsigned mask    = (1u << bit_sz) - 1;
         return (data[word_sz] & mask) != 0;
     }
     return false;
diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h
index 6738ba0aa..f7af2019d 100644
--- a/src/util/bit_vector.h
+++ b/src/util/bit_vector.h
@@ -75,8 +75,11 @@ public:
     bit_vector(bit_vector const & source):
         m_num_bits(source.m_num_bits),
         m_capacity(source.m_capacity),
-        m_data(alloc_svect(unsigned, source.m_capacity)) {
-        memcpy(m_data, source.m_data, source.m_capacity * sizeof(unsigned));
+        m_data(0) {
+        if (source.m_data) {
+            m_data = alloc_svect(unsigned, m_capacity);
+            memcpy(m_data, source.m_data, m_capacity * sizeof(unsigned));
+        }
     }
     
     bit_vector(unsigned const * source, int num_bits):
@@ -184,6 +187,9 @@ public:
 
     bit_vector & operator=(bit_vector const & source) {
         m_num_bits = source.m_num_bits;
+        if (!source.m_data)
+            return *this;
+
         if (m_capacity < source.m_capacity) {
             dealloc_svect(m_data);
             m_data     = alloc_svect(unsigned, source.m_capacity);
diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp
index b979b32ff..14c67e7c0 100644
--- a/src/util/mpff.cpp
+++ b/src/util/mpff.cpp
@@ -255,7 +255,7 @@ void mpff_manager::set(mpff & n, int64 v) {
     }
     else {
         if (v < 0) {
-            set(n, static_cast<uint64>(-v));
+            set(n, -static_cast<uint64>(v));
             n.m_sign = 1;
         }
         else {
@@ -680,7 +680,7 @@ void mpff_manager::add_sub(bool is_sub, mpff const & a, mpff const & b, mpff & c
     
     // Make sure that a and b have the same exponent.
     if (exp_a > exp_b) {
-        unsigned shift = exp_a - exp_b;
+        unsigned shift = (unsigned)exp_a - (unsigned)exp_b;
         n_sig_b = m_buffers[0].c_ptr();
         shr(m_precision, sig_b, shift, m_precision, n_sig_b);
         if (sgn_b != m_to_plus_inf && has_one_at_first_k_bits(m_precision, sig_b, shift)) {