1(set-option :print-success false) 2(set-logic AUFLIAFS) 3(set-info :status unsat) 4(declare-sort Loc 0) 5(define-sort SetLoc () (Set Loc)) 6(define-sort SetInt () (Set Int)) 7(declare-sort FldLoc 0) 8(declare-sort FldInt 0) 9(declare-fun null$0 () Loc) 10(declare-fun read$0 (FldLoc Loc) Loc) 11(declare-fun write$0 (FldLoc Loc Loc) FldLoc) 12(declare-fun ep$0 (FldLoc SetLoc Loc) Loc) 13(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool) 14(declare-fun Frame$0 (SetLoc SetLoc FldLoc FldLoc) Bool) 15(declare-fun Alloc$0 () SetLoc) 16(declare-fun FP$0 () SetLoc) 17(declare-fun FP_1$0 () SetLoc) 18(declare-fun FP_2$0 () SetLoc) 19(declare-fun FP_Caller$0 () SetLoc) 20(declare-fun FP_Caller_1$0 () SetLoc) 21(declare-fun curr_2$0 () Loc) 22(declare-fun curr_3$0 () Loc) 23(declare-fun lseg_domain$0 (FldLoc Loc Loc) SetLoc) 24(declare-fun lseg_struct$0 (SetLoc FldLoc Loc Loc) Bool) 25(declare-fun lst$0 () Loc) 26(declare-fun lst_1$0 () Loc) 27(declare-fun next$0 () FldLoc) 28(declare-fun next_1$0 () FldLoc) 29(declare-fun nondet_2$0 () Bool) 30(declare-fun sk_?X_27$0 () SetLoc) 31(declare-fun sk_?X_28$0 () SetLoc) 32(declare-fun sk_?X_29$0 () SetLoc) 33(declare-fun sk_?X_30$0 () SetLoc) 34(declare-fun sk_?X_31$0 () SetLoc) 35(declare-fun sk_?X_32$0 () SetLoc) 36(declare-fun sk_?X_33$0 () SetLoc) 37(declare-fun tmp_2$0 () Loc) 38 39(assert (! (forall ((?y Loc)) 40 (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y) 41 (Btwn$0 next$0 null$0 (read$0 next$0 null$0) ?y))) 42 :named btwn_reach_8)) 43 44(assert (! (forall ((?y Loc)) 45 (or (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y) 46 (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) ?y))) 47 :named btwn_reach_9)) 48 49(assert (! (forall ((?y Loc)) 50 (or (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y) 51 (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) ?y))) 52 :named btwn_reach_10)) 53 54(assert (! (forall ((?y Loc)) 55 (or (not (= (read$0 next$0 null$0) null$0)) 56 (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y))) 57 :named btwn_cycl_8)) 58 59(assert (! (forall ((?y Loc)) 60 (or (not (= (read$0 next$0 tmp_2$0) tmp_2$0)) 61 (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y))) 62 :named btwn_cycl_9)) 63 64(assert (! (forall ((?y Loc)) 65 (or (not (= (read$0 next$0 curr_3$0) curr_3$0)) 66 (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y))) 67 :named btwn_cycl_10)) 68 69(assert (! (Btwn$0 next$0 null$0 (read$0 next$0 null$0) (read$0 next$0 null$0)) 70 :named btwn_step_8)) 71 72(assert (! (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) (read$0 next$0 tmp_2$0)) 73 :named btwn_step_9)) 74 75(assert (! (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) (read$0 next$0 curr_3$0)) 76 :named btwn_step_10)) 77 78(assert (! (forall ((?f FldLoc)) 79 (or (member (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0) 80 (= null$0 (ep$0 ?f sk_?X_30$0 null$0)))) 81 :named entry-point3_10)) 82 83(assert (! (forall ((?f FldLoc)) 84 (or (member (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0) 85 (= lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0)))) 86 :named entry-point3_11)) 87 88(assert (! (forall ((?f FldLoc)) 89 (or (member (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0) 90 (= curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0)))) 91 :named entry-point3_12)) 92 93(assert (! (forall ((?f FldLoc)) 94 (or (member (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0) 95 (= tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0)))) 96 :named entry-point3_13)) 97 98(assert (! (forall ((?f FldLoc)) 99 (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0) 100 (ep$0 ?f sk_?X_30$0 null$0))) 101 :named entry-point1_10)) 102 103(assert (! (forall ((?f FldLoc)) 104 (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0) 105 (ep$0 ?f sk_?X_30$0 lst_1$0))) 106 :named entry-point1_11)) 107 108(assert (! (forall ((?f FldLoc)) 109 (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0) 110 (ep$0 ?f sk_?X_30$0 curr_3$0))) 111 :named entry-point1_12)) 112 113(assert (! (forall ((?f FldLoc)) 114 (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0) 115 (ep$0 ?f sk_?X_30$0 tmp_2$0))) 116 :named entry-point1_13)) 117 118(assert (! (forall ((?f FldLoc) (?y Loc)) 119 (or (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0) ?y) 120 (not (Btwn$0 ?f null$0 ?y ?y)) (not (member ?y sk_?X_30$0)))) 121 :named entry-point4_10)) 122 123(assert (! (forall ((?f FldLoc) (?y Loc)) 124 (or (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0) ?y) 125 (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (member ?y sk_?X_30$0)))) 126 :named entry-point4_11)) 127 128(assert (! (forall ((?f FldLoc) (?y Loc)) 129 (or (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0) ?y) 130 (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (member ?y sk_?X_30$0)))) 131 :named entry-point4_12)) 132 133(assert (! (forall ((?f FldLoc) (?y Loc)) 134 (or (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0) ?y) 135 (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (member ?y sk_?X_30$0)))) 136 :named entry-point4_13)) 137 138(assert (! (forall ((?f FldLoc) (?y Loc)) 139 (or (not (Btwn$0 ?f null$0 ?y ?y)) (not (member ?y sk_?X_30$0)) 140 (member (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0))) 141 :named entry-point2_10)) 142 143(assert (! (forall ((?f FldLoc) (?y Loc)) 144 (or (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (member ?y sk_?X_30$0)) 145 (member (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0))) 146 :named entry-point2_11)) 147 148(assert (! (forall ((?f FldLoc) (?y Loc)) 149 (or (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (member ?y sk_?X_30$0)) 150 (member (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0))) 151 :named entry-point2_12)) 152 153(assert (! (forall ((?f FldLoc) (?y Loc)) 154 (or (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (member ?y sk_?X_30$0)) 155 (member (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0))) 156 :named entry-point2_13)) 157 158(assert (! (= (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0) 159 (read$0 next$0 tmp_2$0)) 160 :named read_write2)) 161 162(assert (! (or (= null$0 curr_3$0) 163 (= (read$0 next$0 null$0) 164 (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) null$0))) 165 :named read_write1)) 166 167(assert (! (or (= tmp_2$0 curr_3$0) 168 (= (read$0 next$0 tmp_2$0) 169 (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) tmp_2$0))) 170 :named read_write1_1)) 171 172(assert (! (or (= curr_3$0 curr_3$0) 173 (= (read$0 next$0 curr_3$0) 174 (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0))) 175 :named read_write1_2)) 176 177(assert (! (= (read$0 next$0 null$0) null$0) :named read_null_5)) 178 179(assert (! (= (read$0 next_1$0 null$0) null$0) :named read_null_6)) 180 181(assert (! (forall ((l1 Loc)) 182 (or 183 (and (Btwn$0 next$0 lst$0 l1 curr_2$0) 184 (member l1 (lseg_domain$0 next$0 lst$0 curr_2$0)) 185 (not (= l1 curr_2$0))) 186 (and 187 (or (= l1 curr_2$0) 188 (not (Btwn$0 next$0 lst$0 l1 curr_2$0))) 189 (not (member l1 (lseg_domain$0 next$0 lst$0 curr_2$0)))))) 190 :named lseg_footprint_20)) 191 192(assert (! (forall ((l1 Loc)) 193 (or 194 (and (Btwn$0 next$0 curr_3$0 l1 null$0) 195 (member l1 (lseg_domain$0 next$0 curr_3$0 null$0)) 196 (not (= l1 null$0))) 197 (and 198 (or (= l1 null$0) 199 (not (Btwn$0 next$0 curr_3$0 l1 null$0))) 200 (not (member l1 (lseg_domain$0 next$0 curr_3$0 null$0)))))) 201 :named lseg_footprint_21)) 202 203(assert (! (not (member tmp_2$0 FP_2$0)) :named check_free_31_6)) 204 205(assert (! (not (member null$0 Alloc$0)) :named framecondition_of_remove_loop_18_4_15)) 206 207(assert (! (not (= lst$0 null$0)) :named if_else_13_6_4)) 208 209(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0)) 210 :named precondition_of_remove_10_11_20)) 211 212(assert (! (= sk_?X_33$0 FP$0) :named precondition_of_remove_10_11_21)) 213 214(assert (! (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0) :named invariant_18_4_62)) 215 216(assert (! (= FP$0 (union FP_1$0 FP$0)) :named invariant_18_4_63)) 217 218(assert (! (= sk_?X_31$0 (lseg_domain$0 next$0 curr_2$0 null$0)) 219 :named invariant_18_4_64)) 220 221(assert (! (= sk_?X_30$0 (union sk_?X_31$0 sk_?X_32$0)) :named invariant_18_4_65)) 222 223(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_66)) 224 225(assert (! (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0) 226 :named invariant_18_4_67)) 227 228(assert (! (= sk_?X_29$0 (union sk_?X_28$0 sk_?X_27$0)) :named invariant_18_4_68)) 229 230(assert (! (= sk_?X_28$0 (lseg_domain$0 next$0 curr_3$0 null$0)) 231 :named invariant_18_4_69)) 232 233(assert (! (= (as emptyset SetLoc) (intersection sk_?X_27$0 sk_?X_28$0)) 234 :named invariant_18_4_70)) 235 236(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0)) 237 :named initial_footprint_of_remove_10_11_10)) 238 239(assert (! (Frame$0 FP_1$0 Alloc$0 next$0 next$0) 240 :named framecondition_of_remove_loop_18_4_16)) 241 242(assert (! (= next_1$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0))) 243 :named assign_30_6)) 244 245(assert (! (= curr_2$0 lst$0) :named assign_17_4_4)) 246 247(assert (! (= FP_2$0 248 (union (setminus FP$0 FP_1$0) 249 (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0)))) 250 :named framecondition_of_remove_loop_18_4_17)) 251 252(assert (! (or (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0) 253 (not (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0))) 254 :named unnamed_23)) 255 256(assert (! (or (Btwn$0 next$0 curr_3$0 null$0 null$0) 257 (not (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0))) 258 :named unnamed_24)) 259 260(assert (! (or (= (read$0 next$0 curr_3$0) null$0) (not nondet_2$0)) 261 :named unnamed_25)) 262 263(assert (! (forall ((l1 Loc)) 264 (or 265 (and (Btwn$0 next$0 lst_1$0 l1 curr_3$0) 266 (member l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0)) 267 (not (= l1 curr_3$0))) 268 (and 269 (or (= l1 curr_3$0) 270 (not (Btwn$0 next$0 lst_1$0 l1 curr_3$0))) 271 (not (member l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0)))))) 272 :named lseg_footprint_22)) 273 274(assert (! (forall ((l1 Loc)) 275 (or 276 (and (Btwn$0 next$0 lst$0 l1 null$0) 277 (member l1 (lseg_domain$0 next$0 lst$0 null$0)) 278 (not (= l1 null$0))) 279 (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0))) 280 (not (member l1 (lseg_domain$0 next$0 lst$0 null$0)))))) 281 :named lseg_footprint_23)) 282 283(assert (! (forall ((l1 Loc)) 284 (or 285 (and (Btwn$0 next$0 curr_2$0 l1 null$0) 286 (member l1 (lseg_domain$0 next$0 curr_2$0 null$0)) 287 (not (= l1 null$0))) 288 (and 289 (or (= l1 null$0) 290 (not (Btwn$0 next$0 curr_2$0 l1 null$0))) 291 (not (member l1 (lseg_domain$0 next$0 curr_2$0 null$0)))))) 292 :named lseg_footprint_24)) 293 294(assert (! (not (member null$0 Alloc$0)) :named initial_footprint_of_remove_10_11_11)) 295 296(assert (! (not (= tmp_2$0 null$0)) :named if_else_28_8_2)) 297 298(assert (! (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0) 299 :named precondition_of_remove_10_11_22)) 300 301(assert (! (= sk_?X_33$0 (lseg_domain$0 next$0 lst$0 null$0)) 302 :named precondition_of_remove_10_11_23)) 303 304(assert (! (not (= curr_2$0 null$0)) :named invariant_18_4_71)) 305 306(assert (! (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0) 307 :named invariant_18_4_72)) 308 309(assert (! (= sk_?X_32$0 (lseg_domain$0 next$0 lst$0 curr_2$0)) 310 :named invariant_18_4_73)) 311 312(assert (! (= sk_?X_30$0 FP_1$0) :named invariant_18_4_74)) 313 314(assert (! (= (as emptyset SetLoc) (intersection sk_?X_32$0 sk_?X_31$0)) 315 :named invariant_18_4_75)) 316 317(assert (! (not (= curr_3$0 null$0)) :named invariant_18_4_76)) 318 319(assert (! (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0) 320 :named invariant_18_4_77)) 321 322(assert (! (= sk_?X_29$0 323 (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0))) 324 :named invariant_18_4_78)) 325 326(assert (! (= sk_?X_27$0 (lseg_domain$0 next$0 lst_1$0 curr_3$0)) 327 :named invariant_18_4_79)) 328 329(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_80)) 330 331(assert (! (= Alloc$0 (union FP_2$0 Alloc$0)) 332 :named framecondition_of_remove_loop_18_4_18)) 333 334(assert (! (= tmp_2$0 (read$0 next$0 curr_3$0)) :named assign_27_4_2)) 335 336(assert (! (= lst_1$0 lst$0) :named framecondition_of_remove_loop_18_4_19)) 337 338(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_13_2_5)) 339 340(assert (! (or (Btwn$0 next$0 lst_1$0 curr_3$0 curr_3$0) 341 (not (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0))) 342 :named unnamed_26)) 343 344(assert (! (or (Btwn$0 next$0 lst$0 null$0 null$0) 345 (not (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0))) 346 :named unnamed_27)) 347 348(assert (! (or (Btwn$0 next$0 curr_2$0 null$0 null$0) 349 (not (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0))) 350 :named unnamed_28)) 351 352(assert (! (forall ((?u Loc) (?v Loc) (?z Loc)) 353 (and 354 (or 355 (Btwn$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) 356 ?z ?u ?v) 357 (not 358 (or 359 (and (Btwn$0 next$0 ?z ?u ?v) 360 (or (Btwn$0 next$0 ?z ?v curr_3$0) 361 (and (Btwn$0 next$0 ?z ?v ?v) 362 (not 363 (Btwn$0 next$0 ?z curr_3$0 364 curr_3$0))))) 365 (and (not (= curr_3$0 ?v)) 366 (or (Btwn$0 next$0 ?z curr_3$0 ?v) 367 (and 368 (Btwn$0 next$0 ?z curr_3$0 369 curr_3$0) 370 (not (Btwn$0 next$0 ?z ?v ?v)))) 371 (Btwn$0 next$0 ?z ?u curr_3$0) 372 (or 373 (Btwn$0 next$0 (read$0 next$0 tmp_2$0) 374 ?v curr_3$0) 375 (and 376 (Btwn$0 next$0 377 (read$0 next$0 tmp_2$0) ?v ?v) 378 (not 379 (Btwn$0 next$0 380 (read$0 next$0 tmp_2$0) 381 curr_3$0 curr_3$0))))) 382 (and (not (= curr_3$0 ?v)) 383 (or (Btwn$0 next$0 ?z curr_3$0 ?v) 384 (and 385 (Btwn$0 next$0 ?z curr_3$0 386 curr_3$0) 387 (not (Btwn$0 next$0 ?z ?v ?v)))) 388 (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u 389 ?v) 390 (or 391 (Btwn$0 next$0 (read$0 next$0 tmp_2$0) 392 ?v curr_3$0) 393 (and 394 (Btwn$0 next$0 395 (read$0 next$0 tmp_2$0) ?v ?v) 396 (not 397 (Btwn$0 next$0 398 (read$0 next$0 tmp_2$0) 399 curr_3$0 curr_3$0)))))))) 400 (or 401 (and (Btwn$0 next$0 ?z ?u ?v) 402 (or (Btwn$0 next$0 ?z ?v curr_3$0) 403 (and (Btwn$0 next$0 ?z ?v ?v) 404 (not (Btwn$0 next$0 ?z curr_3$0 curr_3$0))))) 405 (and (not (= curr_3$0 ?v)) 406 (or (Btwn$0 next$0 ?z curr_3$0 ?v) 407 (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0) 408 (not (Btwn$0 next$0 ?z ?v ?v)))) 409 (Btwn$0 next$0 ?z ?u curr_3$0) 410 (or 411 (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v 412 curr_3$0) 413 (and 414 (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v 415 ?v) 416 (not 417 (Btwn$0 next$0 (read$0 next$0 tmp_2$0) 418 curr_3$0 curr_3$0))))) 419 (and (not (= curr_3$0 ?v)) 420 (or (Btwn$0 next$0 ?z curr_3$0 ?v) 421 (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0) 422 (not (Btwn$0 next$0 ?z ?v ?v)))) 423 (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u ?v) 424 (or 425 (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v 426 curr_3$0) 427 (and 428 (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v 429 ?v) 430 (not 431 (Btwn$0 next$0 (read$0 next$0 tmp_2$0) 432 curr_3$0 curr_3$0))))) 433 (not 434 (Btwn$0 435 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) 436 ?z ?u ?v))))) 437 :named btwn_write)) 438 439(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_5)) 440 441(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y))) 442 :named btwn_sndw_5)) 443 444(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) 445 (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z)) 446 (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y))) 447 :named btwn_ord1_5)) 448 449(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) 450 (or (not (Btwn$0 next$0 ?x ?y ?z)) 451 (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z)))) 452 :named btwn_ord2_5)) 453 454(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) 455 (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z)) 456 (Btwn$0 next$0 ?x ?z ?z))) 457 :named btwn_trn1_5)) 458 459(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) 460 (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z)) 461 (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z)))) 462 :named btwn_trn2_5)) 463 464(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) 465 (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y)) 466 (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z)))) 467 :named btwn_trn3_5)) 468 469(check-sat) 470(exit) 471