test/regress/regress1/sygus/strings-any-term1.sy


1
2
3
4
5
6
7
8
9
10

; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term
(set-logic ALL)
(synth-fun f ((x String) (y String)) Int)
(declare-var x String)
(constraint (= (f "A" "BC") 11))
(constraint (= (f "BB" "CC") 18))
(constraint (= (f "BCB" "") 25))
(constraint (= (f "BCBD" "") 32))
(check-synth)