(set-option :incremental false)
(set-info :source "This benchmark comes from bounded model checking of two fifo implementations.
The fifos are resetted once at the beginning. We show that the
implementations are behaviorally equivalent up to a bound of 5 clock cycles.
Fifo inputs: 'enqueue', 'dequeue', 'reset' (active low) and 'data_in'.
Fifo output: 'empty', 'full' and 'data_out'.
Bit-width: 32
The fifos have an internal memory of size 16, respectively modelled as array.

Contributed by Robert Brummayer (robert.brummayer@gmail.com).")
(set-info :status unsat)
(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 a30 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun a31 () (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 a158 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun a159 () (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 a281 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun a282 () (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 a404 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun a405 () (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 a527 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun a528 () (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 a650 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun a651 () (Array (_ BitVec 4) (_ BitVec 32)))
(assert (let ((_let_0 (bvnot empty_fs_0))) (let ((_let_1 (bvnot empty_fq_0))) (let ((_let_2 (= (_ bv1 1) full_fs_0))) (let ((_let_3 (= (_ bv1 1) enqeue_0))) (let ((_let_4 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_0) (bvnot deqeue_0))) (bvnot (bvand enqeue_0 deqeue_0)))))) (let ((_let_5 (= (_ bv1 1) reset_0))) (let ((_let_6 (= (_ bv1 1) deqeue_0))) (let ((_let_7 (bvadd (_ bv1 4) head_fq_0))) (let ((_let_8 (bvadd (_ bv1 4) tail_fq_0))) (let ((_let_9 (= (_ bv1 1) full_fq_0))) (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 (= (_ bv1 1) full_fs_2))) (let ((_let_19 (= (_ bv1 1) enqeue_2))) (let ((_let_20 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_2) (bvnot deqeue_2))) (bvnot (bvand enqeue_2 deqeue_2)))))) (let ((_let_21 (= (_ bv1 1) reset_2))) (let ((_let_22 (= (_ bv1 1) deqeue_2))) (let ((_let_23 (bvadd (_ bv1 4) head_fq_2))) (let ((_let_24 (bvadd (_ bv1 4) tail_fq_2))) (let ((_let_25 (= (_ bv1 1) full_fq_2))) (let ((_let_26 (= (_ bv1 1) full_fs_3))) (let ((_let_27 (= (_ bv1 1) enqeue_3))) (let ((_let_28 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_3) (bvnot deqeue_3))) (bvnot (bvand enqeue_3 deqeue_3)))))) (let ((_let_29 (= (_ bv1 1) reset_3))) (let ((_let_30 (= (_ bv1 1) deqeue_3))) (let ((_let_31 (bvadd (_ bv1 4) head_fq_3))) (let ((_let_32 (bvadd (_ bv1 4) tail_fq_3))) (let ((_let_33 (= (_ bv1 1) full_fq_3))) (let ((_let_34 (= (_ bv1 1) full_fs_4))) (let ((_let_35 (= (_ bv1 1) enqeue_4))) (let ((_let_36 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_4) (bvnot deqeue_4))) (bvnot (bvand enqeue_4 deqeue_4)))))) (let ((_let_37 (= (_ bv1 1) reset_4))) (let ((_let_38 (= (_ bv1 1) deqeue_4))) (let ((_let_39 (bvadd (_ bv1 4) head_fq_4))) (let ((_let_40 (bvadd (_ bv1 4) tail_fq_4))) (let ((_let_41 (= (_ bv1 1) full_fq_4))) (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_37 (ite _let_36 (ite _let_35 (ite _let_41 a528 (store a528 tail_fq_4 data_in_4)) a528) a528) a528) a651) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_37 (ite _let_36 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_4) deqeue_4)) (select a528 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_37 (ite _let_36 (ite _let_35 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_4 _let_39) (_ 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_37 (ite _let_36 (ite _let_38 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_4 (bvadd (_ bv1 4) _let_40)) (_ 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_37 (ite _let_36 (ite _let_35 (ite _let_41 tail_fq_4 _let_40) tail_fq_4) tail_fq_4) (_ bv0 4)) tail_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_37 (ite _let_36 (ite _let_38 (ite (= (_ bv1 1) empty_fq_4) head_fq_4 _let_39) head_fq_4) head_fq_4) (_ bv0 4)) head_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_37 (ite _let_36 (ite _let_35 (ite _let_34 a527 (store a527 tail_fs_4 data_in_4)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store a527 (_ bv0 4) (select a527 (_ bv1 4))) (_ bv1 4) (select a527 (_ bv2 4))) (_ bv2 4) (select a527 (_ bv3 4))) (_ bv3 4) (select a527 (_ bv4 4))) (_ bv4 4) (select a527 (_ bv5 4))) (_ bv5 4) (select a527 (_ bv6 4))) (_ bv6 4) (select a527 (_ bv7 4))) (_ bv7 4) (select a527 (_ bv8 4))) (_ bv8 4) (select a527 (_ bv9 4))) (_ bv9 4) (select a527 (_ bv10 4))) (_ bv10 4) (select a527 (_ bv11 4))) (_ bv11 4) (select a527 (_ bv12 4))) (_ bv12 4) (select a527 (_ bv13 4))) (_ bv13 4) (select a527 (_ bv14 4)))) a527) a527) a650) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_37 (ite _let_36 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_4) deqeue_4)) (select a527 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_37 (ite _let_36 (ite _let_35 (_ 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_37 (ite _let_36 (ite _let_38 (_ 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_37 (ite _let_36 (ite _let_35 (ite _let_34 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 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_29 (ite _let_28 (ite _let_27 (ite _let_33 a405 (store a405 tail_fq_3 data_in_3)) a405) a405) a405) a528) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_29 (ite _let_28 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_3) deqeue_3)) (select a405 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_29 (ite _let_28 (ite _let_27 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_3 _let_31) (_ 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_29 (ite _let_28 (ite _let_30 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_3 (bvadd (_ bv1 4) _let_32)) (_ 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_29 (ite _let_28 (ite _let_27 (ite _let_33 tail_fq_3 _let_32) tail_fq_3) tail_fq_3) (_ bv0 4)) tail_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_29 (ite _let_28 (ite _let_30 (ite (= (_ bv1 1) empty_fq_3) head_fq_3 _let_31) head_fq_3) head_fq_3) (_ bv0 4)) head_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_29 (ite _let_28 (ite _let_27 (ite _let_26 a404 (store a404 tail_fs_3 data_in_3)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store a404 (_ bv0 4) (select a404 (_ bv1 4))) (_ bv1 4) (select a404 (_ bv2 4))) (_ bv2 4) (select a404 (_ bv3 4))) (_ bv3 4) (select a404 (_ bv4 4))) (_ bv4 4) (select a404 (_ bv5 4))) (_ bv5 4) (select a404 (_ bv6 4))) (_ bv6 4) (select a404 (_ bv7 4))) (_ bv7 4) (select a404 (_ bv8 4))) (_ bv8 4) (select a404 (_ bv9 4))) (_ bv9 4) (select a404 (_ bv10 4))) (_ bv10 4) (select a404 (_ bv11 4))) (_ bv11 4) (select a404 (_ bv12 4))) (_ bv12 4) (select a404 (_ bv13 4))) (_ bv13 4) (select a404 (_ bv14 4)))) a404) a404) a527) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_29 (ite _let_28 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_3) deqeue_3)) (select a404 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_29 (ite _let_28 (ite _let_27 (_ 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_29 (ite _let_28 (ite _let_30 (_ 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_29 (ite _let_28 (ite _let_27 (ite _let_26 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 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_21 (ite _let_20 (ite _let_19 (ite _let_25 a282 (store a282 tail_fq_2 data_in_2)) a282) a282) a282) a405) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_21 (ite _let_20 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_2) deqeue_2)) (select a282 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_21 (ite _let_20 (ite _let_19 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_2 _let_23) (_ 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_21 (ite _let_20 (ite _let_22 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_2 (bvadd (_ bv1 4) _let_24)) (_ 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_21 (ite _let_20 (ite _let_19 (ite _let_25 tail_fq_2 _let_24) tail_fq_2) tail_fq_2) (_ bv0 4)) tail_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_21 (ite _let_20 (ite _let_22 (ite (= (_ bv1 1) empty_fq_2) head_fq_2 _let_23) head_fq_2) head_fq_2) (_ bv0 4)) head_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_21 (ite _let_20 (ite _let_19 (ite _let_18 a281 (store a281 tail_fs_2 data_in_2)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store a281 (_ bv0 4) (select a281 (_ bv1 4))) (_ bv1 4) (select a281 (_ bv2 4))) (_ bv2 4) (select a281 (_ bv3 4))) (_ bv3 4) (select a281 (_ bv4 4))) (_ bv4 4) (select a281 (_ bv5 4))) (_ bv5 4) (select a281 (_ bv6 4))) (_ bv6 4) (select a281 (_ bv7 4))) (_ bv7 4) (select a281 (_ bv8 4))) (_ bv8 4) (select a281 (_ bv9 4))) (_ bv9 4) (select a281 (_ bv10 4))) (_ bv10 4) (select a281 (_ bv11 4))) (_ bv11 4) (select a281 (_ bv12 4))) (_ bv12 4) (select a281 (_ bv13 4))) (_ bv13 4) (select a281 (_ bv14 4)))) a281) a281) a404) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_21 (ite _let_20 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_2) deqeue_2)) (select a281 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_21 (ite _let_20 (ite _let_19 (_ 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_21 (ite _let_20 (ite _let_22 (_ 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_21 (ite _let_20 (ite _let_19 (ite _let_18 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 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 a159 (store a159 tail_fq_1 data_in_1)) a159) a159) a159) a282) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_13 (ite _let_12 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_1) deqeue_1)) (select a159 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 a158 (store a158 tail_fs_1 data_in_1)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store a158 (_ bv0 4) (select a158 (_ bv1 4))) (_ bv1 4) (select a158 (_ bv2 4))) (_ bv2 4) (select a158 (_ bv3 4))) (_ bv3 4) (select a158 (_ bv4 4))) (_ bv4 4) (select a158 (_ bv5 4))) (_ bv5 4) (select a158 (_ bv6 4))) (_ bv6 4) (select a158 (_ bv7 4))) (_ bv7 4) (select a158 (_ bv8 4))) (_ bv8 4) (select a158 (_ bv9 4))) (_ bv9 4) (select a158 (_ bv10 4))) (_ bv10 4) (select a158 (_ bv11 4))) (_ bv11 4) (select a158 (_ bv12 4))) (_ bv12 4) (select a158 (_ bv13 4))) (_ bv13 4) (select a158 (_ bv14 4)))) a158) a158) a281) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_13 (ite _let_12 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_1) deqeue_1)) (select a158 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 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_5 (ite _let_4 (ite _let_3 (ite _let_9 a31 (store a31 tail_fq_0 data_in_0)) a31) a31) a31) a159) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_5 (ite _let_4 (ite (= (_ bv1 1) (bvand _let_1 deqeue_0)) (select a31 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_5 (ite _let_4 (ite _let_3 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_0 _let_7) (_ 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_5 (ite _let_4 (ite _let_6 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_0 (bvadd (_ bv1 4) _let_8)) (_ 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_5 (ite _let_4 (ite _let_3 (ite _let_9 tail_fq_0 _let_8) tail_fq_0) tail_fq_0) (_ bv0 4)) tail_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_5 (ite _let_4 (ite _let_6 (ite (= (_ bv1 1) empty_fq_0) head_fq_0 _let_7) head_fq_0) head_fq_0) (_ bv0 4)) head_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_5 (ite _let_4 (ite _let_3 (ite _let_2 a30 (store a30 tail_fs_0 data_in_0)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store a30 (_ bv0 4) (select a30 (_ bv1 4))) (_ bv1 4) (select a30 (_ bv2 4))) (_ bv2 4) (select a30 (_ bv3 4))) (_ bv3 4) (select a30 (_ bv4 4))) (_ bv4 4) (select a30 (_ bv5 4))) (_ bv5 4) (select a30 (_ bv6 4))) (_ bv6 4) (select a30 (_ bv7 4))) (_ bv7 4) (select a30 (_ bv8 4))) (_ bv8 4) (select a30 (_ bv9 4))) (_ bv9 4) (select a30 (_ bv10 4))) (_ bv10 4) (select a30 (_ bv11 4))) (_ bv11 4) (select a30 (_ bv12 4))) (_ bv12 4) (select a30 (_ bv13 4))) (_ bv13 4) (select a30 (_ bv14 4)))) a30) a30) a158) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite _let_5 (ite _let_4 (ite (= (_ bv1 1) (bvand _let_0 deqeue_0)) (select a30 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_5 (ite _let_4 (ite _let_3 (_ 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_5 (ite _let_4 (ite _let_6 (_ 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_5 (ite _let_4 (ite _let_3 (ite _let_2 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 (bvand (bvnot reset_0) (bvand (bvand _let_1 (bvand (bvnot full_fq_0) (bvand (bvand (bvand (bvand _let_0 (bvand (bvnot full_fs_0) (bvand (ite (= (_ bv0 4) head_fs_0) (_ bv1 1) (_ bv0 1)) (ite (= (_ bv0 4) tail_fs_0) (_ bv1 1) (_ bv0 1))))) (ite (= data_out_fs_0 (_ bv0 32)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 4) head_fq_0) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 4) tail_fq_0) (_ bv1 1) (_ bv0 1))))) (ite (= data_out_fq_0 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))) (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (_ bv0 1))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)