Disable all custom extensions in strict mode

[bclement-ocp]

See #1133:

Currently, the --strict option only disables optimization. It should also disable extensions such as ae.round and bv2nat / int2bv.

[Halbaroth]

Do you know how to fix this issue. I quickly took a look to our codebase and Dolmen and we have no mechanism to disable Typer extension like bv2nat. We could disable bv2nat and ae.round only with the CLI flag --strict before the initialization of the typer.

If there is a way to create a local environment for the typer, we could add bv2nat in this environment when we process (set-option :strict-mode true) and remove it when we process (set-option :strict-mode false).
What's your opinion @Gbury ?

[bclement-ocp]

I think we can disable typer extensions, it should just be a matter of resetting the appropriate key on the state (it might not be exposed but we can expose it). Did not think about it more than that because this is likely one of the lowest priority issues we have.

[Halbaroth]

Sure, I think about it because I am writing documentation.