Z3: disable ematching and rely solely on MBQI
gives a ~3x speedup
MODIFY
smt/ctx.cpp
smt/ctx.cpp
@@ -12,6 +12,7 @@ context ctx;
void context::init() {
auto config = Z3_mk_config();
Z3_set_param_value(config, "timeout", get_query_timeout());
+ Z3_global_param_set("smt.ematching", "false");
ctx = Z3_mk_context_rc(config);
Z3_del_config(config);
}

Z3: disable ematching and rely solely on MBQI
gives a ~3x speedup