From dc8062ba6727e59dc789ba1a4e27c2fe48eecbb5 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 22 Sep 2016 20:14:42 -0400 Subject: [PATCH] patch out contains check for substr reduction fixes all regressions in release build, we may want to revisit this later --- src/smt/theory_str.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index ab6a9f229..23b2af0fb 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -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)));