@@ -502,7 +502,9 @@ void value_sett::get_value_set_rec(
502502 it1!=object_map.end ();
503503 it1++)
504504 {
505- const exprt &object=object_numbering[it1->first ];
505+ // / Do not take a reference to object_numbering's storage as we may call
506+ // / object_numbering.number(), which may reallocate it.
507+ const exprt object=object_numbering[it1->first ];
506508 get_value_set_rec (object, dest, suffix, original_type, ns);
507509 }
508510 }
@@ -525,7 +527,9 @@ void value_sett::get_value_set_rec(
525527 it!=object_map.end ();
526528 it++)
527529 {
528- const exprt &object=object_numbering[it->first ];
530+ // / Do not take a reference to object_numbering's storage as we may call
531+ // / object_numbering.number(), which may reallocate it.
532+ const exprt object=object_numbering[it->first ];
529533 get_value_set_rec (object, dest, suffix, original_type, ns);
530534 }
531535 }
@@ -1429,7 +1433,9 @@ void value_sett::assign_rec(
14291433 it!=reference_set.read ().end ();
14301434 it++)
14311435 {
1432- const exprt &object=object_numbering[it->first ];
1436+ // / Do not take a reference to object_numbering's storage as we may call
1437+ // / object_numbering.number(), which may reallocate it.
1438+ const exprt object=object_numbering[it->first ];
14331439
14341440 if (object.id ()!=ID_unknown)
14351441 assign_rec (object, values_rhs, suffix, ns, add_to_sets);
0 commit comments