(set-option :produce-models true) (set-option :pull-nested-quantifiers true) (set-option :mbqi true) (declare-const x (_ BitVec 182)) (declare-const y (_ BitVec 182)) (declare-const xs (_ BitVec 182)) (declare-fun T ((_ BitVec 182) (_ BitVec 182) ) bool) ; -------------- Transition Relation: ----------------- (assert (= (T x y) (and (and (or (and (and (= ((_ extract 53 48) y) (bvadd ((_ extract 53 48) x) (_ bv1 6))) (= ((_ extract 149 144) y) (bvadd ((_ extract 149 144) x) (_ bv1 6))) (= ((_ extract 35 30) y) (bvadd ((_ extract 35 30) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 47 42) y) (bvadd ((_ extract 47 42) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 23 18) y) ((_ extract 23 18) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 77 72) y) ((_ extract 77 72) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 162 162) x) (_ bv1 1))) (and (and (= ((_ extract 53 48) y) (bvadd ((_ extract 53 48) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 149 144) y) (bvadd ((_ extract 149 144) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 35 30) y) (bvadd ((_ extract 35 30) x) (_ bv1 6))) (= ((_ extract 47 42) y) (bvadd ((_ extract 47 42) x) (_ bv1 6))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 23 18) y) ((_ extract 23 18) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 77 72) y) ((_ extract 77 72) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 163 163) x) (_ bv1 1))) (and (and (= ((_ extract 59 54) y) (bvadd ((_ extract 59 54) x) (_ bv1 6))) (= ((_ extract 77 72) y) (bvadd ((_ extract 77 72) x) (_ bv1 6))) (= ((_ extract 53 48) y) (bvadd ((_ extract 53 48) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 23 18) y) (bvadd ((_ extract 23 18) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 164 164) x) (_ bv1 1))) (and (and (= ((_ extract 59 54) y) (bvadd ((_ extract 59 54) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 77 72) y) (bvadd ((_ extract 77 72) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 53 48) y) (bvadd ((_ extract 53 48) x) (_ bv1 6))) (= ((_ extract 23 18) y) (bvadd ((_ extract 23 18) x) (_ bv1 6))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 165 165) x) (_ bv1 1))) (and (and (= ((_ extract 65 60) y) (bvadd ((_ extract 65 60) x) (_ bv1 6))) (= ((_ extract 71 66) y) (bvadd ((_ extract 71 66) x) (_ bv1 6))) (= ((_ extract 59 54) y) (bvadd ((_ extract 59 54) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 23 18) y) (bvadd ((_ extract 23 18) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 77 72) y) ((_ extract 77 72) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 166 166) x) (_ bv1 1))) (and (and (= ((_ extract 83 78) y) (bvadd ((_ extract 83 78) x) (_ bv1 6))) (= ((_ extract 23 18) y) (bvadd ((_ extract 23 18) x) (_ bv1 6))) (= ((_ extract 5 0) y) (bvadd ((_ extract 5 0) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 77 72) y) (bvadd ((_ extract 77 72) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 167 167) x) (_ bv1 1))) (and (and (= ((_ extract 83 78) y) (bvadd ((_ extract 83 78) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 23 18) y) (bvadd ((_ extract 23 18) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 5 0) y) (bvadd ((_ extract 5 0) x) (_ bv1 6))) (= ((_ extract 77 72) y) (bvadd ((_ extract 77 72) x) (_ bv1 6))) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 168 168) x) (_ bv1 1))) (and (and (= ((_ extract 113 108) y) (bvadd ((_ extract 113 108) x) (_ bv1 6))) (= ((_ extract 23 18) y) (bvadd ((_ extract 23 18) x) (_ bv1 6))) (= ((_ extract 29 24) y) (bvadd ((_ extract 29 24) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 77 72) y) (bvadd ((_ extract 77 72) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 169 169) x) (_ bv1 1))) (and (and (= ((_ extract 113 108) y) (bvadd ((_ extract 113 108) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 23 18) y) (bvadd ((_ extract 23 18) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 29 24) y) (bvadd ((_ extract 29 24) x) (_ bv1 6))) (= ((_ extract 77 72) y) (bvadd ((_ extract 77 72) x) (_ bv1 6))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 170 170) x) (_ bv1 1))) (and (and (= ((_ extract 89 84) y) (bvadd ((_ extract 89 84) x) (_ bv1 6))) (= ((_ extract 107 102) y) (bvadd ((_ extract 107 102) x) (_ bv1 6))) (= ((_ extract 83 78) y) (bvadd ((_ extract 83 78) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 17 12) y) (bvadd ((_ extract 17 12) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 23 18) y) ((_ extract 23 18) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 77 72) y) ((_ extract 77 72) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 171 171) x) (_ bv1 1))) (and (and (= ((_ extract 89 84) y) (bvadd ((_ extract 89 84) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 107 102) y) (bvadd ((_ extract 107 102) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 83 78) y) (bvadd ((_ extract 83 78) x) (_ bv1 6))) (= ((_ extract 17 12) y) (bvadd ((_ extract 17 12) x) (_ bv1 6))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 23 18) y) ((_ extract 23 18) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 77 72) y) ((_ extract 77 72) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 172 172) x) (_ bv1 1))) (and (and (= ((_ extract 95 90) y) (bvadd ((_ extract 95 90) x) (_ bv1 6))) (= ((_ extract 101 96) y) (bvadd ((_ extract 101 96) x) (_ bv1 6))) (= ((_ extract 89 84) y) (bvadd ((_ extract 89 84) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 41 36) y) (bvadd ((_ extract 41 36) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 23 18) y) ((_ extract 23 18) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 77 72) y) ((_ extract 77 72) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 173 173) x) (_ bv1 1))) (and (and (= ((_ extract 119 114) y) (bvadd ((_ extract 119 114) x) (_ bv1 6))) (= ((_ extract 125 120) y) (bvadd ((_ extract 125 120) x) (_ bv1 6))) (= ((_ extract 113 108) y) (bvadd ((_ extract 113 108) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 41 36) y) (bvadd ((_ extract 41 36) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 23 18) y) ((_ extract 23 18) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 77 72) y) ((_ extract 77 72) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 174 174) x) (_ bv1 1))) (and (and (= ((_ extract 119 114) y) (bvadd ((_ extract 119 114) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 125 120) y) (bvadd ((_ extract 125 120) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 113 108) y) (bvadd ((_ extract 113 108) x) (_ bv1 6))) (= ((_ extract 41 36) y) (bvadd ((_ extract 41 36) x) (_ bv1 6))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 23 18) y) ((_ extract 23 18) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 77 72) y) ((_ extract 77 72) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 175 175) x) (_ bv1 1))) (and (and (= ((_ extract 131 126) y) (bvadd ((_ extract 131 126) x) (_ bv1 6))) (= ((_ extract 41 36) y) (bvadd ((_ extract 41 36) x) (_ bv1 6))) (= ((_ extract 11 6) y) (bvadd ((_ extract 11 6) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 125 120) y) (bvadd ((_ extract 125 120) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 23 18) y) ((_ extract 23 18) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 77 72) y) ((_ extract 77 72) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 176 176) x) (_ bv1 1))) (and (and (= ((_ extract 131 126) y) (bvadd ((_ extract 131 126) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 41 36) y) (bvadd ((_ extract 41 36) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 11 6) y) (bvadd ((_ extract 11 6) x) (_ bv1 6))) (= ((_ extract 125 120) y) (bvadd ((_ extract 125 120) x) (_ bv1 6))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 23 18) y) ((_ extract 23 18) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 77 72) y) ((_ extract 77 72) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 177 177) x) (_ bv1 1))) (and (and (= ((_ extract 137 132) y) (bvadd ((_ extract 137 132) x) (_ bv1 6))) (= ((_ extract 77 72) y) (bvadd ((_ extract 77 72) x) (_ bv1 6))) (= ((_ extract 131 126) y) (bvadd ((_ extract 131 126) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 23 18) y) (bvadd ((_ extract 23 18) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 178 178) x) (_ bv1 1))) (and (and (= ((_ extract 137 132) y) (bvadd ((_ extract 137 132) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 77 72) y) (bvadd ((_ extract 77 72) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 131 126) y) (bvadd ((_ extract 131 126) x) (_ bv1 6))) (= ((_ extract 23 18) y) (bvadd ((_ extract 23 18) x) (_ bv1 6))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 179 179) x) (_ bv1 1))) (and (and (= ((_ extract 143 138) y) (bvadd ((_ extract 143 138) x) (_ bv1 6))) (= ((_ extract 71 66) y) (bvadd ((_ extract 71 66) x) (_ bv1 6))) (= ((_ extract 137 132) y) (bvadd ((_ extract 137 132) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 23 18) y) (bvadd ((_ extract 23 18) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 77 72) y) ((_ extract 77 72) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 119 114) y) ((_ extract 119 114) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 149 144) y) ((_ extract 149 144) x)) (= ((_ extract 155 150) y) ((_ extract 155 150) x)) (= ((_ extract 161 156) y) ((_ extract 161 156) x))) (= ((_ extract 180 180) x) (_ bv1 1))) (and (and (= ((_ extract 155 150) y) (bvadd ((_ extract 155 150) x) (_ bv1 6))) (= ((_ extract 161 156) y) (bvadd ((_ extract 161 156) x) (_ bv1 6))) (= ((_ extract 119 114) y) (bvadd ((_ extract 119 114) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 149 144) y) (bvadd ((_ extract 149 144) x) (bvmul (_ bv63 6) (_ bv1 6)))) (= ((_ extract 5 0) y) ((_ extract 5 0) x)) (= ((_ extract 11 6) y) ((_ extract 11 6) x)) (= ((_ extract 17 12) y) ((_ extract 17 12) x)) (= ((_ extract 23 18) y) ((_ extract 23 18) x)) (= ((_ extract 29 24) y) ((_ extract 29 24) x)) (= ((_ extract 35 30) y) ((_ extract 35 30) x)) (= ((_ extract 41 36) y) ((_ extract 41 36) x)) (= ((_ extract 47 42) y) ((_ extract 47 42) x)) (= ((_ extract 53 48) y) ((_ extract 53 48) x)) (= ((_ extract 59 54) y) ((_ extract 59 54) x)) (= ((_ extract 65 60) y) ((_ extract 65 60) x)) (= ((_ extract 71 66) y) ((_ extract 71 66) x)) (= ((_ extract 77 72) y) ((_ extract 77 72) x)) (= ((_ extract 83 78) y) ((_ extract 83 78) x)) (= ((_ extract 89 84) y) ((_ extract 89 84) x)) (= ((_ extract 95 90) y) ((_ extract 95 90) x)) (= ((_ extract 101 96) y) ((_ extract 101 96) x)) (= ((_ extract 107 102) y) ((_ extract 107 102) x)) (= ((_ extract 113 108) y) ((_ extract 113 108) x)) (= ((_ extract 125 120) y) ((_ extract 125 120) x)) (= ((_ extract 131 126) y) ((_ extract 131 126) x)) (= ((_ extract 137 132) y) ((_ extract 137 132) x)) (= ((_ extract 143 138) y) ((_ extract 143 138) x))) (= ((_ extract 181 181) x) (_ bv1 1)))) (and (= (= ((_ extract 162 162) y) (_ bv1 1)) (and (bvuge ((_ extract 35 30) y) (_ bv1 6)) (bvuge ((_ extract 47 42) y) (_ bv1 6)))) (= (= ((_ extract 163 163) y) (_ bv1 1)) (and (bvuge ((_ extract 53 48) y) (_ bv1 6)) (bvuge ((_ extract 149 144) y) (_ bv1 6)))) (= (= ((_ extract 164 164) y) (_ bv1 1)) (and (bvuge ((_ extract 53 48) y) (_ bv1 6)) (bvuge ((_ extract 23 18) y) (_ bv1 6)))) (= (= ((_ extract 165 165) y) (_ bv1 1)) (and (bvuge ((_ extract 59 54) y) (_ bv1 6)) (bvuge ((_ extract 77 72) y) (_ bv1 6)))) (= (= ((_ extract 166 166) y) (_ bv1 1)) (and (bvuge ((_ extract 59 54) y) (_ bv1 6)) (bvuge ((_ extract 23 18) y) (_ bv1 6)))) (= (= ((_ extract 167 167) y) (_ bv1 1)) (and (bvuge ((_ extract 5 0) y) (_ bv1 6)) (bvuge ((_ extract 77 72) y) (_ bv1 6)))) (= (= ((_ extract 168 168) y) (_ bv1 1)) (and (bvuge ((_ extract 83 78) y) (_ bv1 6)) (bvuge ((_ extract 23 18) y) (_ bv1 6)))) (= (= ((_ extract 169 169) y) (_ bv1 1)) (and (bvuge ((_ extract 29 24) y) (_ bv1 6)) (bvuge ((_ extract 77 72) y) (_ bv1 6)))) (= (= ((_ extract 170 170) y) (_ bv1 1)) (and (bvuge ((_ extract 113 108) y) (_ bv1 6)) (bvuge ((_ extract 23 18) y) (_ bv1 6)))) (= (= ((_ extract 171 171) y) (_ bv1 1)) (and (bvuge ((_ extract 83 78) y) (_ bv1 6)) (bvuge ((_ extract 17 12) y) (_ bv1 6)))) (= (= ((_ extract 172 172) y) (_ bv1 1)) (and (bvuge ((_ extract 89 84) y) (_ bv1 6)) (bvuge ((_ extract 107 102) y) (_ bv1 6)))) (= (= ((_ extract 173 173) y) (_ bv1 1)) (and (bvuge ((_ extract 89 84) y) (_ bv1 6)) (bvuge ((_ extract 41 36) y) (_ bv1 6)))) (= (= ((_ extract 174 174) y) (_ bv1 1)) (and (bvuge ((_ extract 113 108) y) (_ bv1 6)) (bvuge ((_ extract 41 36) y) (_ bv1 6)))) (= (= ((_ extract 175 175) y) (_ bv1 1)) (and (bvuge ((_ extract 119 114) y) (_ bv1 6)) (bvuge ((_ extract 125 120) y) (_ bv1 6)))) (= (= ((_ extract 176 176) y) (_ bv1 1)) (and (bvuge ((_ extract 11 6) y) (_ bv1 6)) (bvuge ((_ extract 125 120) y) (_ bv1 6)))) (= (= ((_ extract 177 177) y) (_ bv1 1)) (and (bvuge ((_ extract 131 126) y) (_ bv1 6)) (bvuge ((_ extract 41 36) y) (_ bv1 6)))) (= (= ((_ extract 178 178) y) (_ bv1 1)) (and (bvuge ((_ extract 131 126) y) (_ bv1 6)) (bvuge ((_ extract 23 18) y) (_ bv1 6)))) (= (= ((_ extract 179 179) y) (_ bv1 1)) (and (bvuge ((_ extract 137 132) y) (_ bv1 6)) (bvuge ((_ extract 77 72) y) (_ bv1 6)))) (= (= ((_ extract 180 180) y) (_ bv1 1)) (and (bvuge ((_ extract 137 132) y) (_ bv1 6)) (bvuge ((_ extract 23 18) y) (_ bv1 6)))) (= (= ((_ extract 181 181) y) (_ bv1 1)) (and (bvuge ((_ extract 119 114) y) (_ bv1 6)) (bvuge ((_ extract 149 144) y) (_ bv1 6))))))))) ; ------------------ END ------------------------------ (declare-fun Init ((_ BitVec 182) ) bool) (assert (forall ((xs (_ BitVec 182)) )(= (Init xs) (and (= ((_ extract 5 0) xs) (_ bv3 6)) (= ((_ extract 11 6) xs) (_ bv3 6)) (= ((_ extract 17 12) xs) (_ bv3 6)) (= ((_ extract 23 18) xs) (_ bv6 6)) (= ((_ extract 29 24) xs) (_ bv3 6)) (= ((_ extract 35 30) xs) (_ bv3 6)) (= ((_ extract 41 36) xs) (_ bv3 6)) (= ((_ extract 47 42) xs) (_ bv3 6)) (= ((_ extract 53 48) xs) (_ bv0 6)) (= ((_ extract 59 54) xs) (_ bv0 6)) (= ((_ extract 65 60) xs) (_ bv0 6)) (= ((_ extract 71 66) xs) (_ bv0 6)) (= ((_ extract 77 72) xs) (_ bv0 6)) (= ((_ extract 83 78) xs) (_ bv0 6)) (= ((_ extract 89 84) xs) (_ bv0 6)) (= ((_ extract 95 90) xs) (_ bv0 6)) (= ((_ extract 101 96) xs) (_ bv0 6)) (= ((_ extract 107 102) xs) (_ bv0 6)) (= ((_ extract 113 108) xs) (_ bv0 6)) (= ((_ extract 119 114) xs) (_ bv0 6)) (= ((_ extract 125 120) xs) (_ bv0 6)) (= ((_ extract 131 126) xs) (_ bv0 6)) (= ((_ extract 137 132) xs) (_ bv0 6)) (= ((_ extract 143 138) xs) (_ bv0 6)) (= ((_ extract 149 144) xs) (_ bv0 6)) (= ((_ extract 155 150) xs) (_ bv0 6)) (= ((_ extract 161 156) xs) (_ bv0 6)) (= ((_ extract 162 162) xs) (_ bv1 1)) (not (= ((_ extract 163 163) xs) (_ bv1 1))) (not (= ((_ extract 164 164) xs) (_ bv1 1))) (not (= ((_ extract 165 165) xs) (_ bv1 1))) (not (= ((_ extract 166 166) xs) (_ bv1 1))) (not (= ((_ extract 167 167) xs) (_ bv1 1))) (not (= ((_ extract 168 168) xs) (_ bv1 1))) (not (= ((_ extract 169 169) xs) (_ bv1 1))) (not (= ((_ extract 170 170) xs) (_ bv1 1))) (not (= ((_ extract 171 171) xs) (_ bv1 1))) (not (= ((_ extract 172 172) xs) (_ bv1 1))) (not (= ((_ extract 173 173) xs) (_ bv1 1))) (not (= ((_ extract 174 174) xs) (_ bv1 1))) (not (= ((_ extract 175 175) xs) (_ bv1 1))) (not (= ((_ extract 176 176) xs) (_ bv1 1))) (not (= ((_ extract 177 177) xs) (_ bv1 1))) (not (= ((_ extract 178 178) xs) (_ bv1 1))) (not (= ((_ extract 179 179) xs) (_ bv1 1))) (not (= ((_ extract 180 180) xs) (_ bv1 1))) (not (= ((_ extract 181 181) xs) (_ bv1 1))))))) (declare-const mpath00 (_ BitVec 182)) (declare-const mpath01 (_ BitVec 182)) (declare-const mpath02 (_ BitVec 182)) (declare-const mpath03 (_ BitVec 182)) (declare-const mpath04 (_ BitVec 182)) (declare-const mpath05 (_ BitVec 182)) (declare-const mpath06 (_ BitVec 182)) (declare-const mpath07 (_ BitVec 182)) (declare-const mpath08 (_ BitVec 182)) (declare-const mpath09 (_ BitVec 182)) (declare-const mpath010 (_ BitVec 182)) (declare-const mpath011 (_ BitVec 182)) (declare-const mpath012 (_ BitVec 182)) (declare-const mpath013 (_ BitVec 182)) (declare-const mpath014 (_ BitVec 182)) (declare-const mpath015 (_ BitVec 182)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T mpath00 mpath01) (T mpath01 mpath02) (T mpath02 mpath03) (T mpath03 mpath04) (T mpath04 mpath05) (T mpath05 mpath06) (T mpath06 mpath07) (T mpath07 mpath08) (T mpath08 mpath09) (T mpath09 mpath010) (T mpath010 mpath011) (T mpath011 mpath012) (T mpath012 mpath013) (T mpath013 mpath014) (T mpath014 mpath015))) ; --------------- END (Path)------------------ (assert (Init mpath00)) (declare-fun Mid0 ((_ BitVec 182) ) bool) ; ---------- Loop Free: --------------- (assert (and (and (not (= mpath01 mpath00))) (and (not (= mpath02 mpath00)) (not (= mpath02 mpath01))) (and (not (= mpath03 mpath00)) (not (= mpath03 mpath01)) (not (= mpath03 mpath02))) (and (not (= mpath04 mpath00)) (not (= mpath04 mpath01)) (not (= mpath04 mpath02)) (not (= mpath04 mpath03))) (and (not (= mpath05 mpath00)) (not (= mpath05 mpath01)) (not (= mpath05 mpath02)) (not (= mpath05 mpath03)) (not (= mpath05 mpath04))) (and (not (= mpath06 mpath00)) (not (= mpath06 mpath01)) (not (= mpath06 mpath02)) (not (= mpath06 mpath03)) (not (= mpath06 mpath04)) (not (= mpath06 mpath05))) (and (not (= mpath07 mpath00)) (not (= mpath07 mpath01)) (not (= mpath07 mpath02)) (not (= mpath07 mpath03)) (not (= mpath07 mpath04)) (not (= mpath07 mpath05)) (not (= mpath07 mpath06))) (and (not (= mpath08 mpath00)) (not (= mpath08 mpath01)) (not (= mpath08 mpath02)) (not (= mpath08 mpath03)) (not (= mpath08 mpath04)) (not (= mpath08 mpath05)) (not (= mpath08 mpath06)) (not (= mpath08 mpath07))) (and (not (= mpath09 mpath00)) (not (= mpath09 mpath01)) (not (= mpath09 mpath02)) (not (= mpath09 mpath03)) (not (= mpath09 mpath04)) (not (= mpath09 mpath05)) (not (= mpath09 mpath06)) (not (= mpath09 mpath07)) (not (= mpath09 mpath08))) (and (not (= mpath010 mpath00)) (not (= mpath010 mpath01)) (not (= mpath010 mpath02)) (not (= mpath010 mpath03)) (not (= mpath010 mpath04)) (not (= mpath010 mpath05)) (not (= mpath010 mpath06)) (not (= mpath010 mpath07)) (not (= mpath010 mpath08)) (not (= mpath010 mpath09))) (and (not (= mpath011 mpath00)) (not (= mpath011 mpath01)) (not (= mpath011 mpath02)) (not (= mpath011 mpath03)) (not (= mpath011 mpath04)) (not (= mpath011 mpath05)) (not (= mpath011 mpath06)) (not (= mpath011 mpath07)) (not (= mpath011 mpath08)) (not (= mpath011 mpath09)) (not (= mpath011 mpath010))) (and (not (= mpath012 mpath00)) (not (= mpath012 mpath01)) (not (= mpath012 mpath02)) (not (= mpath012 mpath03)) (not (= mpath012 mpath04)) (not (= mpath012 mpath05)) (not (= mpath012 mpath06)) (not (= mpath012 mpath07)) (not (= mpath012 mpath08)) (not (= mpath012 mpath09)) (not (= mpath012 mpath010)) (not (= mpath012 mpath011))) (and (not (= mpath013 mpath00)) (not (= mpath013 mpath01)) (not (= mpath013 mpath02)) (not (= mpath013 mpath03)) (not (= mpath013 mpath04)) (not (= mpath013 mpath05)) (not (= mpath013 mpath06)) (not (= mpath013 mpath07)) (not (= mpath013 mpath08)) (not (= mpath013 mpath09)) (not (= mpath013 mpath010)) (not (= mpath013 mpath011)) (not (= mpath013 mpath012))) (and (not (= mpath014 mpath00)) (not (= mpath014 mpath01)) (not (= mpath014 mpath02)) (not (= mpath014 mpath03)) (not (= mpath014 mpath04)) (not (= mpath014 mpath05)) (not (= mpath014 mpath06)) (not (= mpath014 mpath07)) (not (= mpath014 mpath08)) (not (= mpath014 mpath09)) (not (= mpath014 mpath010)) (not (= mpath014 mpath011)) (not (= mpath014 mpath012)) (not (= mpath014 mpath013))) (and (not (= mpath015 mpath00)) (not (= mpath015 mpath01)) (not (= mpath015 mpath02)) (not (= mpath015 mpath03)) (not (= mpath015 mpath04)) (not (= mpath015 mpath05)) (not (= mpath015 mpath06)) (not (= mpath015 mpath07)) (not (= mpath015 mpath08)) (not (= mpath015 mpath09)) (not (= mpath015 mpath010)) (not (= mpath015 mpath011)) (not (= mpath015 mpath012)) (not (= mpath015 mpath013)) (not (= mpath015 mpath014))))) ; --------------- END (Loop free)------------------ (check-sat) (get-model) (eval mpath015) (assert (forall ((xs (_ BitVec 182)) )(= (Mid0 xs) (= xs (_ bv0 182))))) (declare-const mpath10 (_ BitVec 182)) (declare-const mpath11 (_ BitVec 182)) (declare-const mpath12 (_ BitVec 182)) (declare-const mpath13 (_ BitVec 182)) (declare-const mpath14 (_ BitVec 182)) (declare-const mpath15 (_ BitVec 182)) (declare-const mpath16 (_ BitVec 182)) (declare-const mpath17 (_ BitVec 182)) (declare-const mpath18 (_ BitVec 182)) (declare-const mpath19 (_ BitVec 182)) (declare-const mpath110 (_ BitVec 182)) (declare-const mpath111 (_ BitVec 182)) (declare-const mpath112 (_ BitVec 182)) (declare-const mpath113 (_ BitVec 182)) (declare-const mpath114 (_ BitVec 182)) (declare-const mpath115 (_ BitVec 182)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T mpath10 mpath11) (T mpath11 mpath12) (T mpath12 mpath13) (T mpath13 mpath14) (T mpath14 mpath15) (T mpath15 mpath16) (T mpath16 mpath17) (T mpath17 mpath18) (T mpath18 mpath19) (T mpath19 mpath110) (T mpath110 mpath111) (T mpath111 mpath112) (T mpath112 mpath113) (T mpath113 mpath114) (T mpath114 mpath115))) ; --------------- END (Path)------------------ (assert (Mid0 mpath10)) (declare-fun Mid1 ((_ BitVec 182) ) bool) ; ---------- Loop Free: --------------- (assert (and (and (not (= mpath11 mpath10))) (and (not (= mpath12 mpath10)) (not (= mpath12 mpath11))) (and (not (= mpath13 mpath10)) (not (= mpath13 mpath11)) (not (= mpath13 mpath12))) (and (not (= mpath14 mpath10)) (not (= mpath14 mpath11)) (not (= mpath14 mpath12)) (not (= mpath14 mpath13))) (and (not (= mpath15 mpath10)) (not (= mpath15 mpath11)) (not (= mpath15 mpath12)) (not (= mpath15 mpath13)) (not (= mpath15 mpath14))) (and (not (= mpath16 mpath10)) (not (= mpath16 mpath11)) (not (= mpath16 mpath12)) (not (= mpath16 mpath13)) (not (= mpath16 mpath14)) (not (= mpath16 mpath15))) (and (not (= mpath17 mpath10)) (not (= mpath17 mpath11)) (not (= mpath17 mpath12)) (not (= mpath17 mpath13)) (not (= mpath17 mpath14)) (not (= mpath17 mpath15)) (not (= mpath17 mpath16))) (and (not (= mpath18 mpath10)) (not (= mpath18 mpath11)) (not (= mpath18 mpath12)) (not (= mpath18 mpath13)) (not (= mpath18 mpath14)) (not (= mpath18 mpath15)) (not (= mpath18 mpath16)) (not (= mpath18 mpath17))) (and (not (= mpath19 mpath10)) (not (= mpath19 mpath11)) (not (= mpath19 mpath12)) (not (= mpath19 mpath13)) (not (= mpath19 mpath14)) (not (= mpath19 mpath15)) (not (= mpath19 mpath16)) (not (= mpath19 mpath17)) (not (= mpath19 mpath18))) (and (not (= mpath110 mpath10)) (not (= mpath110 mpath11)) (not (= mpath110 mpath12)) (not (= mpath110 mpath13)) (not (= mpath110 mpath14)) (not (= mpath110 mpath15)) (not (= mpath110 mpath16)) (not (= mpath110 mpath17)) (not (= mpath110 mpath18)) (not (= mpath110 mpath19))) (and (not (= mpath111 mpath10)) (not (= mpath111 mpath11)) (not (= mpath111 mpath12)) (not (= mpath111 mpath13)) (not (= mpath111 mpath14)) (not (= mpath111 mpath15)) (not (= mpath111 mpath16)) (not (= mpath111 mpath17)) (not (= mpath111 mpath18)) (not (= mpath111 mpath19)) (not (= mpath111 mpath110))) (and (not (= mpath112 mpath10)) (not (= mpath112 mpath11)) (not (= mpath112 mpath12)) (not (= mpath112 mpath13)) (not (= mpath112 mpath14)) (not (= mpath112 mpath15)) (not (= mpath112 mpath16)) (not (= mpath112 mpath17)) (not (= mpath112 mpath18)) (not (= mpath112 mpath19)) (not (= mpath112 mpath110)) (not (= mpath112 mpath111))) (and (not (= mpath113 mpath10)) (not (= mpath113 mpath11)) (not (= mpath113 mpath12)) (not (= mpath113 mpath13)) (not (= mpath113 mpath14)) (not (= mpath113 mpath15)) (not (= mpath113 mpath16)) (not (= mpath113 mpath17)) (not (= mpath113 mpath18)) (not (= mpath113 mpath19)) (not (= mpath113 mpath110)) (not (= mpath113 mpath111)) (not (= mpath113 mpath112))) (and (not (= mpath114 mpath10)) (not (= mpath114 mpath11)) (not (= mpath114 mpath12)) (not (= mpath114 mpath13)) (not (= mpath114 mpath14)) (not (= mpath114 mpath15)) (not (= mpath114 mpath16)) (not (= mpath114 mpath17)) (not (= mpath114 mpath18)) (not (= mpath114 mpath19)) (not (= mpath114 mpath110)) (not (= mpath114 mpath111)) (not (= mpath114 mpath112)) (not (= mpath114 mpath113))) (and (not (= mpath115 mpath10)) (not (= mpath115 mpath11)) (not (= mpath115 mpath12)) (not (= mpath115 mpath13)) (not (= mpath115 mpath14)) (not (= mpath115 mpath15)) (not (= mpath115 mpath16)) (not (= mpath115 mpath17)) (not (= mpath115 mpath18)) (not (= mpath115 mpath19)) (not (= mpath115 mpath110)) (not (= mpath115 mpath111)) (not (= mpath115 mpath112)) (not (= mpath115 mpath113)) (not (= mpath115 mpath114))))) ; --------------- END (Loop free)------------------ (check-sat) (get-model) (eval mpath115) (assert (forall ((xs (_ BitVec 182)) )(= (Mid1 xs) (= xs (_ bv4214362737381194360485454324663350254951532586004905984 182))))) (declare-const dlock (_ BitVec 182)) (assert (= (bvand dlock (_ bv6129976317457006109821715293861905869342877865004236800 182)) (_ bv0 182))) (assert (bvugt (bvand dlock (_ bv1405295396650831781587613638119892659365478399 182)) (_ bv1 182))) (push) (declare-const p0 (_ BitVec 182)) (declare-const p1 (_ BitVec 182)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p0 p1))) ; --------------- END (Path)------------------ ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))))) ; --------------- END (Loop free)------------------ (assert (Mid1 p0)) (check-sat) (get-model) (assert (= dlock p1)) (check-sat) (get-model) (eval mpath00) (eval dlock) (get-info :all-statistics)