É possível alterar o valor de tempo limite do solver em tempo de execução usando a API C? Para definir o tempo limite, o seguinte pode ser feito -

Z3_config  cfg = Z3_mk_config();
Z3_set_param_value(cfg, "SOFT_TIMEOUT", "10000") // set timeout to 10 seconds
Z3_context ctx = Z3_mk_context(cfg);
....
Z3_check_and_get_model(ctx);
....
....
Z3_check_and_get_model(ctx);

No entanto, suponha que queremos alterar o tempo limite da próxima consulta enquanto retemos o contexto. É possível alterar o valor de tempo limite entre os dois?