summaryrefslogtreecommitdiff
path: root/test/regress/regress0/strings/unicode-esc.smt2
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-04-01 00:30:44 -0500
committerGitHub <noreply@github.com>2020-03-31 22:30:44 -0700
commit936e9c442443799c866a65c6ca3fbdcd3ac9aab8 (patch)
treeb953269087d78261c6a5d81e4d32e4cce70d5f41 /test/regress/regress0/strings/unicode-esc.smt2
parent6d43ef828f5cc84f05b2c52a1991f3fb8505db84 (diff)
Support char smt-lib syntax (#4188)
Towards support for the strings standard. Adds support to (_ char #x ... ) syntax for characters.
Diffstat (limited to 'test/regress/regress0/strings/unicode-esc.smt2')
-rw-r--r--test/regress/regress0/strings/unicode-esc.smt22
1 files changed, 2 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/unicode-esc.smt2 b/test/regress/regress0/strings/unicode-esc.smt2
index 01f5f30ab..02b313d4a 100644
--- a/test/regress/regress0/strings/unicode-esc.smt2
+++ b/test/regress/regress0/strings/unicode-esc.smt2
@@ -26,5 +26,7 @@
(assert (= (str.len "\u{E}") 1))
(assert (= (str.len "\u{44444}") 9))
(assert (= (str.len "\u") 2))
+(assert (= (str.len "\u001") 5))
+(assert (= (str.len "\u0001") 1))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback