CBMC version: 5.25.0
Operating system: macOS Mojave
Exact command line resulting in the issue: N/A.
What behaviour did you expect: N/A.
What happened instead: N/A.
Refactor: remove all get_namespacefrom code_contracts.*. This could require refactoring input values across functions.