(set-logic QF_AUFBV) (declare-fun EDX_0 () (_ BitVec 32)) (declare-fun EBX_0 () (_ BitVec 32)) (define-sort MEM () (Array (_ BitVec 5) (_ BitVec 8))) (declare-fun MEM_ACTIVATION () MEM) (declare-fun MEM_OUTPUT_0 () MEM) (define-fun MEM_OUTPUT_1 () MEM (store MEM_OUTPUT_0 (_ bv0 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv0 5)) ((_ extract 7 0) EBX_0 )) ((_ extract 7 0) EDX_0 )))) (define-fun EDX_1 () (_ BitVec 32) ((_ rotate_left 1) EDX_0 )) (define-fun EBX_1 () (_ BitVec 32) ((_ rotate_left 1) EBX_0 )) (define-fun MEM_OUTPUT_2 () MEM (store MEM_OUTPUT_1 (_ bv1 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv1 5)) ((_ extract 7 0) EBX_1 )) ((_ extract 7 0) EDX_1 )))) (define-fun EDX_2 () (_ BitVec 32) ((_ rotate_left 1) EDX_1 )) (define-fun EBX_2 () (_ BitVec 32) ((_ rotate_left 1) EBX_1 )) (define-fun MEM_OUTPUT_3 () MEM (store MEM_OUTPUT_2 (_ bv2 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv2 5)) ((_ extract 7 0) EBX_2 )) ((_ extract 7 0) EDX_2 )))) (define-fun EDX_3 () (_ BitVec 32) ((_ rotate_left 1) EDX_2 )) (define-fun EBX_3 () (_ BitVec 32) ((_ rotate_left 1) EBX_2 )) (define-fun MEM_OUTPUT_4 () MEM (store MEM_OUTPUT_3 (_ bv3 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv3 5)) ((_ extract 7 0) EBX_3 )) ((_ extract 7 0) EDX_3 )))) (define-fun EDX_4 () (_ BitVec 32) ((_ rotate_left 1) EDX_3 )) (define-fun EBX_4 () (_ BitVec 32) ((_ rotate_left 1) EBX_3 )) (define-fun MEM_OUTPUT_5 () MEM (store MEM_OUTPUT_4 (_ bv4 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv4 5)) ((_ extract 7 0) EBX_4 )) ((_ extract 7 0) EDX_4 )))) (define-fun EDX_5 () (_ BitVec 32) ((_ rotate_left 1) EDX_4 )) (define-fun EBX_5 () (_ BitVec 32) ((_ rotate_left 1) EBX_4 )) (define-fun MEM_OUTPUT_6 () MEM (store MEM_OUTPUT_5 (_ bv5 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv5 5)) ((_ extract 7 0) EBX_5 )) ((_ extract 7 0) EDX_5 )))) (define-fun EDX_6 () (_ BitVec 32) ((_ rotate_left 1) EDX_5 )) (define-fun EBX_6 () (_ BitVec 32) ((_ rotate_left 1) EBX_5 )) (define-fun MEM_OUTPUT_7 () MEM (store MEM_OUTPUT_6 (_ bv6 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv6 5)) ((_ extract 7 0) EBX_6 )) ((_ extract 7 0) EDX_6 )))) (define-fun EDX_7 () (_ BitVec 32) ((_ rotate_left 1) EDX_6 )) (define-fun EBX_7 () (_ BitVec 32) ((_ rotate_left 1) EBX_6 )) (define-fun MEM_OUTPUT_8 () MEM (store MEM_OUTPUT_7 (_ bv7 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv7 5)) ((_ extract 7 0) EBX_7 )) ((_ extract 7 0) EDX_7 )))) (define-fun EDX_8 () (_ BitVec 32) ((_ rotate_left 1) EDX_7 )) (define-fun EBX_8 () (_ BitVec 32) ((_ rotate_left 1) EBX_7 )) (define-fun MEM_OUTPUT_9 () MEM (store MEM_OUTPUT_8 (_ bv8 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv8 5)) ((_ extract 7 0) EBX_8 )) ((_ extract 7 0) EDX_8 )))) (define-fun EDX_9 () (_ BitVec 32) ((_ rotate_left 1) EDX_8 )) (define-fun EBX_9 () (_ BitVec 32) ((_ rotate_left 1) EBX_8 )) (define-fun MEM_OUTPUT_10 () MEM (store MEM_OUTPUT_9 (_ bv9 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv9 5)) ((_ extract 7 0) EBX_9 )) ((_ extract 7 0) EDX_9 )))) (define-fun EDX_10 () (_ BitVec 32) ((_ rotate_left 1) EDX_9 )) (define-fun EBX_10 () (_ BitVec 32) ((_ rotate_left 1) EBX_9 )) (define-fun MEM_OUTPUT_11 () MEM (store MEM_OUTPUT_10 (_ bv10 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv10 5)) ((_ extract 7 0) EBX_10)) ((_ extract 7 0) EDX_10)))) (define-fun EDX_11 () (_ BitVec 32) ((_ rotate_left 1) EDX_10)) (define-fun EBX_11 () (_ BitVec 32) ((_ rotate_left 1) EBX_10)) (define-fun MEM_OUTPUT_12 () MEM (store MEM_OUTPUT_11 (_ bv11 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv11 5)) ((_ extract 7 0) EBX_11)) ((_ extract 7 0) EDX_11)))) (define-fun EDX_12 () (_ BitVec 32) ((_ rotate_left 1) EDX_11)) (define-fun EBX_12 () (_ BitVec 32) ((_ rotate_left 1) EBX_11)) (define-fun MEM_OUTPUT_13 () MEM (store MEM_OUTPUT_12 (_ bv12 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv12 5)) ((_ extract 7 0) EBX_12)) ((_ extract 7 0) EDX_12)))) (define-fun EDX_13 () (_ BitVec 32) ((_ rotate_left 1) EDX_12)) (define-fun EBX_13 () (_ BitVec 32) ((_ rotate_left 1) EBX_12)) (define-fun MEM_OUTPUT_14 () MEM (store MEM_OUTPUT_13 (_ bv13 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv13 5)) ((_ extract 7 0) EBX_13)) ((_ extract 7 0) EDX_13)))) (define-fun EDX_14 () (_ BitVec 32) ((_ rotate_left 1) EDX_13)) (define-fun EBX_14 () (_ BitVec 32) ((_ rotate_left 1) EBX_13)) (define-fun MEM_OUTPUT_15 () MEM (store MEM_OUTPUT_14 (_ bv14 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv14 5)) ((_ extract 7 0) EBX_14)) ((_ extract 7 0) EDX_14)))) (define-fun EDX_15 () (_ BitVec 32) ((_ rotate_left 1) EDX_14)) (define-fun EBX_15 () (_ BitVec 32) ((_ rotate_left 1) EBX_14)) (define-fun MEM_OUTPUT_16 () MEM (store MEM_OUTPUT_15 (_ bv15 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv15 5)) ((_ extract 7 0) EBX_15)) ((_ extract 7 0) EDX_15)))) (define-fun EDX_16 () (_ BitVec 32) ((_ rotate_left 1) EDX_15)) (define-fun EBX_16 () (_ BitVec 32) ((_ rotate_left 1) EBX_15)) (define-fun MEM_OUTPUT_17 () MEM (store MEM_OUTPUT_16 (_ bv16 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv16 5)) ((_ extract 7 0) EBX_16)) ((_ extract 7 0) EDX_16)))) (define-fun EDX_17 () (_ BitVec 32) ((_ rotate_left 1) EDX_16)) (define-fun EBX_17 () (_ BitVec 32) ((_ rotate_left 1) EBX_16)) (define-fun MEM_OUTPUT_18 () MEM (store MEM_OUTPUT_17 (_ bv17 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv17 5)) ((_ extract 7 0) EBX_17)) ((_ extract 7 0) EDX_17)))) (define-fun EDX_18 () (_ BitVec 32) ((_ rotate_left 1) EDX_17)) (define-fun EBX_18 () (_ BitVec 32) ((_ rotate_left 1) EBX_17)) (define-fun MEM_OUTPUT_19 () MEM (store MEM_OUTPUT_18 (_ bv18 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv18 5)) ((_ extract 7 0) EBX_18)) ((_ extract 7 0) EDX_18)))) (define-fun EDX_19 () (_ BitVec 32) ((_ rotate_left 1) EDX_18)) (define-fun EBX_19 () (_ BitVec 32) ((_ rotate_left 1) EBX_18)) (define-fun MEM_OUTPUT_20 () MEM (store MEM_OUTPUT_19 (_ bv19 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv19 5)) ((_ extract 7 0) EBX_19)) ((_ extract 7 0) EDX_19)))) (define-fun EDX_20 () (_ BitVec 32) ((_ rotate_left 1) EDX_19)) (define-fun EBX_20 () (_ BitVec 32) ((_ rotate_left 1) EBX_19)) (define-fun MEM_OUTPUT_21 () MEM (store MEM_OUTPUT_20 (_ bv20 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv20 5)) ((_ extract 7 0) EBX_20)) ((_ extract 7 0) EDX_20)))) (define-fun EDX_21 () (_ BitVec 32) ((_ rotate_left 1) EDX_20)) (define-fun EBX_21 () (_ BitVec 32) ((_ rotate_left 1) EBX_20)) (define-fun MEM_OUTPUT_22 () MEM (store MEM_OUTPUT_21 (_ bv21 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv21 5)) ((_ extract 7 0) EBX_21)) ((_ extract 7 0) EDX_21)))) (define-fun EDX_22 () (_ BitVec 32) ((_ rotate_left 1) EDX_21)) (define-fun EBX_22 () (_ BitVec 32) ((_ rotate_left 1) EBX_21)) (define-fun MEM_OUTPUT_23 () MEM (store MEM_OUTPUT_22 (_ bv22 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv22 5)) ((_ extract 7 0) EBX_22)) ((_ extract 7 0) EDX_22)))) (define-fun EDX_23 () (_ BitVec 32) ((_ rotate_left 1) EDX_22)) (define-fun EBX_23 () (_ BitVec 32) ((_ rotate_left 1) EBX_22)) (define-fun MEM_OUTPUT_24 () MEM (store MEM_OUTPUT_23 (_ bv23 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv23 5)) ((_ extract 7 0) EBX_23)) ((_ extract 7 0) EDX_23)))) (define-fun EDX_24 () (_ BitVec 32) ((_ rotate_left 1) EDX_23)) (define-fun EBX_24 () (_ BitVec 32) ((_ rotate_left 1) EBX_23)) (define-fun MEM_OUTPUT_25 () MEM (store MEM_OUTPUT_24 (_ bv24 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv24 5)) ((_ extract 7 0) EBX_24)) ((_ extract 7 0) EDX_24)))) (define-fun EDX_25 () (_ BitVec 32) ((_ rotate_left 1) EDX_24)) (define-fun EBX_25 () (_ BitVec 32) ((_ rotate_left 1) EBX_24)) (define-fun MEM_OUTPUT_26 () MEM (store MEM_OUTPUT_25 (_ bv25 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv25 5)) ((_ extract 7 0) EBX_25)) ((_ extract 7 0) EDX_25)))) (define-fun EDX_26 () (_ BitVec 32) ((_ rotate_left 1) EDX_25)) (define-fun EBX_26 () (_ BitVec 32) ((_ rotate_left 1) EBX_25)) (define-fun MEM_OUTPUT_27 () MEM (store MEM_OUTPUT_26 (_ bv26 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv26 5)) ((_ extract 7 0) EBX_26)) ((_ extract 7 0) EDX_26)))) (define-fun EDX_27 () (_ BitVec 32) ((_ rotate_left 1) EDX_26)) (define-fun EBX_27 () (_ BitVec 32) ((_ rotate_left 1) EBX_26)) (define-fun MEM_OUTPUT_28 () MEM (store MEM_OUTPUT_27 (_ bv27 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv27 5)) ((_ extract 7 0) EBX_27)) ((_ extract 7 0) EDX_27)))) (define-fun EDX_28 () (_ BitVec 32) ((_ rotate_left 1) EDX_27)) (define-fun EBX_28 () (_ BitVec 32) ((_ rotate_left 1) EBX_27)) (define-fun MEM_OUTPUT_29 () MEM (store MEM_OUTPUT_28 (_ bv28 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv28 5)) ((_ extract 7 0) EBX_28)) ((_ extract 7 0) EDX_28)))) (define-fun EDX_29 () (_ BitVec 32) ((_ rotate_left 1) EDX_28)) (define-fun EBX_29 () (_ BitVec 32) ((_ rotate_left 1) EBX_28)) (define-fun MEM_OUTPUT_30 () MEM (store MEM_OUTPUT_29 (_ bv29 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv29 5)) ((_ extract 7 0) EBX_29)) ((_ extract 7 0) EDX_29)))) (define-fun EDX_30 () (_ BitVec 32) ((_ rotate_left 1) EDX_29)) (define-fun EBX_30 () (_ BitVec 32) ((_ rotate_left 1) EBX_29)) (define-fun MEM_OUTPUT_31 () MEM (store MEM_OUTPUT_30 (_ bv30 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv30 5)) ((_ extract 7 0) EBX_30)) ((_ extract 7 0) EDX_30)))) (define-fun EDX_31 () (_ BitVec 32) ((_ rotate_left 1) EDX_30)) (define-fun EBX_31 () (_ BitVec 32) ((_ rotate_left 1) EBX_30)) (define-fun MEM_OUTPUT_32 () MEM (store MEM_OUTPUT_31 (_ bv31 5) (bvxor (bvsub (select MEM_ACTIVATION (_ bv31 5)) ((_ extract 7 0) EBX_31)) ((_ extract 7 0) EDX_31)))) (define-fun EDX_32 () (_ BitVec 32) ((_ rotate_left 1) EDX_31)) (define-fun EBX_32 () (_ BitVec 32) ((_ rotate_left 1) EBX_31)) (assert (= (select MEM_OUTPUT_32 (_ bv0 5)) (_ bv48 8))) (assert (= (select MEM_OUTPUT_32 (_ bv1 5)) (_ bv104 8))) (assert (= (select MEM_OUTPUT_32 (_ bv2 5)) (_ bv111 8))) (assert (= (select MEM_OUTPUT_32 (_ bv3 5)) (_ bv119 8))) (assert (= (select MEM_OUTPUT_32 (_ bv4 5)) (_ bv52 8))) (assert (= (select MEM_OUTPUT_32 (_ bv5 5)) (_ bv122 8))) (assert (= (select MEM_OUTPUT_32 (_ bv6 5)) (_ bv100 8))) (assert (= (select MEM_OUTPUT_32 (_ bv7 5)) (_ bv121 8))) (assert (= (select MEM_OUTPUT_32 (_ bv8 5)) (_ bv56 8))) (assert (= (select MEM_OUTPUT_32 (_ bv9 5)) (_ bv49 8))) (assert (= (select MEM_OUTPUT_32 (_ bv10 5)) (_ bv106 8))) (assert (= (select MEM_OUTPUT_32 (_ bv11 5)) (_ bv112 8))) (assert (= (select MEM_OUTPUT_32 (_ bv12 5)) (_ bv101 8))) (assert (= (select MEM_OUTPUT_32 (_ bv13 5)) (_ bv53 8))) (assert (= (select MEM_OUTPUT_32 (_ bv14 5)) (_ bv120 8))) (assert (= (select MEM_OUTPUT_32 (_ bv15 5)) (_ bv102 8))) (assert (= (select MEM_OUTPUT_32 (_ bv16 5)) (_ bv117 8))) (assert (= (select MEM_OUTPUT_32 (_ bv17 5)) (_ bv57 8))) (assert (= (select MEM_OUTPUT_32 (_ bv18 5)) (_ bv50 8))) (assert (= (select MEM_OUTPUT_32 (_ bv19 5)) (_ bv107 8))) (assert (= (select MEM_OUTPUT_32 (_ bv20 5)) (_ bv97 8))) (assert (= (select MEM_OUTPUT_32 (_ bv21 5)) (_ bv114 8))) (assert (= (select MEM_OUTPUT_32 (_ bv22 5)) (_ bv54 8))) (assert (= (select MEM_OUTPUT_32 (_ bv23 5)) (_ bv99 8))) (assert (= (select MEM_OUTPUT_32 (_ bv24 5)) (_ bv103 8))) (assert (= (select MEM_OUTPUT_32 (_ bv25 5)) (_ bv105 8))) (assert (= (select MEM_OUTPUT_32 (_ bv26 5)) (_ bv113 8))) (assert (= (select MEM_OUTPUT_32 (_ bv27 5)) (_ bv51 8))) (assert (= (select MEM_OUTPUT_32 (_ bv28 5)) (_ bv108 8))) (assert (= (select MEM_OUTPUT_32 (_ bv29 5)) (_ bv115 8))) (assert (= (select MEM_OUTPUT_32 (_ bv30 5)) (_ bv116 8))) (assert (= (select MEM_OUTPUT_32 (_ bv31 5)) (_ bv55 8))) (assert (= (select MEM_ACTIVATION (_ bv0 5)) (_ bv245 8))) (assert (= (select MEM_ACTIVATION (_ bv1 5)) (_ bv243 8))) (assert (= (select MEM_ACTIVATION (_ bv2 5)) (_ bv118 8))) (assert (= (select MEM_ACTIVATION (_ bv3 5)) (_ bv134 8))) (assert (= (select MEM_ACTIVATION (_ bv4 5)) (_ bv83 8))) (assert (= (select MEM_ACTIVATION (_ bv5 5)) (_ bv185 8))) (assert (= (select MEM_ACTIVATION (_ bv6 5)) (_ bv228 8))) (assert (= (select MEM_ACTIVATION (_ bv7 5)) (_ bv120 8))) (assert (= (select MEM_ACTIVATION (_ bv8 5)) (_ bv43 8))) (assert (= (select MEM_ACTIVATION (_ bv9 5)) (_ bv23 8))) (assert (= (select MEM_ACTIVATION (_ bv10 5)) (_ bv38 8))) (assert (= (select MEM_ACTIVATION (_ bv11 5)) (_ bv178 8))) (assert (= (select MEM_ACTIVATION (_ bv12 5)) (_ bv233 8))) (assert (= (select MEM_ACTIVATION (_ bv13 5)) (_ bv153 8))) (assert (= (select MEM_ACTIVATION (_ bv14 5)) (_ bv70 8))) (assert (= (select MEM_ACTIVATION (_ bv15 5)) (_ bv23 8))) (assert (= (select MEM_ACTIVATION (_ bv16 5)) (_ bv135 8))) (assert (= (select MEM_ACTIVATION (_ bv17 5)) (_ bv193 8))) (assert (= (select MEM_ACTIVATION (_ bv18 5)) (_ bv195 8))) (assert (= (select MEM_ACTIVATION (_ bv19 5)) (_ bv133 8))) (assert (= (select MEM_ACTIVATION (_ bv20 5)) (_ bv181 8))) (assert (= (select MEM_ACTIVATION (_ bv21 5)) (_ bv186 8))) (assert (= (select MEM_ACTIVATION (_ bv22 5)) (_ bv70 8))) (assert (= (select MEM_ACTIVATION (_ bv23 5)) (_ bv148 8))) (assert (= (select MEM_ACTIVATION (_ bv24 5)) (_ bv201 8))) (assert (= (select MEM_ACTIVATION (_ bv25 5)) (_ bv242 8))) (assert (= (select MEM_ACTIVATION (_ bv26 5)) (_ bv130 8))) (assert (= (select MEM_ACTIVATION (_ bv27 5)) (_ bv85 8))) (assert (= (select MEM_ACTIVATION (_ bv28 5)) (_ bv180 8))) (assert (= (select MEM_ACTIVATION (_ bv29 5)) (_ bv211 8))) (assert (= (select MEM_ACTIVATION (_ bv30 5)) (_ bv20 8))) (assert (= (select MEM_ACTIVATION (_ bv31 5)) (_ bv87 8))) (declare-fun REAL_EDX () (_ BitVec 32)) (declare-fun REAL_EBX () (_ BitVec 32)) (assert (= (bvxor EBX_0 EDX_0) REAL_EBX)) (check-sat) (get-model)