fixup! Symbolic Toom-Cook multiplication

Author: tautschnig

src/solvers/flattening/bv_utils.cpp

@@ -2035,14 +2035,13 @@ bvt bv_utilst::unsigned_karatsuba_multiplier(const bvt &_op0, const bvt &_op1)
 
 bvt bv_utilst::unsigned_toom_cook_multiplier(const bvt &_op0, const bvt &_op1)
 {
+  PRECONDITION(_op0.size() == _op1.size());
   PRECONDITION(!_op0.empty());
-  PRECONDITION(!_op1.empty());
 
-  if(_op1.size() == 1)
-    return unsigned_multiplier(_op0, _op1);
+  if(_op0.size() == 1)
+    return {prop.land(_op0[0], _op1[0])};
 
   // break up _op0, _op1 in groups of at most GROUP_SIZE bits
-  PRECONDITION(_op0.size() == _op1.size());
 #define GROUP_SIZE 8
   const std::size_t d_bits =
     2 * GROUP_SIZE +