Disable int/real coercions in the API

[pclayton]

In switching from Z3 version 4.8.12 to 4.13.0, I have found that some SMT constraints that were previously ill-sorted and failed have become valid and give unsat because 4.13.0 casts terms of sort Bool to Int or Real as required (and an inequality on a symbol of sort Bool was not satisfiable for 0 or 1). This specific issue can easily be resolved but has raised a more general issue about the int/real coercions. Where Z3 terms are generated by a tool via the API, the tool - at least in my case - already ensures that terms are well sorted. The coercions are unnecessary and can hide issues with the tool and, with the coercion of sort Bool now, it seems more likely that an issue could be undetected. Generally, it would be desirable to be able to choose failure to avoid giving an incorrect 'unsafe' result.

In SMT-LIB 2 input, we can disable the int/real coercions using

(set-option :smtlib2-compliant true)

or, more specifically, using

(set-option :int-real-coercions false)

These options do not appear to work when specified in the string given to Z3_solver_from_string. Also, for programmatic use, we cannot set smtlib2_compliant in the API via Z3_set_param_value nor Z3_update_param_value because it is a shell-only parameter and there is no API parameter int_real_coercions.

Would a PR adding an API parameter int_real_coercions (that disables coercions in the API) be useful?