path: root/test/regress/regress2/sygus/strings-no-syntax-len.sy

; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)

(synth-fun f ((x String)) Int)

(declare-var x String)
(constraint (>= (f (str.++ "A" x)) (f x)))
(constraint (= (f "A") 2))
(constraint (= (f "BB") 4))
(constraint (= (f "BCB") 6))

(check-synth)