diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-29 10:07:08 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-29 10:09:58 -0800 |
commit | 030cdf1e7f61034dda5b9ed8fd4925d87c6a1c3d (patch) | |
tree | f74ee561e2e0bcb4aa7edf3286a49f64b13e1f4d /test/unit | |
parent | 467ef8692009f440bda74083d476131ff1e88b51 (diff) |
Fix corner case in stripConstantEndpoints
`stripConstantEndpoints()` was returning `true` when the first argument
was a list only containing an empty string, which could lead to rewrite
loops. This commit checks for that case and adds a unit test for it.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index 59d36d9e8..4ad0b4ad2 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -1166,6 +1166,23 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite } } + void testStripConstantEndpoints() + { + Node empty = d_nm->mkConst(::CVC4::String("")); + Node a = d_nm->mkConst(::CVC4::String("A")); + + { + // stripConstantEndpoints({ "" }, { "a" }, {}, {}, 0) ---> false + std::vector<Node> n1 = {empty}; + std::vector<Node> n2 = {a}; + std::vector<Node> nb; + std::vector<Node> ne; + bool res = + TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0); + TS_ASSERT(!res); + } + } + private: ExprManager* d_em; SmtEngine* d_smt; |