CORE
Test.class
--function Test.main
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
--
--
This checks that jbmc knows that test.x and parent.x refer to the same field.
Both test and parent are concrete (available) classes.
