(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) (_ bv6 6)) (= ((_ extract 11 6) xs) (_ bv6 6)) (= ((_ extract 17 12) xs) (_ bv6 6)) (= ((_ extract 23 18) xs) (_ bv12 6)) (= ((_ extract 29 24) xs) (_ bv6 6)) (= ((_ extract 35 30) xs) (_ bv6 6)) (= ((_ extract 41 36) xs) (_ bv6 6)) (= ((_ extract 47 42) xs) (_ bv6 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)) (declare-const mpath018 (_ BitVec 182)) (declare-const mpath019 (_ BitVec 182)) (declare-const mpath020 (_ BitVec 182)) (declare-const mpath021 (_ 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) (T mpath017 mpath018) (T mpath018 mpath019) (T mpath019 mpath020) (T mpath020 mpath021))) ; --------------- 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))) (and (not (= mpath018 mpath00)) (not (= mpath018 mpath01)) (not (= mpath018 mpath02)) (not (= mpath018 mpath03)) (not (= mpath018 mpath04)) (not (= mpath018 mpath05)) (not (= mpath018 mpath06)) (not (= mpath018 mpath07)) (not (= mpath018 mpath08)) (not (= mpath018 mpath09)) (not (= mpath018 mpath010)) (not (= mpath018 mpath011)) (not (= mpath018 mpath012)) (not (= mpath018 mpath013)) (not (= mpath018 mpath014)) (not (= mpath018 mpath015)) (not (= mpath018 mpath016)) (not (= mpath018 mpath017))) (and (not (= mpath019 mpath00)) (not (= mpath019 mpath01)) (not (= mpath019 mpath02)) (not (= mpath019 mpath03)) (not (= mpath019 mpath04)) (not (= mpath019 mpath05)) (not (= mpath019 mpath06)) (not (= mpath019 mpath07)) (not (= mpath019 mpath08)) (not (= mpath019 mpath09)) (not (= mpath019 mpath010)) (not (= mpath019 mpath011)) (not (= mpath019 mpath012)) (not (= mpath019 mpath013)) (not (= mpath019 mpath014)) (not (= mpath019 mpath015)) (not (= mpath019 mpath016)) (not (= mpath019 mpath017)) (not (= mpath019 mpath018))) (and (not (= mpath020 mpath00)) (not (= mpath020 mpath01)) (not (= mpath020 mpath02)) (not (= mpath020 mpath03)) (not (= mpath020 mpath04)) (not (= mpath020 mpath05)) (not (= mpath020 mpath06)) (not (= mpath020 mpath07)) (not (= mpath020 mpath08)) (not (= mpath020 mpath09)) (not (= mpath020 mpath010)) (not (= mpath020 mpath011)) (not (= mpath020 mpath012)) (not (= mpath020 mpath013)) (not (= mpath020 mpath014)) (not (= mpath020 mpath015)) (not (= mpath020 mpath016)) (not (= mpath020 mpath017)) (not (= mpath020 mpath018)) (not (= mpath020 mpath019))) (and (not (= mpath021 mpath00)) (not (= mpath021 mpath01)) (not (= mpath021 mpath02)) (not (= mpath021 mpath03)) (not (= mpath021 mpath04)) (not (= mpath021 mpath05)) (not (= mpath021 mpath06)) (not (= mpath021 mpath07)) (not (= mpath021 mpath08)) (not (= mpath021 mpath09)) (not (= mpath021 mpath010)) (not (= mpath021 mpath011)) (not (= mpath021 mpath012)) (not (= mpath021 mpath013)) (not (= mpath021 mpath014)) (not (= mpath021 mpath015)) (not (= mpath021 mpath016)) (not (= mpath021 mpath017)) (not (= mpath021 mpath018)) (not (= mpath021 mpath019)) (not (= mpath021 mpath020))))) ; --------------- END (Loop free)------------------ (check-sat) (get-model) (eval mpath021) (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)) (declare-const mpath118 (_ BitVec 182)) (declare-const mpath119 (_ BitVec 182)) (declare-const mpath120 (_ BitVec 182)) (declare-const mpath121 (_ 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) (T mpath117 mpath118) (T mpath118 mpath119) (T mpath119 mpath120) (T mpath120 mpath121))) ; --------------- 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))) (and (not (= mpath118 mpath10)) (not (= mpath118 mpath11)) (not (= mpath118 mpath12)) (not (= mpath118 mpath13)) (not (= mpath118 mpath14)) (not (= mpath118 mpath15)) (not (= mpath118 mpath16)) (not (= mpath118 mpath17)) (not (= mpath118 mpath18)) (not (= mpath118 mpath19)) (not (= mpath118 mpath110)) (not (= mpath118 mpath111)) (not (= mpath118 mpath112)) (not (= mpath118 mpath113)) (not (= mpath118 mpath114)) (not (= mpath118 mpath115)) (not (= mpath118 mpath116)) (not (= mpath118 mpath117))) (and (not (= mpath119 mpath10)) (not (= mpath119 mpath11)) (not (= mpath119 mpath12)) (not (= mpath119 mpath13)) (not (= mpath119 mpath14)) (not (= mpath119 mpath15)) (not (= mpath119 mpath16)) (not (= mpath119 mpath17)) (not (= mpath119 mpath18)) (not (= mpath119 mpath19)) (not (= mpath119 mpath110)) (not (= mpath119 mpath111)) (not (= mpath119 mpath112)) (not (= mpath119 mpath113)) (not (= mpath119 mpath114)) (not (= mpath119 mpath115)) (not (= mpath119 mpath116)) (not (= mpath119 mpath117)) (not (= mpath119 mpath118))) (and (not (= mpath120 mpath10)) (not (= mpath120 mpath11)) (not (= mpath120 mpath12)) (not (= mpath120 mpath13)) (not (= mpath120 mpath14)) (not (= mpath120 mpath15)) (not (= mpath120 mpath16)) (not (= mpath120 mpath17)) (not (= mpath120 mpath18)) (not (= mpath120 mpath19)) (not (= mpath120 mpath110)) (not (= mpath120 mpath111)) (not (= mpath120 mpath112)) (not (= mpath120 mpath113)) (not (= mpath120 mpath114)) (not (= mpath120 mpath115)) (not (= mpath120 mpath116)) (not (= mpath120 mpath117)) (not (= mpath120 mpath118)) (not (= mpath120 mpath119))) (and (not (= mpath121 mpath10)) (not (= mpath121 mpath11)) (not (= mpath121 mpath12)) (not (= mpath121 mpath13)) (not (= mpath121 mpath14)) (not (= mpath121 mpath15)) (not (= mpath121 mpath16)) (not (= mpath121 mpath17)) (not (= mpath121 mpath18)) (not (= mpath121 mpath19)) (not (= mpath121 mpath110)) (not (= mpath121 mpath111)) (not (= mpath121 mpath112)) (not (= mpath121 mpath113)) (not (= mpath121 mpath114)) (not (= mpath121 mpath115)) (not (= mpath121 mpath116)) (not (= mpath121 mpath117)) (not (= mpath121 mpath118)) (not (= mpath121 mpath119)) (not (= mpath121 mpath120))))) ; --------------- END (Loop free)------------------ (check-sat) (get-model) (eval mpath121) (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)) (declare-const mpath218 (_ BitVec 182)) (declare-const mpath219 (_ BitVec 182)) (declare-const mpath220 (_ BitVec 182)) (declare-const mpath221 (_ 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) (T mpath217 mpath218) (T mpath218 mpath219) (T mpath219 mpath220) (T mpath220 mpath221))) ; --------------- 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))) (and (not (= mpath218 mpath20)) (not (= mpath218 mpath21)) (not (= mpath218 mpath22)) (not (= mpath218 mpath23)) (not (= mpath218 mpath24)) (not (= mpath218 mpath25)) (not (= mpath218 mpath26)) (not (= mpath218 mpath27)) (not (= mpath218 mpath28)) (not (= mpath218 mpath29)) (not (= mpath218 mpath210)) (not (= mpath218 mpath211)) (not (= mpath218 mpath212)) (not (= mpath218 mpath213)) (not (= mpath218 mpath214)) (not (= mpath218 mpath215)) (not (= mpath218 mpath216)) (not (= mpath218 mpath217))) (and (not (= mpath219 mpath20)) (not (= mpath219 mpath21)) (not (= mpath219 mpath22)) (not (= mpath219 mpath23)) (not (= mpath219 mpath24)) (not (= mpath219 mpath25)) (not (= mpath219 mpath26)) (not (= mpath219 mpath27)) (not (= mpath219 mpath28)) (not (= mpath219 mpath29)) (not (= mpath219 mpath210)) (not (= mpath219 mpath211)) (not (= mpath219 mpath212)) (not (= mpath219 mpath213)) (not (= mpath219 mpath214)) (not (= mpath219 mpath215)) (not (= mpath219 mpath216)) (not (= mpath219 mpath217)) (not (= mpath219 mpath218))) (and (not (= mpath220 mpath20)) (not (= mpath220 mpath21)) (not (= mpath220 mpath22)) (not (= mpath220 mpath23)) (not (= mpath220 mpath24)) (not (= mpath220 mpath25)) (not (= mpath220 mpath26)) (not (= mpath220 mpath27)) (not (= mpath220 mpath28)) (not (= mpath220 mpath29)) (not (= mpath220 mpath210)) (not (= mpath220 mpath211)) (not (= mpath220 mpath212)) (not (= mpath220 mpath213)) (not (= mpath220 mpath214)) (not (= mpath220 mpath215)) (not (= mpath220 mpath216)) (not (= mpath220 mpath217)) (not (= mpath220 mpath218)) (not (= mpath220 mpath219))) (and (not (= mpath221 mpath20)) (not (= mpath221 mpath21)) (not (= mpath221 mpath22)) (not (= mpath221 mpath23)) (not (= mpath221 mpath24)) (not (= mpath221 mpath25)) (not (= mpath221 mpath26)) (not (= mpath221 mpath27)) (not (= mpath221 mpath28)) (not (= mpath221 mpath29)) (not (= mpath221 mpath210)) (not (= mpath221 mpath211)) (not (= mpath221 mpath212)) (not (= mpath221 mpath213)) (not (= mpath221 mpath214)) (not (= mpath221 mpath215)) (not (= mpath221 mpath216)) (not (= mpath221 mpath217)) (not (= mpath221 mpath218)) (not (= mpath221 mpath219)) (not (= mpath221 mpath220))))) ; --------------- END (Loop free)------------------ (check-sat) (get-model) (eval mpath221) (assert (forall ((xs (_ BitVec 182)) )(= (Mid2 xs) (= xs (_ bv16384 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)) (declare-const mpath318 (_ BitVec 182)) (declare-const mpath319 (_ BitVec 182)) (declare-const mpath320 (_ BitVec 182)) (declare-const mpath321 (_ 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) (T mpath317 mpath318) (T mpath318 mpath319) (T mpath319 mpath320) (T mpath320 mpath321))) ; --------------- 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))) (and (not (= mpath318 mpath30)) (not (= mpath318 mpath31)) (not (= mpath318 mpath32)) (not (= mpath318 mpath33)) (not (= mpath318 mpath34)) (not (= mpath318 mpath35)) (not (= mpath318 mpath36)) (not (= mpath318 mpath37)) (not (= mpath318 mpath38)) (not (= mpath318 mpath39)) (not (= mpath318 mpath310)) (not (= mpath318 mpath311)) (not (= mpath318 mpath312)) (not (= mpath318 mpath313)) (not (= mpath318 mpath314)) (not (= mpath318 mpath315)) (not (= mpath318 mpath316)) (not (= mpath318 mpath317))) (and (not (= mpath319 mpath30)) (not (= mpath319 mpath31)) (not (= mpath319 mpath32)) (not (= mpath319 mpath33)) (not (= mpath319 mpath34)) (not (= mpath319 mpath35)) (not (= mpath319 mpath36)) (not (= mpath319 mpath37)) (not (= mpath319 mpath38)) (not (= mpath319 mpath39)) (not (= mpath319 mpath310)) (not (= mpath319 mpath311)) (not (= mpath319 mpath312)) (not (= mpath319 mpath313)) (not (= mpath319 mpath314)) (not (= mpath319 mpath315)) (not (= mpath319 mpath316)) (not (= mpath319 mpath317)) (not (= mpath319 mpath318))) (and (not (= mpath320 mpath30)) (not (= mpath320 mpath31)) (not (= mpath320 mpath32)) (not (= mpath320 mpath33)) (not (= mpath320 mpath34)) (not (= mpath320 mpath35)) (not (= mpath320 mpath36)) (not (= mpath320 mpath37)) (not (= mpath320 mpath38)) (not (= mpath320 mpath39)) (not (= mpath320 mpath310)) (not (= mpath320 mpath311)) (not (= mpath320 mpath312)) (not (= mpath320 mpath313)) (not (= mpath320 mpath314)) (not (= mpath320 mpath315)) (not (= mpath320 mpath316)) (not (= mpath320 mpath317)) (not (= mpath320 mpath318)) (not (= mpath320 mpath319))) (and (not (= mpath321 mpath30)) (not (= mpath321 mpath31)) (not (= mpath321 mpath32)) (not (= mpath321 mpath33)) (not (= mpath321 mpath34)) (not (= mpath321 mpath35)) (not (= mpath321 mpath36)) (not (= mpath321 mpath37)) (not (= mpath321 mpath38)) (not (= mpath321 mpath39)) (not (= mpath321 mpath310)) (not (= mpath321 mpath311)) (not (= mpath321 mpath312)) (not (= mpath321 mpath313)) (not (= mpath321 mpath314)) (not (= mpath321 mpath315)) (not (= mpath321 mpath316)) (not (= mpath321 mpath317)) (not (= mpath321 mpath318)) (not (= mpath321 mpath319)) (not (= mpath321 mpath320))))) ; --------------- END (Loop free)------------------ (check-sat) (get-model) (eval mpath321) (assert (forall ((xs (_ BitVec 182)) )(= (Mid3 xs) (= xs (_ bv2298743311298833287537520540725463775428108683275403264 182))))) (declare-const mpath40 (_ BitVec 182)) (declare-const mpath41 (_ BitVec 182)) (declare-const mpath42 (_ BitVec 182)) (declare-const mpath43 (_ BitVec 182)) (declare-const mpath44 (_ BitVec 182)) (declare-const mpath45 (_ BitVec 182)) (declare-const mpath46 (_ BitVec 182)) (declare-const mpath47 (_ BitVec 182)) (declare-const mpath48 (_ BitVec 182)) (declare-const mpath49 (_ BitVec 182)) (declare-const mpath410 (_ BitVec 182)) (declare-const mpath411 (_ BitVec 182)) (declare-const mpath412 (_ BitVec 182)) (declare-const mpath413 (_ BitVec 182)) (declare-const mpath414 (_ BitVec 182)) (declare-const mpath415 (_ BitVec 182)) (declare-const mpath416 (_ BitVec 182)) (declare-const mpath417 (_ BitVec 182)) (declare-const mpath418 (_ BitVec 182)) (declare-const mpath419 (_ BitVec 182)) (declare-const mpath420 (_ BitVec 182)) (declare-const mpath421 (_ BitVec 182)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T mpath40 mpath41) (T mpath41 mpath42) (T mpath42 mpath43) (T mpath43 mpath44) (T mpath44 mpath45) (T mpath45 mpath46) (T mpath46 mpath47) (T mpath47 mpath48) (T mpath48 mpath49) (T mpath49 mpath410) (T mpath410 mpath411) (T mpath411 mpath412) (T mpath412 mpath413) (T mpath413 mpath414) (T mpath414 mpath415) (T mpath415 mpath416) (T mpath416 mpath417) (T mpath417 mpath418) (T mpath418 mpath419) (T mpath419 mpath420) (T mpath420 mpath421))) ; --------------- END (Path)------------------ (assert (Mid3 mpath40)) (declare-fun Mid4 ((_ BitVec 182) ) bool) ; ---------- Loop Free: --------------- (assert (and (and (not (= mpath41 mpath40))) (and (not (= mpath42 mpath40)) (not (= mpath42 mpath41))) (and (not (= mpath43 mpath40)) (not (= mpath43 mpath41)) (not (= mpath43 mpath42))) (and (not (= mpath44 mpath40)) (not (= mpath44 mpath41)) (not (= mpath44 mpath42)) (not (= mpath44 mpath43))) (and (not (= mpath45 mpath40)) (not (= mpath45 mpath41)) (not (= mpath45 mpath42)) (not (= mpath45 mpath43)) (not (= mpath45 mpath44))) (and (not (= mpath46 mpath40)) (not (= mpath46 mpath41)) (not (= mpath46 mpath42)) (not (= mpath46 mpath43)) (not (= mpath46 mpath44)) (not (= mpath46 mpath45))) (and (not (= mpath47 mpath40)) (not (= mpath47 mpath41)) (not (= mpath47 mpath42)) (not (= mpath47 mpath43)) (not (= mpath47 mpath44)) (not (= mpath47 mpath45)) (not (= mpath47 mpath46))) (and (not (= mpath48 mpath40)) (not (= mpath48 mpath41)) (not (= mpath48 mpath42)) (not (= mpath48 mpath43)) (not (= mpath48 mpath44)) (not (= mpath48 mpath45)) (not (= mpath48 mpath46)) (not (= mpath48 mpath47))) (and (not (= mpath49 mpath40)) (not (= mpath49 mpath41)) (not (= mpath49 mpath42)) (not (= mpath49 mpath43)) (not (= mpath49 mpath44)) (not (= mpath49 mpath45)) (not (= mpath49 mpath46)) (not (= mpath49 mpath47)) (not (= mpath49 mpath48))) (and (not (= mpath410 mpath40)) (not (= mpath410 mpath41)) (not (= mpath410 mpath42)) (not (= mpath410 mpath43)) (not (= mpath410 mpath44)) (not (= mpath410 mpath45)) (not (= mpath410 mpath46)) (not (= mpath410 mpath47)) (not (= mpath410 mpath48)) (not (= mpath410 mpath49))) (and (not (= mpath411 mpath40)) (not (= mpath411 mpath41)) (not (= mpath411 mpath42)) (not (= mpath411 mpath43)) (not (= mpath411 mpath44)) (not (= mpath411 mpath45)) (not (= mpath411 mpath46)) (not (= mpath411 mpath47)) (not (= mpath411 mpath48)) (not (= mpath411 mpath49)) (not (= mpath411 mpath410))) (and (not (= mpath412 mpath40)) (not (= mpath412 mpath41)) (not (= mpath412 mpath42)) (not (= mpath412 mpath43)) (not (= mpath412 mpath44)) (not (= mpath412 mpath45)) (not (= mpath412 mpath46)) (not (= mpath412 mpath47)) (not (= mpath412 mpath48)) (not (= mpath412 mpath49)) (not (= mpath412 mpath410)) (not (= mpath412 mpath411))) (and (not (= mpath413 mpath40)) (not (= mpath413 mpath41)) (not (= mpath413 mpath42)) (not (= mpath413 mpath43)) (not (= mpath413 mpath44)) (not (= mpath413 mpath45)) (not (= mpath413 mpath46)) (not (= mpath413 mpath47)) (not (= mpath413 mpath48)) (not (= mpath413 mpath49)) (not (= mpath413 mpath410)) (not (= mpath413 mpath411)) (not (= mpath413 mpath412))) (and (not (= mpath414 mpath40)) (not (= mpath414 mpath41)) (not (= mpath414 mpath42)) (not (= mpath414 mpath43)) (not (= mpath414 mpath44)) (not (= mpath414 mpath45)) (not (= mpath414 mpath46)) (not (= mpath414 mpath47)) (not (= mpath414 mpath48)) (not (= mpath414 mpath49)) (not (= mpath414 mpath410)) (not (= mpath414 mpath411)) (not (= mpath414 mpath412)) (not (= mpath414 mpath413))) (and (not (= mpath415 mpath40)) (not (= mpath415 mpath41)) (not (= mpath415 mpath42)) (not (= mpath415 mpath43)) (not (= mpath415 mpath44)) (not (= mpath415 mpath45)) (not (= mpath415 mpath46)) (not (= mpath415 mpath47)) (not (= mpath415 mpath48)) (not (= mpath415 mpath49)) (not (= mpath415 mpath410)) (not (= mpath415 mpath411)) (not (= mpath415 mpath412)) (not (= mpath415 mpath413)) (not (= mpath415 mpath414))) (and (not (= mpath416 mpath40)) (not (= mpath416 mpath41)) (not (= mpath416 mpath42)) (not (= mpath416 mpath43)) (not (= mpath416 mpath44)) (not (= mpath416 mpath45)) (not (= mpath416 mpath46)) (not (= mpath416 mpath47)) (not (= mpath416 mpath48)) (not (= mpath416 mpath49)) (not (= mpath416 mpath410)) (not (= mpath416 mpath411)) (not (= mpath416 mpath412)) (not (= mpath416 mpath413)) (not (= mpath416 mpath414)) (not (= mpath416 mpath415))) (and (not (= mpath417 mpath40)) (not (= mpath417 mpath41)) (not (= mpath417 mpath42)) (not (= mpath417 mpath43)) (not (= mpath417 mpath44)) (not (= mpath417 mpath45)) (not (= mpath417 mpath46)) (not (= mpath417 mpath47)) (not (= mpath417 mpath48)) (not (= mpath417 mpath49)) (not (= mpath417 mpath410)) (not (= mpath417 mpath411)) (not (= mpath417 mpath412)) (not (= mpath417 mpath413)) (not (= mpath417 mpath414)) (not (= mpath417 mpath415)) (not (= mpath417 mpath416))) (and (not (= mpath418 mpath40)) (not (= mpath418 mpath41)) (not (= mpath418 mpath42)) (not (= mpath418 mpath43)) (not (= mpath418 mpath44)) (not (= mpath418 mpath45)) (not (= mpath418 mpath46)) (not (= mpath418 mpath47)) (not (= mpath418 mpath48)) (not (= mpath418 mpath49)) (not (= mpath418 mpath410)) (not (= mpath418 mpath411)) (not (= mpath418 mpath412)) (not (= mpath418 mpath413)) (not (= mpath418 mpath414)) (not (= mpath418 mpath415)) (not (= mpath418 mpath416)) (not (= mpath418 mpath417))) (and (not (= mpath419 mpath40)) (not (= mpath419 mpath41)) (not (= mpath419 mpath42)) (not (= mpath419 mpath43)) (not (= mpath419 mpath44)) (not (= mpath419 mpath45)) (not (= mpath419 mpath46)) (not (= mpath419 mpath47)) (not (= mpath419 mpath48)) (not (= mpath419 mpath49)) (not (= mpath419 mpath410)) (not (= mpath419 mpath411)) (not (= mpath419 mpath412)) (not (= mpath419 mpath413)) (not (= mpath419 mpath414)) (not (= mpath419 mpath415)) (not (= mpath419 mpath416)) (not (= mpath419 mpath417)) (not (= mpath419 mpath418))) (and (not (= mpath420 mpath40)) (not (= mpath420 mpath41)) (not (= mpath420 mpath42)) (not (= mpath420 mpath43)) (not (= mpath420 mpath44)) (not (= mpath420 mpath45)) (not (= mpath420 mpath46)) (not (= mpath420 mpath47)) (not (= mpath420 mpath48)) (not (= mpath420 mpath49)) (not (= mpath420 mpath410)) (not (= mpath420 mpath411)) (not (= mpath420 mpath412)) (not (= mpath420 mpath413)) (not (= mpath420 mpath414)) (not (= mpath420 mpath415)) (not (= mpath420 mpath416)) (not (= mpath420 mpath417)) (not (= mpath420 mpath418)) (not (= mpath420 mpath419))) (and (not (= mpath421 mpath40)) (not (= mpath421 mpath41)) (not (= mpath421 mpath42)) (not (= mpath421 mpath43)) (not (= mpath421 mpath44)) (not (= mpath421 mpath45)) (not (= mpath421 mpath46)) (not (= mpath421 mpath47)) (not (= mpath421 mpath48)) (not (= mpath421 mpath49)) (not (= mpath421 mpath410)) (not (= mpath421 mpath411)) (not (= mpath421 mpath412)) (not (= mpath421 mpath413)) (not (= mpath421 mpath414)) (not (= mpath421 mpath415)) (not (= mpath421 mpath416)) (not (= mpath421 mpath417)) (not (= mpath421 mpath418)) (not (= mpath421 mpath419)) (not (= mpath421 mpath420))))) ; --------------- END (Loop free)------------------ (check-sat) (get-model) (eval mpath421) (assert (forall ((xs (_ BitVec 182)) )(= (Mid4 xs) (= xs (_ bv4022800794772958253190660946269561606999190195731955712 182))))) (declare-const dlock (_ BitVec 182)) (assert (= (bvand dlock (_ bv6129976317457006109821715293861905869342877865004236800 182)) (_ bv0 182))) (assert (bvugt (bvand dlock (_ bv1405295396650831781587613638119892659365478399 182)) (_ bv1 182))) (push) (declare-const p0 (_ BitVec 182)) (declare-const p1 (_ BitVec 182)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p0 p1))) ; --------------- END (Path)------------------ ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))))) ; --------------- END (Loop free)------------------ (assert (Mid4 p0)) (check-sat) (get-model) (assert (= dlock p1)) (check-sat) (get-model) (eval mpath00) (eval dlock) (get-info :all-statistics)