Consider all non-obvious choose's to be impure

Created by: jad-hamza

Temporary fix for https://github.com/epfl-lara/stainless/issues/483

I couldn't use Ensure in the InoxEncoder because it's not an Inox tree, is that fix ok?