Z3: bump max number of mbqi iterations
MODIFY
smt/ctx.cpp
smt/ctx.cpp
@@ -11,6 +11,7 @@ context ctx;
void context::init() {
Z3_global_param_set("smt.ematching", "false");
+ Z3_global_param_set("smt.mbqi.max_iterations", "1000000");
Z3_global_param_set("timeout", get_query_timeout());
ctx = Z3_mk_context_rc(nullptr);
}

Z3: bump max number of mbqi iterations