blob: 6628ff74654ef92b77c2f12e40e5b01084286da9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic SLIA)
(synth-fun f ((x String)) String
((Start String (ntString))
(ntString String (x "" (str.++ ntStringConst ntString ntString)))
(ntStringConst String ("a" "b" " "))
))
; can be solved with concat PBE strategy, although we currently are not (issue #1259)
; regardless, this is small enough to solve quickly
(constraint (= (f "def") "ab def"))
(check-synth)
|
