test/regress/regress0/strings/char-representations.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

; COMMAND-LINE: --lang=smt2.6
; 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)