(benchmark array_alu
  :logic UNKNOWN
  :extrasorts (Array Index Data Operation)
  :extrapreds ((bubble_wb) (bubble_ex) (stall))
  :extrafuns ((read Array Index Data))
  :extrafuns ((write Array Index Data Array)
	      (alu Operation Data Data Data)
	      (regfile Array)
	      (dest Index)
	      (dest_ex Index)
	      (dest_wb Index)
	      (src1 Index)
	      (src2 Index)
	      (result Data)
	      (op Operation)
	      (op_ex Operation)
	      (arg1 Data)
	      (arg2 Data))
  :formula
  (not
    (implies
      (and (forall (?a Array) (?i Index) (?e Data) (= ?e (read (write ?a ?i ?e) ?i)))
	(forall (?a Array) (?i Index) (?j Index) (?e Data) 
	  (implies (not (= ?i ?j))
	    (= (read ?a ?j) (read (write ?a ?i ?e) ?j)))))
      (let (?t2 (ite bubble_wb regfile (write regfile dest_wb result)))
	(let (?t3 (alu op_ex arg1 arg2))
	  (let (?t1 (ite bubble_ex ?t2 (write ?t2 dest_ex ?t3)))
	    (not
	      (= 
		(ite stall ?t1
		  (write ?t1 dest (alu op (read ?t1 src1) (read ?t1 src2))))
		(ite stall
		  ?t1
		  (write ?t1
		    dest
		    (alu op
		      (ite (or bubble_ex (not (= src1 dest_ex)))
			(read ?t2 src1)
			?t3)
		      (ite (or bubble_ex (not (= dest_ex src2)))
			(read ?t2 src2)
			?t3)))))))))))
  :status unsat
)
