path: root/test/regress/regress3/decision-wchains010ue.smtv1.smt2

; COMMAND-LINE: --decision=justification
; EXPECT: unsat
(set-option :incremental false)
(set-info :source "This benchmark generates write chain permutations and tries to show
via extensionality that they are equal.

Contributed by Armin Biere (armin.biere@jku.at).")
(set-info :status unsat)
(set-info :category "crafted")
(set-info :difficulty "2")
(set-logic QF_AUFBV)
(declare-fun a1 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun v6 () (_ BitVec 32))
(declare-fun v7 () (_ BitVec 32))
(declare-fun v8 () (_ BitVec 32))
(declare-fun v9 () (_ BitVec 32))
(declare-fun v10 () (_ BitVec 32))
(declare-fun v11 () (_ BitVec 32))
(declare-fun v12 () (_ BitVec 32))
(declare-fun v13 () (_ BitVec 32))
(declare-fun v14 () (_ BitVec 32))
(declare-fun v15 () (_ BitVec 32))
(check-sat-assuming ( (let ((_let_0 (bvadd (_ bv0 32) v6))) (let ((_let_1 ((_ extract 7 0) v6))) (let ((_let_2 (bvadd (_ bv1 32) v6))) (let ((_let_3 ((_ extract 15 8) v6))) (let ((_let_4 (bvadd (_ bv2 32) v6))) (let ((_let_5 ((_ extract 23 16) v6))) (let ((_let_6 (bvadd (_ bv3 32) v6))) (let ((_let_7 ((_ extract 31 24) v6))) (let ((_let_8 (bvadd (_ bv0 32) v7))) (let ((_let_9 ((_ extract 7 0) v7))) (let ((_let_10 (bvadd (_ bv1 32) v7))) (let ((_let_11 ((_ extract 15 8) v7))) (let ((_let_12 (bvadd (_ bv2 32) v7))) (let ((_let_13 ((_ extract 23 16) v7))) (let ((_let_14 (bvadd (_ bv3 32) v7))) (let ((_let_15 ((_ extract 31 24) v7))) (let ((_let_16 (bvadd (_ bv0 32) v8))) (let ((_let_17 ((_ extract 7 0) v8))) (let ((_let_18 (bvadd (_ bv1 32) v8))) (let ((_let_19 ((_ extract 15 8) v8))) (let ((_let_20 (bvadd (_ bv2 32) v8))) (let ((_let_21 ((_ extract 23 16) v8))) (let ((_let_22 (bvadd (_ bv3 32) v8))) (let ((_let_23 ((_ extract 31 24) v8))) (let ((_let_24 (bvadd (_ bv0 32) v9))) (let ((_let_25 ((_ extract 7 0) v9))) (let ((_let_26 (bvadd (_ bv1 32) v9))) (let ((_let_27 ((_ extract 15 8) v9))) (let ((_let_28 (bvadd (_ bv2 32) v9))) (let ((_let_29 ((_ extract 23 16) v9))) (let ((_let_30 (bvadd (_ bv3 32) v9))) (let ((_let_31 ((_ extract 31 24) v9))) (let ((_let_32 (bvadd (_ bv0 32) v10))) (let ((_let_33 ((_ extract 7 0) v10))) (let ((_let_34 (bvadd (_ bv1 32) v10))) (let ((_let_35 ((_ extract 15 8) v10))) (let ((_let_36 (bvadd (_ bv2 32) v10))) (let ((_let_37 ((_ extract 23 16) v10))) (let ((_let_38 (bvadd (_ bv3 32) v10))) (let ((_let_39 ((_ extract 31 24) v10))) (let ((_let_40 (bvadd (_ bv0 32) v11))) (let ((_let_41 ((_ extract 7 0) v11))) (let ((_let_42 (bvadd (_ bv1 32) v11))) (let ((_let_43 ((_ extract 15 8) v11))) (let ((_let_44 (bvadd (_ bv2 32) v11))) (let ((_let_45 ((_ extract 23 16) v11))) (let ((_let_46 (bvadd (_ bv3 32) v11))) (let ((_let_47 ((_ extract 31 24) v11))) (let ((_let_48 (bvadd (_ bv0 32) v12))) (let ((_let_49 ((_ extract 7 0) v12))) (let ((_let_50 (bvadd (_ bv1 32) v12))) (let ((_let_51 ((_ extract 15 8) v12))) (let ((_let_52 (bvadd (_ bv2 32) v12))) (let ((_let_53 ((_ extract 23 16) v12))) (let ((_let_54 (bvadd (_ bv3 32) v12))) (let ((_let_55 ((_ extract 31 24) v12))) (let ((_let_56 (bvadd (_ bv0 32) v13))) (let ((_let_57 ((_ extract 7 0) v13))) (let ((_let_58 (bvadd (_ bv1 32) v13))) (let ((_let_59 ((_ extract 15 8) v13))) (let ((_let_60 (bvadd (_ bv2 32) v13))) (let ((_let_61 ((_ extract 23 16) v13))) (let ((_let_62 (bvadd (_ bv3 32) v13))) (let ((_let_63 ((_ extract 31 24) v13))) (let ((_let_64 (bvadd (_ bv0 32) v14))) (let ((_let_65 ((_ extract 7 0) v14))) (let ((_let_66 (bvadd (_ bv1 32) v14))) (let ((_let_67 ((_ extract 15 8) v14))) (let ((_let_68 (bvadd (_ bv2 32) v14))) (let ((_let_69 ((_ extract 23 16) v14))) (let ((_let_70 (bvadd (_ bv3 32) v14))) (let ((_let_71 ((_ extract 31 24) v14))) (let ((_let_72 (bvadd (_ bv0 32) v15))) (let ((_let_73 ((_ extract 7 0) v15))) (let ((_let_74 (bvadd (_ bv1 32) v15))) (let ((_let_75 ((_ extract 15 8) v15))) (let ((_let_76 (bvadd (_ bv2 32) v15))) (let ((_let_77 ((_ extract 23 16) v15))) (let ((_let_78 (bvadd (_ bv3 32) v15))) (let ((_let_79 ((_ extract 31 24) v15))) (not (= (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvnot (ite (= (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a1 _let_0 _let_1) _let_2 _let_3) _let_4 _let_5) _let_6 _let_7) _let_8 _let_9) _let_10 _let_11) _let_12 _let_13) _let_14 _let_15) _let_16 _let_17) _let_18 _let_19) _let_20 _let_21) _let_22 _let_23) _let_24 _let_25) _let_26 _let_27) _let_28 _let_29) _let_30 _let_31) _let_32 _let_33) _let_34 _let_35) _let_36 _let_37) _let_38 _let_39) _let_40 _let_41) _let_42 _let_43) _let_44 _let_45) _let_46 _let_47) _let_48 _let_49) _let_50 _let_51) _let_52 _let_53) _let_54 _let_55) _let_56 _let_57) _let_58 _let_59) _let_60 _let_61) _let_62 _let_63) _let_64 _let_65) _let_66 _let_67) _let_68 _let_69) _let_70 _let_71) _let_72 _let_73) _let_74 _let_75) _let_76 _let_77) _let_78 _let_79) (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a1 _let_72 _let_73) _let_74 _let_75) _let_76 _let_77) _let_78 _let_79) _let_64 _let_65) _let_66 _let_67) _let_68 _let_69) _let_70 _let_71) _let_56 _let_57) _let_58 _let_59) _let_60 _let_61) _let_62 _let_63) _let_48 _let_49) _let_50 _let_51) _let_52 _let_53) _let_54 _let_55) _let_40 _let_41) _let_42 _let_43) _let_44 _let_45) _let_46 _let_47) _let_32 _let_33) _let_34 _let_35) _let_36 _let_37) _let_38 _let_39) _let_24 _let_25) _let_26 _let_27) _let_28 _let_29) _let_30 _let_31) _let_16 _let_17) _let_18 _let_19) _let_20 _let_21) _let_22 _let_23) _let_8 _let_9) _let_10 _let_11) _let_12 _let_13) _let_14 _let_15) _let_0 _let_1) _let_2 _let_3) _let_4 _let_5) _let_6 _let_7)) (_ bv1 1) (_ bv0 1))) (ite (= ((_ extract 1 0) v6) (_ bv0 2)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v7)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v8)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v9)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v10)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v11)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v12)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v13)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v14)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v15)) (_ bv1 1) (_ bv0 1))) (_ bv0 1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))