@@ -1477,28 +1477,31 @@ TEST_CASE(
14771477 const symbol_exprt bar{" bar" , unsignedbv_typet{32 }};
14781478 SECTION (" Address of symbol" )
14791479 {
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" )
14841481 {
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+ }
15021505 }
15031506 }
15041507 SECTION (" Invariant checks" )
0 commit comments