diff options
Diffstat (limited to 'test/regress/regress0/strings/unicode-esc.smt2')
| -rw-r--r-- | test/regress/regress0/strings/unicode-esc.smt2 | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/unicode-esc.smt2 b/test/regress/regress0/strings/unicode-esc.smt2 new file mode 100644 index 000000000..01f5f30ab --- /dev/null +++ b/test/regress/regress0/strings/unicode-esc.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --strings-exp --lang=smt2.6.1 +; EXPECT: sat +(set-logic ALL) + +(assert (= "\u{14}" "\u0014")) +(assert (= "\u{00}" "\u{0}")) +(assert (= "\u0000" "\u{0}")) +(assert (= (str.len "\u1234") 1)) +(assert (= (str.len "\u{1}") 1)) +(assert (= (str.len "\u{99}") 1)) +(assert (= (str.len "\u{779}") 1)) +(assert (= (str.len "\u{0779}") 1)) +(assert (= (str.len "\u{01779}") 1)) +(assert (= (str.len "\u{001779}") 10)) +(assert (= (str.len "\u{0vv79}") 9)) +(assert (= (str.len "\u{11\u1234}") 7)) +(assert (= (str.len "\u12345") 2)) +(assert (= (str.len "\uu") 3)) +(assert (= (str.len "\u{123}\u{567}") 2)) +(assert (= (str.len "\u{0017") 7)) +(assert (= (str.len "\\u00178") 3)) +(assert (= (str.len "2\u{}") 5)) +(assert (= (str.len "\uaaaa") 1)) +(assert (= (str.len "\uAAAA") 1)) +(assert (= (str.len "\u{0AbC}") 1)) +(assert (= (str.len "\u{E}") 1)) +(assert (= (str.len "\u{44444}") 9)) +(assert (= (str.len "\u") 2)) + +(check-sat) |