fix for multi-ary fixed-bv multiplication

Author: Daniel Kroening

regression/cbmc/Fixedbv8/main.c

@@ -0,0 +1,13 @@
+typedef __CPROVER_fixedbv[64][32] __plant_typet;
+extern __plant_typet A0, A1;
+
+int main(void) {
+  __CPROVER_assume(A0 == (__plant_typet)0.125);
+  __CPROVER_assume(A1 == (__plant_typet)0.015625);
+
+  const __plant_typet XXX1a=A0 * A1;
+  const __plant_typet XXX2a=(__plant_typet)-1 * XXX1a;
+  const __plant_typet XXX2b=-0.001953125;
+  __CPROVER_assert(XXX2a==XXX2b, "");
+  return 0;
+}

regression/cbmc/Fixedbv8/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/solvers/flattening/boolbv_mult.cpp

@@ -53,15 +53,15 @@ bvt boolbvt::convert_mult(const exprt &expr)
     std::size_t fraction_bits=
       to_fixedbv_type(expr.type()).get_fraction_bits();
 
-    // do a sign extension by fraction_bits bits
-    bv=bv_utils.sign_extension(bv, bv.size()+fraction_bits);
-
     for(exprt::operandst::const_iterator it=operands.begin()+1;
         it!=operands.end(); it++)
     {
       if(it->type()!=expr.type())
         throw "multiplication with mixed types";
 
+      // do a sign extension by fraction_bits bits
+      bv=bv_utils.sign_extension(bv, bv.size()+fraction_bits);
+
       bvt op=convert_bv(*it);
 
       if(op.size()!=width)
@@ -70,10 +70,10 @@ bvt boolbvt::convert_mult(const exprt &expr)
       op=bv_utils.sign_extension(op, bv.size());
 
       bv=bv_utils.signed_multiplier(bv, op);
-    }
 
-    // cut it down again
-    bv.erase(bv.begin(), bv.begin()+fraction_bits);
+      // cut it down again
+      bv.erase(bv.begin(), bv.begin()+fraction_bits);
+    }
 
     return bv;
   }