bv2int: implementing the iand-sum mode (#5265)

[cvc5.git] / src / theory / arith / nl / iand_table.cpp

diff --git a/src/theory/arith/nl/iand_table.cpp b/src/theory/arith/nl/iand_table.cpp
index 12e06ed58e4ae4d8cf0da09b7e902c7f8a106d0f..050e6baed305c5135d696b645eb2b11ba68de639 100644 (file)
--- a/src/theory/arith/nl/iand_table.cpp
+++ b/src/theory/arith/nl/iand_table.cpp
@@ -198,7 +198,7 @@ void IAndTable::addDefaultValue(
   }
 
   // compute the most common result
-  uint64_t most_common_result;
+  uint64_t most_common_result = 0;
   uint64_t max_num_of_occ = 0;
   for (uint64_t i = 0; i <= num_of_values; i++)
   {
@@ -208,6 +208,9 @@ void IAndTable::addDefaultValue(
       most_common_result = i;
     }
   }
+  // sanity check: some value appears at least once.
+  Assert(max_num_of_occ != 0);
+
   // -1 is the default case of the table.
   // add it to the table
   table[std::make_pair(-1, -1)] = most_common_result;