Use multiplication in sum_over_map for factor > 1

When the factor is not -1, 0 or 1 using multiplication makes the
resulting expression simpler.

Author: romainbrenguier

src/solvers/strings/string_constraint_instantiation.cpp

@@ -126,24 +126,13 @@ exprt sum_over_map(std::map<exprt, int> &m, const typet &type, bool negated)
         break;
 
       default:
-        if(factor > 1)
-        {
-          if(sum.is_nil())
-            sum = t;
-          else
-            sum = plus_exprt(sum, t);
-          for(int i = 1; i < factor; i++)
-            sum = plus_exprt(sum, t);
-        }
-        else if(factor < -1)
-        {
-          if(sum.is_nil())
-            sum = unary_minus_exprt(t);
-          else
-            sum = minus_exprt(sum, t);
-          for(int i = -1; i > factor; i--)
-            sum = minus_exprt(sum, t);
-        }
+      {
+        const mult_exprt to_add{t, from_integer(factor, t.type())};
+        if(sum.is_nil())
+          sum = to_add;
+        else
+          sum = plus_exprt(sum, to_add);
+      }
       }
     }
   }