test/regress/regress3/strings-any-term.sy


1
2
3
4
5
6
7
8
9
10

; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term --sygus-active-gen=none
(set-logic ALL)
(synth-fun f ((x String) (y String)) Int)
(declare-var x String)
(constraint (= (f "A" "BC") 207))
(constraint (= (f "BB" "CC") 214))
(constraint (= (f "BCB" "") 21))
(constraint (= (f "BCBD" "") 28))
(check-synth)