(Note: by default, multiplication (‘*’), division (’/’) and modulo (‘%’) are abstracted by uninterpreted functions, since they may lead to very long run-times.

If the correctness of your equivalence depends on them, then please use the ‘keep arithmetic’ option. Replacing ‘int’ with ‘char’ typically also reduces run-time.)