@@ -502,7 +502,9 @@ void value_sett::get_value_set_rec(
502
502
it1!=object_map.end ();
503
503
it1++)
504
504
{
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 ];
506
508
get_value_set_rec (object, dest, suffix, original_type, ns);
507
509
}
508
510
}
@@ -525,7 +527,9 @@ void value_sett::get_value_set_rec(
525
527
it!=object_map.end ();
526
528
it++)
527
529
{
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 ];
529
533
get_value_set_rec (object, dest, suffix, original_type, ns);
530
534
}
531
535
}
@@ -1429,7 +1433,9 @@ void value_sett::assign_rec(
1429
1433
it!=reference_set.read ().end ();
1430
1434
it++)
1431
1435
{
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 ];
1433
1439
1434
1440
if (object.id ()!=ID_unknown)
1435
1441
assign_rec (object, values_rhs, suffix, ns, add_to_sets);
0 commit comments