(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) (_ bv2 6)) (= ((_ extract 11 6) xs) (_ bv2 6)) (= ((_ extract 17 12) xs) (_ bv2 6)) (= ((_ extract 23 18) xs) (_ bv4 6)) (= ((_ extract 29 24) xs) (_ bv2 6)) (= ((_ extract 35 30) xs) (_ bv2 6)) (= ((_ extract 41 36) xs) (_ bv2 6)) (= ((_ extract 47 42) xs) (_ bv2 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)) ; ---------- 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))) ; --------------- 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))))) ; --------------- END (Loop free)------------------ (check-sat) (get-model) (eval mpath010) (assert (forall ((xs (_ BitVec 182)) )(= (Mid0 xs) (= xs (_ bv0 182))))) (declare-const dlock (_ BitVec 182)) (assert (= (bvand dlock (_ bv6129976317457006109821715293861905869342877865004236800 182)) (_ bv0 182))) (assert (= (bvand dlock (_ bv1405295396650831781587613638119892659365478399 182)) (_ bv0 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 (Mid0 p0)) (check-sat) (get-model) (assert (= dlock p1)) (check-sat) (get-model) (eval mpath00) (eval dlock) (get-info :all-statistics)