Fix sum update in sum_over_map

romainbrenguier · romainbrenguier · commit fae7c714c54e · 2019-04-29T08:02:40.000+01:00
The instruction was without an effect and should have updated sum instead.
diff --git a/src/solvers/strings/string_constraint_instantiation.cpp b/src/solvers/strings/string_constraint_instantiation.cpp
@@ -131,8 +131,9 @@ exprt sum_over_map(std::map<exprt, int> &m, const typet &type, bool negated)
           if(sum.is_nil())
             sum = t;
           else
-            plus_exprt(sum, t);
-          for(int i = 1; i < factor; i++)             sum = plus_exprt(sum, t);
+            sum = plus_exprt(sum, t);
+          for(int i = 1; i < factor; i++)
+            sum = plus_exprt(sum, t);
         }
         else if(factor < -1)
         {

Original file line number	Diff line number	Diff line change
`@@ -131,8 +131,9 @@ exprt sum_over_map(std::map<exprt, int> &m, const typet &type, bool negated)`
`131`	`131`	`if(sum.is_nil())`
`132`	`132`	`sum = t;`
`133`	`133`	`else`
`134`		`- plus_exprt(sum, t);`
`135`		`- for(int i = 1; i < factor; i++) sum = plus_exprt(sum, t);`
	`134`	`+ sum = plus_exprt(sum, t);`
	`135`	`+ for(int i = 1; i < factor; i++)`
	`136`	`+ sum = plus_exprt(sum, t);`
`136`	`137`	`}`
`137`	`138`	`else if(factor < -1)`
`138`	`139`	`{`