3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-19 15:19:01 +00:00

patch out contains check for substr reduction

fixes all regressions in release build, we may want to revisit this later
This commit is contained in:
Murphy Berzish 2016-09-22 20:14:42 -04:00
parent 1061cdf58a
commit dc8062ba67

View file

@ -1496,7 +1496,8 @@ void theory_str::instantiate_axiom_Substr(enode * e) {
expr_ref ts0_contains_ts1(mk_contains(expr->get_arg(0), ts1), m);
expr_ref_vector and_item(m);
and_item.push_back(ts0_contains_ts1);
// TODO simulate this contains check; it causes problems with a few regressions but we might need it for performance
//and_item.push_back(ts0_contains_ts1);
and_item.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(ts0, mk_concat(ts1, ts2))));
and_item.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_strlen(ts0)));
and_item.push_back(ctx.mk_eq_atom(expr->get_arg(2), mk_strlen(ts1)));