summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arr2.smt
blob: 213660c0a17391c613348ab4b0ca0aec8e9d7d55 (plain) 
1
2
3
4
5
6
7

(benchmark simple_arr
  :logic QF_AX
  :status unsat
  :extrafuns ((a Array))
  :extrafuns ((i1 Index) (i2 Index) (i3 Index))
  :formula (not (implies (and (= i1 i2) (= i2 i3)) (= (select a i1) (select a i3))))
)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback