diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp
index 96cd9cf2b57..31dd12fea20 100644
--- 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);