test/regress/regress0/sygus/array-grammar-store.sy


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

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

(synth-fun f
  ((s (Array (BitVec 4) (BitVec 4))) (t (BitVec 4)))
  (Array (BitVec 4) (BitVec 4))
  )

(declare-var x (Array (BitVec 4) (BitVec 4)))

(constraint (= (= (store x #b0000 #b0000) (store x #b0001 #b0000)) (= (f x #b0000) (f x #b0001))))

(check-synth)