diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-27 11:07:19 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-27 16:07:19 +0000 |
commit | 9cf32b5d3f12a886779b85066d8c5997b49aefc1 (patch) | |
tree | a777c7d24726e3dfee4575864920466163323487 /test/unit/theory/sequences_rewriter_white.cpp | |
parent | 7bb6e7970de3719308110dd993cf4393031b8d80 (diff) |
Avoid non-terminating check with assumptions in strings rewriter (#7503)
These rewrites introduce the possibility of non-termination in the rewriter, as demonstrated in the included regression.
Instead, these rewrites are now moved to the extended rewriter.
Diffstat (limited to 'test/unit/theory/sequences_rewriter_white.cpp')
-rw-r--r-- | test/unit/theory/sequences_rewriter_white.cpp | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index 32122e619..bcac315a7 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -248,8 +248,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) a, d_nodeManager->mkNode(kind::PLUS, x, d_nodeManager->mkConst(Rational(1))), x); - res = sr.rewriteSubstr(n); - ASSERT_EQ(res, empty); + sameNormalForm(n, empty); // (str.substr "A" (+ x (str.len s2)) x) -> "" n = d_nodeManager->mkNode( @@ -258,8 +257,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) d_nodeManager->mkNode( kind::PLUS, x, d_nodeManager->mkNode(kind::STRING_LENGTH, s)), x); - res = sr.rewriteSubstr(n); - ASSERT_EQ(res, empty); + sameNormalForm(n, empty); // (str.substr "A" x y) -> (str.substr "A" x y) n = d_nodeManager->mkNode(kind::STRING_SUBSTR, a, x, y); @@ -271,14 +269,13 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) abcd, d_nodeManager->mkNode(kind::PLUS, x, three), x); - res = sr.rewriteSubstr(n); - ASSERT_EQ(res, empty); + sameNormalForm(n, empty); // (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x) n = d_nodeManager->mkNode( kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::PLUS, x, two), x); res = sr.rewriteSubstr(n); - ASSERT_EQ(res, n); + sameNormalForm(res, n); // (str.substr (str.substr s x x) x x) -> "" n = d_nodeManager->mkNode(kind::STRING_SUBSTR, |