(set-info :source "This benchmark comes from bounded model checking of two fifo implementations.
The fifos are reset once at the beginning.
We try to verify behavioral equivalence with k-induction.
All different constraints are used on registers
and also on arrays that model internal memory respectively.
Fifo inputs: 'enqueue', 'dequeue', 'reset' (active low) and 'data_in'.
Fifo output: 'empty', 'full' and 'data_out'.
Bit-width: 32
k: 5
The fifos have an internal memory of size 16, respectively modelled as array.

Contributed by Robert Brummayer (robert.brummayer@gmail.com).")
(set-info :status sat)
(set-info :category "crafted")
(set-logic QF_AUFBV)
(declare-fun head_fs_0 () (_ BitVec 4))
(declare-fun tail_fs_0 () (_ BitVec 4))
(declare-fun full_fs_0 () (_ BitVec 1))
(declare-fun empty_fs_0 () (_ BitVec 1))
(declare-fun data_out_fs_0 () (_ BitVec 32))
(declare-fun head_fq_0 () (_ BitVec 4))
(declare-fun tail_fq_0 () (_ BitVec 4))
(declare-fun full_fq_0 () (_ BitVec 1))
(declare-fun empty_fq_0 () (_ BitVec 1))
(declare-fun data_out_fq_0 () (_ BitVec 32))
(declare-fun reset_0 () (_ BitVec 1))
(declare-fun a40 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun a41 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun enqeue_0 () (_ BitVec 1))
(declare-fun deqeue_0 () (_ BitVec 1))
(declare-fun data_in_0 () (_ BitVec 32))
(declare-fun head_fs_1 () (_ BitVec 4))
(declare-fun tail_fs_1 () (_ BitVec 4))
(declare-fun full_fs_1 () (_ BitVec 1))
(declare-fun empty_fs_1 () (_ BitVec 1))
(declare-fun data_out_fs_1 () (_ BitVec 32))
(declare-fun head_fq_1 () (_ BitVec 4))
(declare-fun tail_fq_1 () (_ BitVec 4))
(declare-fun full_fq_1 () (_ BitVec 1))
(declare-fun empty_fq_1 () (_ BitVec 1))
(declare-fun data_out_fq_1 () (_ BitVec 32))
(declare-fun reset_1 () (_ BitVec 1))
(declare-fun a161 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun a163 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun enqeue_1 () (_ BitVec 1))
(declare-fun deqeue_1 () (_ BitVec 1))
(declare-fun data_in_1 () (_ BitVec 32))
(declare-fun head_fs_2 () (_ BitVec 4))
(declare-fun tail_fs_2 () (_ BitVec 4))
(declare-fun full_fs_2 () (_ BitVec 1))
(declare-fun empty_fs_2 () (_ BitVec 1))
(declare-fun data_out_fs_2 () (_ BitVec 32))
(declare-fun head_fq_2 () (_ BitVec 4))
(declare-fun tail_fq_2 () (_ BitVec 4))
(declare-fun full_fq_2 () (_ BitVec 1))
(declare-fun empty_fq_2 () (_ BitVec 1))
(declare-fun data_out_fq_2 () (_ BitVec 32))
(declare-fun reset_2 () (_ BitVec 1))
(declare-fun a299 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun a303 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun enqeue_2 () (_ BitVec 1))
(declare-fun deqeue_2 () (_ BitVec 1))
(declare-fun data_in_2 () (_ BitVec 32))
(declare-fun head_fs_3 () (_ BitVec 4))
(declare-fun tail_fs_3 () (_ BitVec 4))
(declare-fun full_fs_3 () (_ BitVec 1))
(declare-fun empty_fs_3 () (_ BitVec 1))
(declare-fun data_out_fs_3 () (_ BitVec 32))
(declare-fun head_fq_3 () (_ BitVec 4))
(declare-fun tail_fq_3 () (_ BitVec 4))
(declare-fun full_fq_3 () (_ BitVec 1))
(declare-fun empty_fq_3 () (_ BitVec 1))
(declare-fun data_out_fq_3 () (_ BitVec 32))
(declare-fun reset_3 () (_ BitVec 1))
(declare-fun a443 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun a449 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun enqeue_3 () (_ BitVec 1))
(declare-fun deqeue_3 () (_ BitVec 1))
(declare-fun data_in_3 () (_ BitVec 32))
(declare-fun head_fs_4 () (_ BitVec 4))
(declare-fun tail_fs_4 () (_ BitVec 4))
(declare-fun full_fs_4 () (_ BitVec 1))
(declare-fun empty_fs_4 () (_ BitVec 1))
(declare-fun data_out_fs_4 () (_ BitVec 32))
(declare-fun head_fq_4 () (_ BitVec 4))
(declare-fun tail_fq_4 () (_ BitVec 4))
(declare-fun full_fq_4 () (_ BitVec 1))
(declare-fun empty_fq_4 () (_ BitVec 1))
(declare-fun data_out_fq_4 () (_ BitVec 32))
(declare-fun reset_4 () (_ BitVec 1))
(declare-fun a593 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun a601 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun enqeue_4 () (_ BitVec 1))
(declare-fun deqeue_4 () (_ BitVec 1))
(declare-fun data_in_4 () (_ BitVec 32))
(declare-fun head_fs_5 () (_ BitVec 4))
(declare-fun tail_fs_5 () (_ BitVec 4))
(declare-fun full_fs_5 () (_ BitVec 1))
(declare-fun empty_fs_5 () (_ BitVec 1))
(declare-fun data_out_fs_5 () (_ BitVec 32))
(declare-fun head_fq_5 () (_ BitVec 4))
(declare-fun tail_fq_5 () (_ BitVec 4))
(declare-fun full_fq_5 () (_ BitVec 1))
(declare-fun empty_fq_5 () (_ BitVec 1))
(declare-fun data_out_fq_5 () (_ BitVec 32))
(declare-fun reset_5 () (_ BitVec 1))
(declare-fun a749 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun a759 () (Array (_ BitVec 4) (_ BitVec 32)))
(assert (let ((_let_0 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat head_fs_0 tail_fs_0) full_fs_0) empty_fs_0) data_out_fs_0) head_fq_0) tail_fq_0) full_fq_0) empty_fq_0) data_out_fq_0) reset_0))) (let ((_let_1 (= (_ bv1 1) full_fs_0))) (let ((_let_2 (= (_ bv1 1) enqeue_0))) (let ((_let_3 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_0) (bvnot deqeue_0))) (bvnot (bvand enqeue_0 deqeue_0)))))) (let ((_let_4 (= (_ bv1 1) reset_0))) (let ((_let_5 (= (_ bv1 1) deqeue_0))) (let ((_let_6 (bvadd (_ bv1 4) head_fq_0))) (let ((_let_7 (bvadd (_ bv1 4) tail_fq_0))) (let ((_let_8 (= (_ bv1 1) full_fq_0))) (let ((_let_9 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat head_fs_1 tail_fs_1) full_fs_1) empty_fs_1) data_out_fs_1) head_fq_1) tail_fq_1) full_fq_1) empty_fq_1) data_out_fq_1) reset_1))) (let ((_let_10 (= (_ bv1 1) full_fs_1))) (let ((_let_11 (= (_ bv1 1) enqeue_1))) (let ((_let_12 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_1) (bvnot deqeue_1))) (bvnot (bvand enqeue_1 deqeue_1)))))) (let ((_let_13 (= (_ bv1 1) reset_1))) (let ((_let_14 (= (_ bv1 1) deqeue_1))) (let ((_let_15 (bvadd (_ bv1 4) head_fq_1))) (let ((_let_16 (bvadd (_ bv1 4) tail_fq_1))) (let ((_let_17 (= (_ bv1 1) full_fq_1))) (let ((_let_18 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat head_fs_2 tail_fs_2) full_fs_2) empty_fs_2) data_out_fs_2) head_fq_2) tail_fq_2) full_fq_2) empty_fq_2) data_out_fq_2) reset_2))) (let ((_let_19 (= (_ bv1 1) full_fs_2))) (let ((_let_20 (= (_ bv1 1) enqeue_2))) (let ((_let_21 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_2) (bvnot deqeue_2))) (bvnot (bvand enqeue_2 deqeue_2)))))) (let ((_let_22 (= (_ bv1 1) reset_2))) (let ((_let_23 (= (_ bv1 1) deqeue_2))) (let ((_let_24 (bvadd (_ bv1 4) head_fq_2))) (let ((_let_25 (bvadd (_ bv1 4) tail_fq_2))) (let ((_let_26 (= (_ bv1 1) full_fq_2))) (let ((_let_27 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat head_fs_3 tail_fs_3) full_fs_3) empty_fs_3) data_out_fs_3) head_fq_3) tail_fq_3) full_fq_3) empty_fq_3) data_out_fq_3) reset_3))) (let ((_let_28 (= (_ bv1 1) full_fs_3))) (let ((_let_29 (= (_ bv1 1) enqeue_3))) (let ((_let_30 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_3) (bvnot deqeue_3))) (bvnot (bvand enqeue_3 deqeue_3)))))) (let ((_let_31 (= (_ bv1 1) reset_3))) (let ((_let_32 (= (_ bv1 1) deqeue_3))) (let ((_let_33 (bvadd (_ bv1 4) head_fq_3))) (let ((_let_34 (bvadd (_ bv1 4) tail_fq_3))) (let ((_let_35 (= (_ bv1 1) full_fq_3))) (let ((_let_36 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat head_fs_4 tail_fs_4) full_fs_4) empty_fs_4) data_out_fs_4) head_fq_4) tail_fq_4) full_fq_4) empty_fq_4) data_out_fq_4) reset_4))) (let ((_let_37 (= (_ bv1 1) full_fs_4))) (let ((_let_38 (= (_ bv1 1) enqeue_4))) (let ((_let_39 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_4) (bvnot deqeue_4))) (bvnot (bvand enqeue_4 deqeue_4)))))) (let ((_let_40 (= (_ bv1 1) reset_4))) (let ((_let_41 (= (_ bv1 1) deqeue_4))) (let ((_let_42 (bvadd (_ bv1 4) head_fq_4))) (let ((_let_43 (bvadd (_ bv1 4) tail_fq_4))) (let ((_let_44 (= (_ bv1 1) full_fq_4))) (let ((_let_45 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat head_fs_5 tail_fs_5) full_fs_5) empty_fs_5) data_out_fs_5) head_fq_5) tail_fq_5) full_fq_5) empty_fq_5) data_out_fq_5) reset_5))) (not (= (bvand reset_5 (bvand (bvnot (bvand (ite (= data_out_fs_5 data_out_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= full_fs_5 full_fq_5) (_ bv1 1) (_ bv0 1)) (ite (= empty_fs_5 empty_fq_5) (_ bv1 1) (_ bv0 1))))) (bvand reset_5 (bvand (ite (= (ite _let_40 (ite _let_39 (ite _let_38 (ite _let_44 a601 (store a601 tail_fq_4 data_in_4)) a601) a601) a601) a759) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_40 (ite _let_39 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_4) deqeue_4)) (select a601 head_fq_4) data_out_fq_4) data_out_fq_4) data_out_fq_4) data_out_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_40 (ite _let_39 (ite _let_38 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_4 _let_42) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fq_4)) empty_fq_4) (_ bv1 1)) empty_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_40 (ite _let_39 (ite _let_41 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_4 (bvadd (_ bv1 4) _let_43)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fq_4)) full_fq_4) (_ bv0 1)) full_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_40 (ite _let_39 (ite _let_38 (ite _let_44 tail_fq_4 _let_43) tail_fq_4) tail_fq_4) (_ bv0 4)) tail_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_40 (ite _let_39 (ite _let_41 (ite (= (_ bv1 1) empty_fq_4) head_fq_4 _let_42) head_fq_4) head_fq_4) (_ bv0 4)) head_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_40 (ite _let_39 (ite _let_38 (ite _let_37 a593 (store a593 tail_fs_4 data_in_4)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store a593 (_ bv0 4) (select a593 (_ bv1 4))) (_ bv1 4) (select a593 (_ bv2 4))) (_ bv2 4) (select a593 (_ bv3 4))) (_ bv3 4) (select a593 (_ bv4 4))) (_ bv4 4) (select a593 (_ bv5 4))) (_ bv5 4) (select a593 (_ bv6 4))) (_ bv6 4) (select a593 (_ bv7 4))) (_ bv7 4) (select a593 (_ bv8 4))) (_ bv8 4) (select a593 (_ bv9 4))) (_ bv9 4) (select a593 (_ bv10 4))) (_ bv10 4) (select a593 (_ bv11 4))) (_ bv11 4) (select a593 (_ bv12 4))) (_ bv12 4) (select a593 (_ bv13 4))) (_ bv13 4) (select a593 (_ bv14 4)))) a593) a593) a749) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_40 (ite _let_39 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_4) deqeue_4)) (select a593 head_fs_4) data_out_fs_4) data_out_fs_4) data_out_fs_4) data_out_fs_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_40 (ite _let_39 (ite _let_38 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv1 4) tail_fs_4) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fs_4)) empty_fs_4) (_ bv1 1)) empty_fs_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_40 (ite _let_39 (ite _let_41 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv14 4) tail_fs_4) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fs_4)) full_fs_4) (_ bv0 1)) full_fs_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_40 (ite _let_39 (ite _let_38 (ite _let_37 tail_fs_4 (bvadd (_ bv1 4) tail_fs_4)) (ite (= (_ bv1 1) empty_fs_4) tail_fs_4 (bvadd (_ bv15 4) tail_fs_4))) tail_fs_4) (_ bv0 4)) tail_fs_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (_ bv0 4) head_fs_5) (_ bv1 1) (_ bv0 1)) (bvand (bvnot (bvand (bvand (bvnot (bvand (bvand (bvand (bvand (bvnot (ite (= a40 a749) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a161 a749) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a299 a749) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a443 a749) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a593 a749) (_ bv1 1) (_ bv0 1))))) (bvnot (bvand (bvand (bvand (bvand (bvnot (ite (= a41 a759) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a163 a759) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a303 a759) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a449 a759) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a601 a759) (_ bv1 1) (_ bv0 1)))))) (bvnot (bvand (bvand (bvand (bvand (bvnot (ite (= _let_0 _let_45) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= _let_9 _let_45) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= _let_18 _let_45) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= _let_27 _let_45) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= _let_36 _let_45) (_ bv1 1) (_ bv0 1))))))) (bvand (bvnot (bvand reset_4 (bvnot (bvand (ite (= data_out_fs_4 data_out_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= full_fs_4 full_fq_4) (_ bv1 1) (_ bv0 1)) (ite (= empty_fs_4 empty_fq_4) (_ bv1 1) (_ bv0 1))))))) (bvand reset_4 (bvand (ite (= (ite _let_31 (ite _let_30 (ite _let_29 (ite _let_35 a449 (store a449 tail_fq_3 data_in_3)) a449) a449) a449) a601) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_31 (ite _let_30 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_3) deqeue_3)) (select a449 head_fq_3) data_out_fq_3) data_out_fq_3) data_out_fq_3) data_out_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_31 (ite _let_30 (ite _let_29 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_3 _let_33) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fq_3)) empty_fq_3) (_ bv1 1)) empty_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_31 (ite _let_30 (ite _let_32 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_3 (bvadd (_ bv1 4) _let_34)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fq_3)) full_fq_3) (_ bv0 1)) full_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_31 (ite _let_30 (ite _let_29 (ite _let_35 tail_fq_3 _let_34) tail_fq_3) tail_fq_3) (_ bv0 4)) tail_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_31 (ite _let_30 (ite _let_32 (ite (= (_ bv1 1) empty_fq_3) head_fq_3 _let_33) head_fq_3) head_fq_3) (_ bv0 4)) head_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_31 (ite _let_30 (ite _let_29 (ite _let_28 a443 (store a443 tail_fs_3 data_in_3)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store a443 (_ bv0 4) (select a443 (_ bv1 4))) (_ bv1 4) (select a443 (_ bv2 4))) (_ bv2 4) (select a443 (_ bv3 4))) (_ bv3 4) (select a443 (_ bv4 4))) (_ bv4 4) (select a443 (_ bv5 4))) (_ bv5 4) (select a443 (_ bv6 4))) (_ bv6 4) (select a443 (_ bv7 4))) (_ bv7 4) (select a443 (_ bv8 4))) (_ bv8 4) (select a443 (_ bv9 4))) (_ bv9 4) (select a443 (_ bv10 4))) (_ bv10 4) (select a443 (_ bv11 4))) (_ bv11 4) (select a443 (_ bv12 4))) (_ bv12 4) (select a443 (_ bv13 4))) (_ bv13 4) (select a443 (_ bv14 4)))) a443) a443) a593) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_31 (ite _let_30 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_3) deqeue_3)) (select a443 head_fs_3) data_out_fs_3) data_out_fs_3) data_out_fs_3) data_out_fs_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_31 (ite _let_30 (ite _let_29 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv1 4) tail_fs_3) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fs_3)) empty_fs_3) (_ bv1 1)) empty_fs_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_31 (ite _let_30 (ite _let_32 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv14 4) tail_fs_3) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fs_3)) full_fs_3) (_ bv0 1)) full_fs_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_31 (ite _let_30 (ite _let_29 (ite _let_28 tail_fs_3 (bvadd (_ bv1 4) tail_fs_3)) (ite (= (_ bv1 1) empty_fs_3) tail_fs_3 (bvadd (_ bv15 4) tail_fs_3))) tail_fs_3) (_ bv0 4)) tail_fs_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (_ bv0 4) head_fs_4) (_ bv1 1) (_ bv0 1)) (bvand (bvnot (bvand (bvand (bvnot (bvand (bvand (bvand (bvnot (ite (= a40 a593) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a161 a593) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a299 a593) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a443 a593) (_ bv1 1) (_ bv0 1))))) (bvnot (bvand (bvand (bvand (bvnot (ite (= a41 a601) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a163 a601) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a303 a601) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a449 a601) (_ bv1 1) (_ bv0 1)))))) (bvnot (bvand (bvand (bvand (bvnot (ite (= _let_0 _let_36) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= _let_9 _let_36) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= _let_18 _let_36) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= _let_27 _let_36) (_ bv1 1) (_ bv0 1))))))) (bvand (bvnot (bvand reset_3 (bvnot (bvand (ite (= data_out_fs_3 data_out_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= full_fs_3 full_fq_3) (_ bv1 1) (_ bv0 1)) (ite (= empty_fs_3 empty_fq_3) (_ bv1 1) (_ bv0 1))))))) (bvand reset_3 (bvand (ite (= (ite _let_22 (ite _let_21 (ite _let_20 (ite _let_26 a303 (store a303 tail_fq_2 data_in_2)) a303) a303) a303) a449) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_22 (ite _let_21 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_2) deqeue_2)) (select a303 head_fq_2) data_out_fq_2) data_out_fq_2) data_out_fq_2) data_out_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_22 (ite _let_21 (ite _let_20 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_2 _let_24) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fq_2)) empty_fq_2) (_ bv1 1)) empty_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_22 (ite _let_21 (ite _let_23 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_2 (bvadd (_ bv1 4) _let_25)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fq_2)) full_fq_2) (_ bv0 1)) full_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_22 (ite _let_21 (ite _let_20 (ite _let_26 tail_fq_2 _let_25) tail_fq_2) tail_fq_2) (_ bv0 4)) tail_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_22 (ite _let_21 (ite _let_23 (ite (= (_ bv1 1) empty_fq_2) head_fq_2 _let_24) head_fq_2) head_fq_2) (_ bv0 4)) head_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_22 (ite _let_21 (ite _let_20 (ite _let_19 a299 (store a299 tail_fs_2 data_in_2)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store a299 (_ bv0 4) (select a299 (_ bv1 4))) (_ bv1 4) (select a299 (_ bv2 4))) (_ bv2 4) (select a299 (_ bv3 4))) (_ bv3 4) (select a299 (_ bv4 4))) (_ bv4 4) (select a299 (_ bv5 4))) (_ bv5 4) (select a299 (_ bv6 4))) (_ bv6 4) (select a299 (_ bv7 4))) (_ bv7 4) (select a299 (_ bv8 4))) (_ bv8 4) (select a299 (_ bv9 4))) (_ bv9 4) (select a299 (_ bv10 4))) (_ bv10 4) (select a299 (_ bv11 4))) (_ bv11 4) (select a299 (_ bv12 4))) (_ bv12 4) (select a299 (_ bv13 4))) (_ bv13 4) (select a299 (_ bv14 4)))) a299) a299) a443) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_22 (ite _let_21 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_2) deqeue_2)) (select a299 head_fs_2) data_out_fs_2) data_out_fs_2) data_out_fs_2) data_out_fs_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_22 (ite _let_21 (ite _let_20 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv1 4) tail_fs_2) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fs_2)) empty_fs_2) (_ bv1 1)) empty_fs_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_22 (ite _let_21 (ite _let_23 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv14 4) tail_fs_2) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fs_2)) full_fs_2) (_ bv0 1)) full_fs_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_22 (ite _let_21 (ite _let_20 (ite _let_19 tail_fs_2 (bvadd (_ bv1 4) tail_fs_2)) (ite (= (_ bv1 1) empty_fs_2) tail_fs_2 (bvadd (_ bv15 4) tail_fs_2))) tail_fs_2) (_ bv0 4)) tail_fs_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (_ bv0 4) head_fs_3) (_ bv1 1) (_ bv0 1)) (bvand (bvnot (bvand (bvand (bvnot (bvand (bvand (bvnot (ite (= a40 a443) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a161 a443) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a299 a443) (_ bv1 1) (_ bv0 1))))) (bvnot (bvand (bvand (bvnot (ite (= a41 a449) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a163 a449) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a303 a449) (_ bv1 1) (_ bv0 1)))))) (bvnot (bvand (bvand (bvnot (ite (= _let_0 _let_27) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= _let_9 _let_27) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= _let_18 _let_27) (_ bv1 1) (_ bv0 1))))))) (bvand (bvnot (bvand reset_2 (bvnot (bvand (ite (= data_out_fs_2 data_out_fq_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= full_fs_2 full_fq_2) (_ bv1 1) (_ bv0 1)) (ite (= empty_fs_2 empty_fq_2) (_ bv1 1) (_ bv0 1))))))) (bvand reset_2 (bvand (ite (= (ite _let_13 (ite _let_12 (ite _let_11 (ite _let_17 a163 (store a163 tail_fq_1 data_in_1)) a163) a163) a163) a303) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_13 (ite _let_12 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_1) deqeue_1)) (select a163 head_fq_1) data_out_fq_1) data_out_fq_1) data_out_fq_1) data_out_fq_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_13 (ite _let_12 (ite _let_11 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_1 _let_15) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fq_1)) empty_fq_1) (_ bv1 1)) empty_fq_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_13 (ite _let_12 (ite _let_14 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_1 (bvadd (_ bv1 4) _let_16)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fq_1)) full_fq_1) (_ bv0 1)) full_fq_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_13 (ite _let_12 (ite _let_11 (ite _let_17 tail_fq_1 _let_16) tail_fq_1) tail_fq_1) (_ bv0 4)) tail_fq_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_13 (ite _let_12 (ite _let_14 (ite (= (_ bv1 1) empty_fq_1) head_fq_1 _let_15) head_fq_1) head_fq_1) (_ bv0 4)) head_fq_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_13 (ite _let_12 (ite _let_11 (ite _let_10 a161 (store a161 tail_fs_1 data_in_1)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store a161 (_ bv0 4) (select a161 (_ bv1 4))) (_ bv1 4) (select a161 (_ bv2 4))) (_ bv2 4) (select a161 (_ bv3 4))) (_ bv3 4) (select a161 (_ bv4 4))) (_ bv4 4) (select a161 (_ bv5 4))) (_ bv5 4) (select a161 (_ bv6 4))) (_ bv6 4) (select a161 (_ bv7 4))) (_ bv7 4) (select a161 (_ bv8 4))) (_ bv8 4) (select a161 (_ bv9 4))) (_ bv9 4) (select a161 (_ bv10 4))) (_ bv10 4) (select a161 (_ bv11 4))) (_ bv11 4) (select a161 (_ bv12 4))) (_ bv12 4) (select a161 (_ bv13 4))) (_ bv13 4) (select a161 (_ bv14 4)))) a161) a161) a299) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_13 (ite _let_12 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_1) deqeue_1)) (select a161 head_fs_1) data_out_fs_1) data_out_fs_1) data_out_fs_1) data_out_fs_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_13 (ite _let_12 (ite _let_11 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv1 4) tail_fs_1) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fs_1)) empty_fs_1) (_ bv1 1)) empty_fs_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_13 (ite _let_12 (ite _let_14 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv14 4) tail_fs_1) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fs_1)) full_fs_1) (_ bv0 1)) full_fs_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_13 (ite _let_12 (ite _let_11 (ite _let_10 tail_fs_1 (bvadd (_ bv1 4) tail_fs_1)) (ite (= (_ bv1 1) empty_fs_1) tail_fs_1 (bvadd (_ bv15 4) tail_fs_1))) tail_fs_1) (_ bv0 4)) tail_fs_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (_ bv0 4) head_fs_2) (_ bv1 1) (_ bv0 1)) (bvand (bvnot (bvand (bvand (bvnot (bvand (bvnot (ite (= a40 a299) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a161 a299) (_ bv1 1) (_ bv0 1))))) (bvnot (bvand (bvnot (ite (= a41 a303) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a163 a303) (_ bv1 1) (_ bv0 1)))))) (bvnot (bvand (bvnot (ite (= _let_0 _let_18) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= _let_9 _let_18) (_ bv1 1) (_ bv0 1))))))) (bvand (bvnot (bvand reset_1 (bvnot (bvand (ite (= data_out_fs_1 data_out_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= full_fs_1 full_fq_1) (_ bv1 1) (_ bv0 1)) (ite (= empty_fs_1 empty_fq_1) (_ bv1 1) (_ bv0 1))))))) (bvand reset_1 (bvand (ite (= (ite _let_4 (ite _let_3 (ite _let_2 (ite _let_8 a41 (store a41 tail_fq_0 data_in_0)) a41) a41) a41) a163) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_4 (ite _let_3 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_0) deqeue_0)) (select a41 head_fq_0) data_out_fq_0) data_out_fq_0) data_out_fq_0) data_out_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_4 (ite _let_3 (ite _let_2 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_0 _let_6) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fq_0)) empty_fq_0) (_ bv1 1)) empty_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_4 (ite _let_3 (ite _let_5 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_0 (bvadd (_ bv1 4) _let_7)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fq_0)) full_fq_0) (_ bv0 1)) full_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_4 (ite _let_3 (ite _let_2 (ite _let_8 tail_fq_0 _let_7) tail_fq_0) tail_fq_0) (_ bv0 4)) tail_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_4 (ite _let_3 (ite _let_5 (ite (= (_ bv1 1) empty_fq_0) head_fq_0 _let_6) head_fq_0) head_fq_0) (_ bv0 4)) head_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_4 (ite _let_3 (ite _let_2 (ite _let_1 a40 (store a40 tail_fs_0 data_in_0)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store a40 (_ bv0 4) (select a40 (_ bv1 4))) (_ bv1 4) (select a40 (_ bv2 4))) (_ bv2 4) (select a40 (_ bv3 4))) (_ bv3 4) (select a40 (_ bv4 4))) (_ bv4 4) (select a40 (_ bv5 4))) (_ bv5 4) (select a40 (_ bv6 4))) (_ bv6 4) (select a40 (_ bv7 4))) (_ bv7 4) (select a40 (_ bv8 4))) (_ bv8 4) (select a40 (_ bv9 4))) (_ bv9 4) (select a40 (_ bv10 4))) (_ bv10 4) (select a40 (_ bv11 4))) (_ bv11 4) (select a40 (_ bv12 4))) (_ bv12 4) (select a40 (_ bv13 4))) (_ bv13 4) (select a40 (_ bv14 4)))) a40) a40) a161) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_4 (ite _let_3 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_0) deqeue_0)) (select a40 head_fs_0) data_out_fs_0) data_out_fs_0) data_out_fs_0) data_out_fs_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_4 (ite _let_3 (ite _let_2 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv1 4) tail_fs_0) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fs_0)) empty_fs_0) (_ bv1 1)) empty_fs_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_4 (ite _let_3 (ite _let_5 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv14 4) tail_fs_0) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fs_0)) full_fs_0) (_ bv0 1)) full_fs_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_4 (ite _let_3 (ite _let_2 (ite _let_1 tail_fs_0 (bvadd (_ bv1 4) tail_fs_0)) (ite (= (_ bv1 1) empty_fs_0) tail_fs_0 (bvadd (_ bv15 4) tail_fs_0))) tail_fs_0) (_ bv0 4)) tail_fs_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (_ bv0 4) head_fs_1) (_ bv1 1) (_ bv0 1)) (bvand (bvnot (bvand reset_0 (bvnot (bvand (ite (= data_out_fs_0 data_out_fq_0) (_ bv1 1) (_ bv0 1)) (bvand (ite (= full_fs_0 full_fq_0) (_ bv1 1) (_ bv0 1)) (ite (= empty_fs_0 empty_fq_0) (_ bv1 1) (_ bv0 1))))))) (bvnot (bvand (bvand (ite (= a40 a161) (_ bv1 1) (_ bv0 1)) (ite (= a41 a163) (_ bv1 1) (_ bv0 1))) (ite (= _let_0 _let_9) (_ bv1 1) (_ bv0 1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (_ bv0 1))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)