diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
index 7475750db..69cc4819a 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/muz/rel/tbv.cpp
@@ -74,8 +74,7 @@ tbv* tbv_manager::allocate(tbv const& bv) {
 }
 tbv* tbv_manager::allocate(uint64 val) {
     tbv* v = allocate0();
-    for (unsigned bit = num_tbits(); bit > 0;) {
-        --bit;
+    for (unsigned bit = std::min(64u, num_tbits()); bit-- > 0;) {
         if (val & (1ULL << bit)) {                        
             set(*v, bit, BIT_1);
         } else {