blob: 71a5a59872ed90d4dbfcbdd7b74aa69bb44ff3f6 (
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
27
28
29
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
(declare-datatype JSIdentifier ((JSString (jsString String)) (Error)))
(synth-fun substring ((x1 String) (x3 Int)) String
((ntString String) (ntInt Int) (ntJSIdentifier JSIdentifier))
(
(ntString String
(x1
(str.substr ntString ntInt ntInt)
(jsString ntJSIdentifier)
(str.++ ntString ntString)
)
)
(ntInt Int
(0 x3)
)
(ntJSIdentifier JSIdentifier
(
Error
)
)
)
)
(constraint (= (substring "ey" 1) "e"))
(check-synth)
|
