diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index 42ac2cdd9..8139f1c2e 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -221,6 +221,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node a = d_nm->mkConst(::CVC4::String("A")); Node b = d_nm->mkConst(::CVC4::String("B")); Node abcd = d_nm->mkConst(::CVC4::String("ABCD")); + Node negone = d_nm->mkConst(Rational(-1)); Node zero = d_nm->mkConst(Rational(0)); Node one = d_nm->mkConst(Rational(1)); Node two = d_nm->mkConst(Rational(2)); @@ -330,6 +331,14 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node substr_itos = d_nm->mkNode( kind::STRING_SUBSTR, d_nm->mkNode(kind::STRING_ITOS, x), x, x); sameNormalForm(substr_itos, empty); + + // (str.substr s (* (- 1) (str.len s)) 1) ---> empty + Node substr = d_nm->mkNode( + kind::STRING_SUBSTR, + s, + d_nm->mkNode(kind::MULT, negone, d_nm->mkNode(kind::STRING_LENGTH, s)), + one); + sameNormalForm(substr, empty); } void testRewriteConcat() |