summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sygus/array-grammar-select.sy
blob: d216bbb247818d9c4687b093acceee1ec6a42eed (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

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

(synth-fun f
  ((s (Array Int Int)) (t Int))
  Int
  )

(declare-var x (Array Int Int))

(constraint (= (= (select x 0) (select x 1)) (= (f x 0) (f x 1))))


(check-synth)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback