======================================
F_HS_CLIENT (invariant admissibility)
Successfully verified.
======================================
ANY.default_create (creator, inherited by F_HS_CLIENT)
Successfully verified.
======================================
F_HS_CLIENT.test
Successfully verified.
======================================
F_HS_CLIENT.test_modification
Successfully verified.
======================================
F_HS_CLIENT.test_modification_fail
Verification failed.

Line: 131. Invariant valid_buckets might not hold on call to {ANY}.wrap.
======================================
F_HS_HASHABLE (invariant admissibility)
Successfully verified.
======================================
F_HS_KEY (invariant admissibility)
Successfully verified.
======================================
F_HS_KEY.hash_code
Successfully verified.
======================================
F_HS_KEY.set_value (creator)
Successfully verified.
======================================
F_HS_KEY.set_value
Successfully verified.
======================================
F_HS_KEY.hash_code_
Successfully verified.
======================================
F_HS_KEY.is_model_equal
Successfully verified.
======================================
F_HS_KEY.lemma_transitive
Successfully verified.
======================================
F_HS_LOCK (invariant admissibility)
Successfully verified.
======================================
ANY.default_create (creator, inherited by F_HS_LOCK)
Successfully verified.
======================================
F_HS_LOCK.add_set
Successfully verified.
======================================
F_HS_LOCK.lock
Successfully verified.
======================================
F_HS_LOCK.unlock
Successfully verified.
======================================
F_HS_SET (invariant admissibility)
Successfully verified.
======================================
F_HS_SET.make (creator)
Successfully verified.
======================================
F_HS_SET.has
Successfully verified.
======================================
F_HS_SET.extend
Successfully verified.
======================================
F_HS_SET.join
Successfully verified.
======================================
F_HS_SET.remove
Successfully verified.
======================================
F_HS_SET.wipe_out
Successfully verified.
======================================
F_HS_SET.bucket_index
Successfully verified.
======================================
F_HS_SET.index_of
Successfully verified.
======================================
F_HS_SET.set_has
Successfully verified.
======================================
F_HS_SET.no_duplicates
Successfully verified.