Z3_set_param_value seems to ignore global parameters, for which Z3_global_param_set should be set. Unfortunately, this is not obvious to users when they interact with Z3 through another layer (like smtlib-backends).

Would it be possible to query the API to learn if some parameter set with Z3_set_param_value has been ignored? This would allow to give users an explicit error message when things don't go as expected.

This issue surfaced when a user was trying to start a Z3 context with dump_models set to true.

Another solution could be having a way to test whether a parameter is in the domain of Z3_set_param_value ahead of making the call. There is a call Z3_get_global_param_descrs, but it requires having a Z3 context first, which isn't necessary with Z3_set_param_value.