test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy


1
2
3
4
5
6
7
8
9
10
11
12
13
14

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

(synth-fun f ((x String) (y String)) String)
(synth-fun g ((x String) (y String)) String)

(declare-var x String)
(declare-var y String)

(constraint (= (f x y) (str.replace (str.++ x y) "A" "ABCD")))
(constraint (= (g x y) (str.replace (f x y) "B" "CDE")))

(check-synth)