Merge pull request #837 from allredj/string-solver-bugfix-symbol-map

forejtv · web-flow · commit ac71afe93346 · 2017-06-06T15:52:31.000+01:00
Correcting addition of symbol to symbol map
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
@@ -187,7 +187,8 @@ void string_refinementt::add_symbol_to_symbol_map(
   symbol_resolve[lhs]=new_rhs;
   reverse_symbol_resolve[new_rhs].push_back(lhs);
 
-  std::list<exprt> symbols_to_update_with_new_rhs(reverse_symbol_resolve[rhs]);
+  const std::list<exprt> &symbols_to_update_with_new_rhs(
+    reverse_symbol_resolve[lhs]);
   for(exprt item : symbols_to_update_with_new_rhs)
   {
     symbol_resolve[item]=new_rhs;

Original file line number	Diff line number	Diff line change
`@@ -187,7 +187,8 @@ void string_refinementt::add_symbol_to_symbol_map(`
`187`	`187`	`symbol_resolve[lhs]=new_rhs;`
`188`	`188`	`reverse_symbol_resolve[new_rhs].push_back(lhs);`
`189`	`189`
`190`		`- std::list<exprt> symbols_to_update_with_new_rhs(reverse_symbol_resolve[rhs]);`
	`190`	`+ const std::list<exprt> &symbols_to_update_with_new_rhs(`
	`191`	`+ reverse_symbol_resolve[lhs]);`
`191`	`192`	`for(exprt item : symbols_to_update_with_new_rhs)`
`192`	`193`	`{`
`193`	`194`	`symbol_resolve[item]=new_rhs;`