Change erase() method of the sharing map to require that key exists

[danpoe]

Previously when sharing_map.erase(key) was called, two traversals of the path to the leaf to erase were done. One to check whether the key was in the map, and if it was, a second one to copy and detach the nodes on the path to the leaf. This commit changes erase() to require that the given key exists in the map. This simplifies the implementation and avoids two traversals of the path to the leaf when it is known that the key exists. If it is not known whether the key exists, sharing_map.has_key(key) should be explicitely called first.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[danpoe]

@tautschnig This will require wrapping the calls propagation.erase(key) in #4464 by if(propagation.has_key(key)) if it is not known whether the key exists.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: b2a548c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107095440

[tautschnig]

This will require wrapping the calls propagation.erase(key) in #4464 by if(propagation.has_key(key)) if it is not known whether the key exists.

Thanks a lot for the heads-up, now done (also in the field-sensitivity PR).