(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) (_ bv1 6)) (= ((_ extract 11 6) xs) (_ bv1 6)) (= ((_ extract 17 12) xs) (_ bv1 6)) (= ((_ extract 23 18) xs) (_ bv2 6)) (= ((_ extract 29 24) xs) (_ bv1 6)) (= ((_ extract 35 30) xs) (_ bv1 6)) (= ((_ extract 41 36) xs) (_ bv1 6)) (= ((_ extract 47 42) xs) (_ bv1 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 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 (Init p0)) (check-sat) (get-model) (assert (= dlock p1)) (check-sat) (get-model) (eval p0) (eval dlock) (get-info :all-statistics)