diff --git a/src/test/bit_vector.cpp b/src/test/bit_vector.cpp
index 2b67c3a71..7d3f96ae4 100644
--- a/src/test/bit_vector.cpp
+++ b/src/test/bit_vector.cpp
@@ -276,12 +276,35 @@ static void tst_bv_reset() {
     }
 }
 
+static void tst_eq() {
+    bit_vector b1, b2, b3;
+    b1.resize(32);
+    b2.resize(32);
+    b3.resize(32);
+
+    b1.set(3, true);
+    SASSERT(b1 != b2);
+    SASSERT(!(b1 == b2));
+    SASSERT(b2 == b3);
+
+    b3.set(3, true);
+    SASSERT(b1 == b3);
+    SASSERT(!(b1 != b3));
+    
+    b2.set(31, true);
+    b3.set(31);
+    b3.unset(3);
+    SASSERT(b2 == b3);
+    SASSERT(!(b2 != b3));
+}
+
 void tst_bit_vector() {
     tst_crash();
     tst_shift(); 
     tst_or();
     tst_and();
     tst_bv_reset();
+    tst_eq();
     return;
     tst2();
     for (unsigned i = 0; i < 20; i++) {
diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp
index 210d230bc..2328a5849 100644
--- a/src/util/bit_vector.cpp
+++ b/src/util/bit_vector.cpp
@@ -116,7 +116,7 @@ void bit_vector::shift_right(unsigned k) {
     }
 }
 
-bool bit_vector::operator==(bit_vector const & source) {
+bool bit_vector::operator==(bit_vector const & source) const {
     if (m_num_bits != source.m_num_bits)
         return false;
     unsigned n = num_words();
@@ -129,6 +129,7 @@ bool bit_vector::operator==(bit_vector const & source) {
     }
     unsigned bit_rest = source.m_num_bits % 32;
     unsigned mask = (1 << bit_rest) - 1;
+    if (mask == 0) mask = UINT_MAX;
     return (m_data[i] & mask) == (source.m_data[i] & mask);
 }
 
diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h
index 9560af7e2..2e7becee7 100644
--- a/src/util/bit_vector.h
+++ b/src/util/bit_vector.h
@@ -171,9 +171,9 @@ public:
             resize(sz, val);
     }
 
-    bool operator==(bit_vector const & other);
+    bool operator==(bit_vector const & other) const;
 
-    bool operator!=(bit_vector const & other) { return !operator==(other); }
+    bool operator!=(bit_vector const & other) const { return !operator==(other); }
 
     bit_vector & operator=(bit_vector const & source) {
         m_num_bits = source.m_num_bits;