From f0b0aa2e0a42551f3ea2f907519eb82a0cb3c2f8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 17 Nov 2023 08:25:54 +0000 Subject: [PATCH] Add invariant that multiplication uses operands of the same size Our implementations swap operands, and determine the size of the result from the size of the operand(s). Make sure we produce consistent-width results. --- src/solvers/flattening/bv_utils.cpp | 5 +++++ 1 file changed, 5 insertions(+) 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);