diff options
Diffstat (limited to 'test/regress/regress0/strings/char-representations.smt2')
-rw-r--r-- | test/regress/regress0/strings/char-representations.smt2 | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/char-representations.smt2 b/test/regress/regress0/strings/char-representations.smt2 new file mode 100644 index 000000000..aaf119ab4 --- /dev/null +++ b/test/regress/regress0/strings/char-representations.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: sat +(set-logic SLIA) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) + +(assert (= x (_ char #x0D4))) +(assert (= x "\u00d4")) + + +(assert (= y (_ char #x1))) +(assert (= y "\u0001")) + +(assert (= z (_ char #xAF))) +(assert (= z (_ char #x0af))) +(assert (= z "\u{af}")) +(assert (= z "\u00af")) + +(check-sat) |