@@ -1477,28 +1477,31 @@ TEST_CASE(
1477
1477
const symbol_exprt bar{" bar" , unsignedbv_typet{32 }};
1478
1478
SECTION (" Address of symbol" )
1479
1479
{
1480
- const address_of_exprt address_of_foo{foo};
1481
- track_expression_objects (address_of_foo, ns, test.object_map );
1482
- INFO (" Expression " + address_of_foo.pretty (1 , 0 ));
1483
- SECTION (" 8 object bits" )
1480
+ SECTION (" bit vector symbol" )
1484
1481
{
1485
- config.bv_encoding .object_bits = 8 ;
1486
- const auto converted = test.convert (address_of_foo);
1487
- CHECK (test.object_map .at (foo).unique_id == 2 );
1488
- CHECK (
1489
- converted == smt_bit_vector_theoryt::concat (
1490
- smt_bit_vector_constant_termt{2 , 8 },
1491
- smt_bit_vector_constant_termt{0 , 56 }));
1492
- }
1493
- SECTION (" 16 object bits" )
1494
- {
1495
- config.bv_encoding .object_bits = 16 ;
1496
- const auto converted = test.convert (address_of_foo);
1497
- CHECK (test.object_map .at (foo).unique_id == 2 );
1498
- CHECK (
1499
- converted == smt_bit_vector_theoryt::concat (
1500
- smt_bit_vector_constant_termt{2 , 16 },
1501
- smt_bit_vector_constant_termt{0 , 48 }));
1482
+ const address_of_exprt address_of_foo{foo};
1483
+ track_expression_objects (address_of_foo, ns, test.object_map );
1484
+ INFO (" Expression " + address_of_foo.pretty (1 , 0 ));
1485
+ SECTION (" 8 object bits" )
1486
+ {
1487
+ config.bv_encoding .object_bits = 8 ;
1488
+ const auto converted = test.convert (address_of_foo);
1489
+ CHECK (test.object_map .at (foo).unique_id == 2 );
1490
+ CHECK (
1491
+ converted == smt_bit_vector_theoryt::concat (
1492
+ smt_bit_vector_constant_termt{2 , 8 },
1493
+ smt_bit_vector_constant_termt{0 , 56 }));
1494
+ }
1495
+ SECTION (" 16 object bits" )
1496
+ {
1497
+ config.bv_encoding .object_bits = 16 ;
1498
+ const auto converted = test.convert (address_of_foo);
1499
+ CHECK (test.object_map .at (foo).unique_id == 2 );
1500
+ CHECK (
1501
+ converted == smt_bit_vector_theoryt::concat (
1502
+ smt_bit_vector_constant_termt{2 , 16 },
1503
+ smt_bit_vector_constant_termt{0 , 48 }));
1504
+ }
1502
1505
}
1503
1506
}
1504
1507
SECTION (" Invariant checks" )
0 commit comments