blob: 0f125a87027655a4f589c9ea23310c825eafe8a3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic SLIA)
(declare-datatype JSIdentifier ((JSString (jsString String)) (Error )))
(synth-fun substring ((x1 String) (x3 Int))String
((Start String (ntString))
(ntInt Int
(0 x3)
)
(ntJSIdentifier JSIdentifier
(
Error
)
)
(ntString String
(x1
(str.substr ntString ntInt ntInt)
(jsString ntJSIdentifier)
(str.++ ntString ntString)
)
)
)
)
(constraint (= (substring "ey" 1) "e"))
(check-synth)
|
