(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) (_ bv5 6)) (= ((_ extract 11 6) xs) (_ bv5 6)) (= ((_ extract 17 12) xs) (_ bv5 6)) (= ((_ extract 23 18) xs) (_ bv10 6)) (= ((_ extract 29 24) xs) (_ bv5 6)) (= ((_ extract 35 30) xs) (_ bv5 6)) (= ((_ extract 41 36) xs) (_ bv5 6)) (= ((_ extract 47 42) xs) (_ bv5 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)) (declare-const mpath016 (_ BitVec 182)) (declare-const mpath017 (_ 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) (T mpath015 mpath016) (T mpath016 mpath017))) ; --------------- 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))) (and (not (= mpath016 mpath00)) (not (= mpath016 mpath01)) (not (= mpath016 mpath02)) (not (= mpath016 mpath03)) (not (= mpath016 mpath04)) (not (= mpath016 mpath05)) (not (= mpath016 mpath06)) (not (= mpath016 mpath07)) (not (= mpath016 mpath08)) (not (= mpath016 mpath09)) (not (= mpath016 mpath010)) (not (= mpath016 mpath011)) (not (= mpath016 mpath012)) (not (= mpath016 mpath013)) (not (= mpath016 mpath014)) (not (= mpath016 mpath015))) (and (not (= mpath017 mpath00)) (not (= mpath017 mpath01)) (not (= mpath017 mpath02)) (not (= mpath017 mpath03)) (not (= mpath017 mpath04)) (not (= mpath017 mpath05)) (not (= mpath017 mpath06)) (not (= mpath017 mpath07)) (not (= mpath017 mpath08)) (not (= mpath017 mpath09)) (not (= mpath017 mpath010)) (not (= mpath017 mpath011)) (not (= mpath017 mpath012)) (not (= mpath017 mpath013)) (not (= mpath017 mpath014)) (not (= mpath017 mpath015)) (not (= mpath017 mpath016))))) ; --------------- END (Loop free)------------------ (check-sat) (get-model) (eval mpath017) (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)) (declare-const mpath116 (_ BitVec 182)) (declare-const mpath117 (_ 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) (T mpath115 mpath116) (T mpath116 mpath117))) ; --------------- 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))) (and (not (= mpath116 mpath10)) (not (= mpath116 mpath11)) (not (= mpath116 mpath12)) (not (= mpath116 mpath13)) (not (= mpath116 mpath14)) (not (= mpath116 mpath15)) (not (= mpath116 mpath16)) (not (= mpath116 mpath17)) (not (= mpath116 mpath18)) (not (= mpath116 mpath19)) (not (= mpath116 mpath110)) (not (= mpath116 mpath111)) (not (= mpath116 mpath112)) (not (= mpath116 mpath113)) (not (= mpath116 mpath114)) (not (= mpath116 mpath115))) (and (not (= mpath117 mpath10)) (not (= mpath117 mpath11)) (not (= mpath117 mpath12)) (not (= mpath117 mpath13)) (not (= mpath117 mpath14)) (not (= mpath117 mpath15)) (not (= mpath117 mpath16)) (not (= mpath117 mpath17)) (not (= mpath117 mpath18)) (not (= mpath117 mpath19)) (not (= mpath117 mpath110)) (not (= mpath117 mpath111)) (not (= mpath117 mpath112)) (not (= mpath117 mpath113)) (not (= mpath117 mpath114)) (not (= mpath117 mpath115)) (not (= mpath117 mpath116))))) ; --------------- END (Loop free)------------------ (check-sat) (get-model) (eval mpath117) (assert (forall ((xs (_ BitVec 182)) )(= (Mid1 xs) (= xs (_ bv478904856520590268236983445984471619880855975682375680 182))))) (declare-const mpath20 (_ BitVec 182)) (declare-const mpath21 (_ BitVec 182)) (declare-const mpath22 (_ BitVec 182)) (declare-const mpath23 (_ BitVec 182)) (declare-const mpath24 (_ BitVec 182)) (declare-const mpath25 (_ BitVec 182)) (declare-const mpath26 (_ BitVec 182)) (declare-const mpath27 (_ BitVec 182)) (declare-const mpath28 (_ BitVec 182)) (declare-const mpath29 (_ BitVec 182)) (declare-const mpath210 (_ BitVec 182)) (declare-const mpath211 (_ BitVec 182)) (declare-const mpath212 (_ BitVec 182)) (declare-const mpath213 (_ BitVec 182)) (declare-const mpath214 (_ BitVec 182)) (declare-const mpath215 (_ BitVec 182)) (declare-const mpath216 (_ BitVec 182)) (declare-const mpath217 (_ BitVec 182)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T mpath20 mpath21) (T mpath21 mpath22) (T mpath22 mpath23) (T mpath23 mpath24) (T mpath24 mpath25) (T mpath25 mpath26) (T mpath26 mpath27) (T mpath27 mpath28) (T mpath28 mpath29) (T mpath29 mpath210) (T mpath210 mpath211) (T mpath211 mpath212) (T mpath212 mpath213) (T mpath213 mpath214) (T mpath214 mpath215) (T mpath215 mpath216) (T mpath216 mpath217))) ; --------------- END (Path)------------------ (assert (Mid1 mpath20)) (declare-fun Mid2 ((_ BitVec 182) ) bool) ; ---------- Loop Free: --------------- (assert (and (and (not (= mpath21 mpath20))) (and (not (= mpath22 mpath20)) (not (= mpath22 mpath21))) (and (not (= mpath23 mpath20)) (not (= mpath23 mpath21)) (not (= mpath23 mpath22))) (and (not (= mpath24 mpath20)) (not (= mpath24 mpath21)) (not (= mpath24 mpath22)) (not (= mpath24 mpath23))) (and (not (= mpath25 mpath20)) (not (= mpath25 mpath21)) (not (= mpath25 mpath22)) (not (= mpath25 mpath23)) (not (= mpath25 mpath24))) (and (not (= mpath26 mpath20)) (not (= mpath26 mpath21)) (not (= mpath26 mpath22)) (not (= mpath26 mpath23)) (not (= mpath26 mpath24)) (not (= mpath26 mpath25))) (and (not (= mpath27 mpath20)) (not (= mpath27 mpath21)) (not (= mpath27 mpath22)) (not (= mpath27 mpath23)) (not (= mpath27 mpath24)) (not (= mpath27 mpath25)) (not (= mpath27 mpath26))) (and (not (= mpath28 mpath20)) (not (= mpath28 mpath21)) (not (= mpath28 mpath22)) (not (= mpath28 mpath23)) (not (= mpath28 mpath24)) (not (= mpath28 mpath25)) (not (= mpath28 mpath26)) (not (= mpath28 mpath27))) (and (not (= mpath29 mpath20)) (not (= mpath29 mpath21)) (not (= mpath29 mpath22)) (not (= mpath29 mpath23)) (not (= mpath29 mpath24)) (not (= mpath29 mpath25)) (not (= mpath29 mpath26)) (not (= mpath29 mpath27)) (not (= mpath29 mpath28))) (and (not (= mpath210 mpath20)) (not (= mpath210 mpath21)) (not (= mpath210 mpath22)) (not (= mpath210 mpath23)) (not (= mpath210 mpath24)) (not (= mpath210 mpath25)) (not (= mpath210 mpath26)) (not (= mpath210 mpath27)) (not (= mpath210 mpath28)) (not (= mpath210 mpath29))) (and (not (= mpath211 mpath20)) (not (= mpath211 mpath21)) (not (= mpath211 mpath22)) (not (= mpath211 mpath23)) (not (= mpath211 mpath24)) (not (= mpath211 mpath25)) (not (= mpath211 mpath26)) (not (= mpath211 mpath27)) (not (= mpath211 mpath28)) (not (= mpath211 mpath29)) (not (= mpath211 mpath210))) (and (not (= mpath212 mpath20)) (not (= mpath212 mpath21)) (not (= mpath212 mpath22)) (not (= mpath212 mpath23)) (not (= mpath212 mpath24)) (not (= mpath212 mpath25)) (not (= mpath212 mpath26)) (not (= mpath212 mpath27)) (not (= mpath212 mpath28)) (not (= mpath212 mpath29)) (not (= mpath212 mpath210)) (not (= mpath212 mpath211))) (and (not (= mpath213 mpath20)) (not (= mpath213 mpath21)) (not (= mpath213 mpath22)) (not (= mpath213 mpath23)) (not (= mpath213 mpath24)) (not (= mpath213 mpath25)) (not (= mpath213 mpath26)) (not (= mpath213 mpath27)) (not (= mpath213 mpath28)) (not (= mpath213 mpath29)) (not (= mpath213 mpath210)) (not (= mpath213 mpath211)) (not (= mpath213 mpath212))) (and (not (= mpath214 mpath20)) (not (= mpath214 mpath21)) (not (= mpath214 mpath22)) (not (= mpath214 mpath23)) (not (= mpath214 mpath24)) (not (= mpath214 mpath25)) (not (= mpath214 mpath26)) (not (= mpath214 mpath27)) (not (= mpath214 mpath28)) (not (= mpath214 mpath29)) (not (= mpath214 mpath210)) (not (= mpath214 mpath211)) (not (= mpath214 mpath212)) (not (= mpath214 mpath213))) (and (not (= mpath215 mpath20)) (not (= mpath215 mpath21)) (not (= mpath215 mpath22)) (not (= mpath215 mpath23)) (not (= mpath215 mpath24)) (not (= mpath215 mpath25)) (not (= mpath215 mpath26)) (not (= mpath215 mpath27)) (not (= mpath215 mpath28)) (not (= mpath215 mpath29)) (not (= mpath215 mpath210)) (not (= mpath215 mpath211)) (not (= mpath215 mpath212)) (not (= mpath215 mpath213)) (not (= mpath215 mpath214))) (and (not (= mpath216 mpath20)) (not (= mpath216 mpath21)) (not (= mpath216 mpath22)) (not (= mpath216 mpath23)) (not (= mpath216 mpath24)) (not (= mpath216 mpath25)) (not (= mpath216 mpath26)) (not (= mpath216 mpath27)) (not (= mpath216 mpath28)) (not (= mpath216 mpath29)) (not (= mpath216 mpath210)) (not (= mpath216 mpath211)) (not (= mpath216 mpath212)) (not (= mpath216 mpath213)) (not (= mpath216 mpath214)) (not (= mpath216 mpath215))) (and (not (= mpath217 mpath20)) (not (= mpath217 mpath21)) (not (= mpath217 mpath22)) (not (= mpath217 mpath23)) (not (= mpath217 mpath24)) (not (= mpath217 mpath25)) (not (= mpath217 mpath26)) (not (= mpath217 mpath27)) (not (= mpath217 mpath28)) (not (= mpath217 mpath29)) (not (= mpath217 mpath210)) (not (= mpath217 mpath211)) (not (= mpath217 mpath212)) (not (= mpath217 mpath213)) (not (= mpath217 mpath214)) (not (= mpath217 mpath215)) (not (= mpath217 mpath216))))) ; --------------- END (Loop free)------------------ (check-sat) (get-model) (eval mpath217) (assert (forall ((xs (_ BitVec 182)) )(= (Mid2 xs) (= xs (_ bv2298743311298833287537520540725463775428108683275403264 182))))) (declare-const mpath30 (_ BitVec 182)) (declare-const mpath31 (_ BitVec 182)) (declare-const mpath32 (_ BitVec 182)) (declare-const mpath33 (_ BitVec 182)) (declare-const mpath34 (_ BitVec 182)) (declare-const mpath35 (_ BitVec 182)) (declare-const mpath36 (_ BitVec 182)) (declare-const mpath37 (_ BitVec 182)) (declare-const mpath38 (_ BitVec 182)) (declare-const mpath39 (_ BitVec 182)) (declare-const mpath310 (_ BitVec 182)) (declare-const mpath311 (_ BitVec 182)) (declare-const mpath312 (_ BitVec 182)) (declare-const mpath313 (_ BitVec 182)) (declare-const mpath314 (_ BitVec 182)) (declare-const mpath315 (_ BitVec 182)) (declare-const mpath316 (_ BitVec 182)) (declare-const mpath317 (_ BitVec 182)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T mpath30 mpath31) (T mpath31 mpath32) (T mpath32 mpath33) (T mpath33 mpath34) (T mpath34 mpath35) (T mpath35 mpath36) (T mpath36 mpath37) (T mpath37 mpath38) (T mpath38 mpath39) (T mpath39 mpath310) (T mpath310 mpath311) (T mpath311 mpath312) (T mpath312 mpath313) (T mpath313 mpath314) (T mpath314 mpath315) (T mpath315 mpath316) (T mpath316 mpath317))) ; --------------- END (Path)------------------ (assert (Mid2 mpath30)) (declare-fun Mid3 ((_ BitVec 182) ) bool) ; ---------- Loop Free: --------------- (assert (and (and (not (= mpath31 mpath30))) (and (not (= mpath32 mpath30)) (not (= mpath32 mpath31))) (and (not (= mpath33 mpath30)) (not (= mpath33 mpath31)) (not (= mpath33 mpath32))) (and (not (= mpath34 mpath30)) (not (= mpath34 mpath31)) (not (= mpath34 mpath32)) (not (= mpath34 mpath33))) (and (not (= mpath35 mpath30)) (not (= mpath35 mpath31)) (not (= mpath35 mpath32)) (not (= mpath35 mpath33)) (not (= mpath35 mpath34))) (and (not (= mpath36 mpath30)) (not (= mpath36 mpath31)) (not (= mpath36 mpath32)) (not (= mpath36 mpath33)) (not (= mpath36 mpath34)) (not (= mpath36 mpath35))) (and (not (= mpath37 mpath30)) (not (= mpath37 mpath31)) (not (= mpath37 mpath32)) (not (= mpath37 mpath33)) (not (= mpath37 mpath34)) (not (= mpath37 mpath35)) (not (= mpath37 mpath36))) (and (not (= mpath38 mpath30)) (not (= mpath38 mpath31)) (not (= mpath38 mpath32)) (not (= mpath38 mpath33)) (not (= mpath38 mpath34)) (not (= mpath38 mpath35)) (not (= mpath38 mpath36)) (not (= mpath38 mpath37))) (and (not (= mpath39 mpath30)) (not (= mpath39 mpath31)) (not (= mpath39 mpath32)) (not (= mpath39 mpath33)) (not (= mpath39 mpath34)) (not (= mpath39 mpath35)) (not (= mpath39 mpath36)) (not (= mpath39 mpath37)) (not (= mpath39 mpath38))) (and (not (= mpath310 mpath30)) (not (= mpath310 mpath31)) (not (= mpath310 mpath32)) (not (= mpath310 mpath33)) (not (= mpath310 mpath34)) (not (= mpath310 mpath35)) (not (= mpath310 mpath36)) (not (= mpath310 mpath37)) (not (= mpath310 mpath38)) (not (= mpath310 mpath39))) (and (not (= mpath311 mpath30)) (not (= mpath311 mpath31)) (not (= mpath311 mpath32)) (not (= mpath311 mpath33)) (not (= mpath311 mpath34)) (not (= mpath311 mpath35)) (not (= mpath311 mpath36)) (not (= mpath311 mpath37)) (not (= mpath311 mpath38)) (not (= mpath311 mpath39)) (not (= mpath311 mpath310))) (and (not (= mpath312 mpath30)) (not (= mpath312 mpath31)) (not (= mpath312 mpath32)) (not (= mpath312 mpath33)) (not (= mpath312 mpath34)) (not (= mpath312 mpath35)) (not (= mpath312 mpath36)) (not (= mpath312 mpath37)) (not (= mpath312 mpath38)) (not (= mpath312 mpath39)) (not (= mpath312 mpath310)) (not (= mpath312 mpath311))) (and (not (= mpath313 mpath30)) (not (= mpath313 mpath31)) (not (= mpath313 mpath32)) (not (= mpath313 mpath33)) (not (= mpath313 mpath34)) (not (= mpath313 mpath35)) (not (= mpath313 mpath36)) (not (= mpath313 mpath37)) (not (= mpath313 mpath38)) (not (= mpath313 mpath39)) (not (= mpath313 mpath310)) (not (= mpath313 mpath311)) (not (= mpath313 mpath312))) (and (not (= mpath314 mpath30)) (not (= mpath314 mpath31)) (not (= mpath314 mpath32)) (not (= mpath314 mpath33)) (not (= mpath314 mpath34)) (not (= mpath314 mpath35)) (not (= mpath314 mpath36)) (not (= mpath314 mpath37)) (not (= mpath314 mpath38)) (not (= mpath314 mpath39)) (not (= mpath314 mpath310)) (not (= mpath314 mpath311)) (not (= mpath314 mpath312)) (not (= mpath314 mpath313))) (and (not (= mpath315 mpath30)) (not (= mpath315 mpath31)) (not (= mpath315 mpath32)) (not (= mpath315 mpath33)) (not (= mpath315 mpath34)) (not (= mpath315 mpath35)) (not (= mpath315 mpath36)) (not (= mpath315 mpath37)) (not (= mpath315 mpath38)) (not (= mpath315 mpath39)) (not (= mpath315 mpath310)) (not (= mpath315 mpath311)) (not (= mpath315 mpath312)) (not (= mpath315 mpath313)) (not (= mpath315 mpath314))) (and (not (= mpath316 mpath30)) (not (= mpath316 mpath31)) (not (= mpath316 mpath32)) (not (= mpath316 mpath33)) (not (= mpath316 mpath34)) (not (= mpath316 mpath35)) (not (= mpath316 mpath36)) (not (= mpath316 mpath37)) (not (= mpath316 mpath38)) (not (= mpath316 mpath39)) (not (= mpath316 mpath310)) (not (= mpath316 mpath311)) (not (= mpath316 mpath312)) (not (= mpath316 mpath313)) (not (= mpath316 mpath314)) (not (= mpath316 mpath315))) (and (not (= mpath317 mpath30)) (not (= mpath317 mpath31)) (not (= mpath317 mpath32)) (not (= mpath317 mpath33)) (not (= mpath317 mpath34)) (not (= mpath317 mpath35)) (not (= mpath317 mpath36)) (not (= mpath317 mpath37)) (not (= mpath317 mpath38)) (not (= mpath317 mpath39)) (not (= mpath317 mpath310)) (not (= mpath317 mpath311)) (not (= mpath317 mpath312)) (not (= mpath317 mpath313)) (not (= mpath317 mpath314)) (not (= mpath317 mpath315)) (not (= mpath317 mpath316))))) ; --------------- END (Loop free)------------------ (check-sat) (get-model) (eval mpath317) (assert (forall ((xs (_ BitVec 182)) )(= (Mid3 xs) (= xs (_ bv4980610507814138789664627838238504846760902147096707072 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 (Mid3 p0)) (check-sat) (get-model) (assert (= dlock p1)) (check-sat) (get-model) (eval mpath00) (eval dlock) (get-info :all-statistics)