======================================
EB2_KEY (invariant admissibility)
Successfully verified.
======================================
EB2_KEY.hash_code
Successfully verified.
======================================
EB2_KEY.set_value (creator)
Successfully verified.
======================================
EB2_KEY.set_value
Successfully verified.
======================================
EB2_KEY.hash_code_
Successfully verified.
======================================
EB2_KEY.is_model_equal
Successfully verified.
======================================
EB2_KEY.lemma_transitive
Successfully verified.
======================================
EB2_TESTER (invariant admissibility)
Successfully verified.
======================================
ANY.default_create (creator, inherited by EB2_TESTER)
Successfully verified.
======================================
EB2_TESTER.test_hash_table
Successfully verified.