@@ -466,7 +466,9 @@ void value_sett::get_value_set_rec(
466
466
it1!=object_map.end ();
467
467
it1++)
468
468
{
469
- const exprt &object=object_numbering[it1->first ];
469
+ // / Do not take a reference to object_numbering's storage as we may call
470
+ // / object_numbering.number(), which may reallocate it.
471
+ const exprt object=object_numbering[it1->first ];
470
472
get_value_set_rec (object, dest, suffix, original_type, ns);
471
473
}
472
474
}
@@ -489,7 +491,9 @@ void value_sett::get_value_set_rec(
489
491
it!=object_map.end ();
490
492
it++)
491
493
{
492
- const exprt &object=object_numbering[it->first ];
494
+ // / Do not take a reference to object_numbering's storage as we may call
495
+ // / object_numbering.number(), which may reallocate it.
496
+ const exprt object=object_numbering[it->first ];
493
497
get_value_set_rec (object, dest, suffix, original_type, ns);
494
498
}
495
499
}
@@ -1348,7 +1352,9 @@ void value_sett::assign_rec(
1348
1352
it!=reference_set.read ().end ();
1349
1353
it++)
1350
1354
{
1351
- const exprt &object=object_numbering[it->first ];
1355
+ // / Do not take a reference to object_numbering's storage as we may call
1356
+ // / object_numbering.number(), which may reallocate it.
1357
+ const exprt object=object_numbering[it->first ];
1352
1358
1353
1359
if (object.id ()!=ID_unknown)
1354
1360
assign_rec (object, values_rhs, suffix, ns, add_to_sets);
0 commit comments