Merge pull request #8241 from tautschnig/cleanup/multiplier-invariant

Add invariant that multiplication uses operands of the same size
diffblue · Apr 20, 2024 · e8ebba3 · e8ebba3
2 parents 1ca18f2 + f0b0aa2
commit e8ebba3
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp
@@ -1071,6 +1071,11 @@ bvt bv_utilst::multiplier(
   const bvt &op1,
   representationt rep)
 {
+  // We determine the result size from the operand size, and the implementation
+  // liberally swaps the operands, so we need to arrive at the same size
+  // whatever the order of the operands.
+  PRECONDITION(op0.size() == op1.size());
+
   switch(rep)
   {
   case representationt::SIGNED: return signed_multiplier(op0, op1);