blob: 681d3ccff4e89ef7b3b1e8115df4318277a8529b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
(synth-fun f ((x String)) String
((ntString String) (ntStringConst String))
((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)
|
