string refiner: sum_over_map is now independent of bitvector representation

kroening · kroening · commit e5850b8cb7df · 2018-10-19T09:46:58.000+01:00
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
@@ -1449,8 +1449,8 @@ static exprt sum_over_map(
     int second=negated?(-term.second):term.second;
     if(t.id()==ID_constant)
     {
-      std::string value(to_constant_expr(t).get_value().c_str());
-      constants+=binary2integer(value, true)*second;
+      const auto int_value = numeric_cast_v<mp_integer>(to_constant_expr(t));
+      constants += int_value * second;
     }
     else
     {

Original file line number	Diff line number	Diff line change
`@@ -1449,8 +1449,8 @@ static exprt sum_over_map(`
`1449`	`1449`	`int second=negated?(-term.second):term.second;`
`1450`	`1450`	`if(t.id()==ID_constant)`
`1451`	`1451`	`{`
`1452`		`- std::string value(to_constant_expr(t).get_value().c_str());`
`1453`		`- constants+=binary2integer(value, true)*second;`
	`1452`	`+ const auto int_value = numeric_cast_v<mp_integer>(to_constant_expr(t));`
	`1453`	`+ constants += int_value * second;`
`1454`	`1454`	`}`
`1455`	`1455`	`else`
`1456`	`1456`	`{`