(declare-const s State)
(declare-const t Index)
(declare-const other Index)
(declare-const a Index)
(declare-const v Word)
(declare-const r Index)
(declare-const destination Index)

(assert (bvult t #x02))
(assert (bvult other #x02))
(assert (bvult a #x10))
(assert (bvult r #x04))
(assert (bvule (at (heads s) t) (at (tails s) t)))
(assert (bvult (at (tails s) t) #x40))
(assert (bvult (pending s t) #x08))
(assert (distinct other t))

(push 1)
(assert (distinct (read (write s t a v) t a) v))
(check-sat)
(pop 1)

(push 1)
(assert (distinct (memory (write s t a v)) (memory s)))
(check-sat)
(pop 1)

(push 1)
(assert (distinct (pending (write s t a v) t) (bvadd (pending s t) #x01)))
(check-sat)
(pop 1)

(push 1)
(assert (distinct (pending (write s t a v) other) (pending s other)))
(check-sat)
(pop 1)

(push 1)
(assert (bvugt (pending s t) #x00))
(assert (distinct (pending (drain s t) t) (bvsub (pending s t) #x01)))
(check-sat)
(pop 1)

(push 1)
(assert (distinct (pending (drain s t) other) (pending s other)))
(check-sat)
(pop 1)

(push 1)
(assert (distinct (reg (put s t r v) t r) v))
(check-sat)
(pop 1)

(push 1)
(assert (distinct (pc (advance s t destination) t) destination))
(check-sat)
(pop 1)

(push 1)
(assert (distinct (pc (advance s t destination) other) (pc s other)))
(check-sat)
(pop 1)

(push 1)
(assert (distinct (at (critical (mark s t #x01)) t) #x01))
(check-sat)
(pop 1)

(push 1)
(assert (distinct (at (memory (exchange s t a r v)) a) v))
(check-sat)
(pop 1)

(push 1)
(assert (distinct (reg (exchange s t a r v) t r) (at (memory s) a)))
(check-sat)
(pop 1)

(push 1)
(assert (distinct (reg (load-step s t a r) t r) (read s t a)))
(check-sat)
(pop 1)

(push 1)
(assert (distinct (memory (load-step s t a r)) (memory s)))
(check-sat)
(pop 1)

(push 1)
(assert (distinct (pending (fence-step s t) t) (pending s t)))
(check-sat)
(pop 1)

(push 1)
(assert (= (pending s t) #x00))
(assert (distinct (at (memory (store-step s t a v true)) a) v))
(check-sat)
(pop 1)