(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
  (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
)



