disable symbolic ptr types until partial models work for type infernece
MODIFY
ir/type.cpp
ir/type.cpp
@@ -552,7 +552,8 @@ expr SymbolicType::operator==(const Type &b) const {
expr c(false);
c |= isInt() && i == rhs->i;
c |= isFloat() && f == rhs->f;
- c |= isPtr() && p == rhs->p;
+ // TODO: to reenable this, we need partial models and/or a shrinker
+ //c |= isPtr() && p == rhs->p;
c |= isArray() && a == rhs->a;
c |= isVector() && v == rhs->v;
// FIXME: add support for this: c |= isStruct() && s == rhs->s;

MODIFY
smt/ctx.cpp
smt/ctx.cpp
@@ -10,6 +10,7 @@ namespace smt {
context ctx;
void context::init() {
+ Z3_global_param_set("model.partial", "true");
Z3_global_param_set("smt.ematching", "false");
Z3_global_param_set("smt.mbqi.max_iterations", "1000000");
Z3_global_param_set("timeout", get_query_timeout());

disable symbolic ptr types until partial models work for type infernece