← nischoy.ai

sudo Verification

SMT2 formal verification of security-critical code paths

ALL VERIFIED

Overall

Properties Checked

Verified

Failed

UID Bounds Validation (0-65534)

🌳 tree-sitter (partial) VERIFIED

Function: sudo_check_suid · Z3 solved in 0.1ms

UID must be 0-65534. From sudo_check_suid() in sudo.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun uid () Int)
(assert
 (<= uid 65534))
(assert
 (>= uid 0))
(assert
 (or (< uid 0) (> uid 65534)))
(check-sat)

GID Bounds Validation (0-65534)

🌳 tree-sitter (partial) VERIFIED

Function: sudo_check_suid · Z3 solved in 0.0ms

GID must be 0-65534. From sudo_check_suid() related validation.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun gid () Int)
(assert
 (<= gid 65534))
(assert
 (>= gid 0))
(assert
 (or (< gid 0) (> gid 65534)))
(check-sat)

Environment Variable Count Bounds (0-1024)

🌳 tree-sitter (partial) VERIFIED

Function: rebuild_env · Z3 solved in 0.0ms

Environment variable count bounded to prevent memory exhaustion.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun env_count () Int)
(assert
 (<= env_count 1024))
(assert
 (>= env_count 0))
(assert
 (or (< env_count 0) (> env_count 1024)))
(check-sat)

Argument Count Bounds (1-4096)

🌳 tree-sitter (partial) VERIFIED

Function: parse_args · Z3 solved in 0.0ms

Argument count bounded. From parse_args() in parse_args.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun argc () Int)
(assert
 (<= argc 4096))
(assert
 (>= argc 1))
(assert
 (or (< argc 1) (> argc 4096)))
(check-sat)

Close-From FD Bounds (3-INT_MAX)

🌳 tree-sitter (partial) VERIFIED

Function: parse_args · Z3 solved in 0.0ms

-C/--close-from value must be >=3 and fit in signed int. From parse_args() in parse_args.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun closefrom () Int)
(assert
 (<= closefrom 2147483647))
(assert
 (>= closefrom 3))
(assert
 (or (< closefrom 3) (> closefrom 2147483647)))
(check-sat)

Prompt Input Mode Flags Allowed Set (TGP_BELL/ASKPASS/STDIN)

🌳 tree-sitter VERIFIED

Function: parse_args · Z3 solved in 0.0ms

tgetpass_flags must be within known prompt bit combinations (0,1,2,3,4,5) in parse_args().

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun tgetpass_flags () Int)
(assert
 (let (($x24 (= tgetpass_flags 5)))
 (let (($x13 (= tgetpass_flags 4)))
 (let (($x34 (= tgetpass_flags 3)))
 (let (($x29 (= tgetpass_flags 2)))
 (let (($x12 (= tgetpass_flags 1)))
 (let (($x23 (= tgetpass_flags 0)))
 (or $x23 $x12 $x29 $x34 $x13 $x24))))))))
(assert
 (let (($x24 (= tgetpass_flags 5)))
(let (($x13 (= tgetpass_flags 4)))
(let (($x34 (= tgetpass_flags 3)))
(let (($x29 (= tgetpass_flags 2)))
(let (($x12 (= tgetpass_flags 1)))
(let (($x23 (= tgetpass_flags 0)))
(let (($x14 (or $x23 $x12 $x29 $x34 $x13 $x24)))
(not $x14)))))))))
(check-sat)

Prompt Input Mode Flags Non-Conflict (-A vs -S)

🌳 tree-sitter VERIFIED

Function: parse_args · Z3 solved in 180.0ms

-A (askpass) and -S (stdin) must not be set together in tgetpass_flags. From parse_args() in parse_args.c.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun tgetpass_flags () Int)
(assert
 (let (($x103 (= tgetpass_flags 61)))
 (let (($x101 (= tgetpass_flags 60)))
 (let (($x99 (= tgetpass_flags 59)))
 (let (($x97 (= tgetpass_flags 58)))
 (let (($x95 (= tgetpass_flags 57)))
 (let (($x93 (= tgetpass_flags 56)))
 (let (($x91 (= tgetpass_flags 53)))
 (let (($x89 (= tgetpass_flags 52)))
 (let (($x87 (= tgetpass_flags 51)))
 (let (($x85 (= tgetpass_flags 50)))
 (let (($x83 (= tgetpass_flags 49)))
 (let (($x81 (= tgetpass_flags 48)))
 (let (($x79 (= tgetpass_flags 45)))
 (let (($x77 (= tgetpass_flags 44)))
 (let (($x75 (= tgetpass_flags 43)))
 (let (($x73 (= tgetpass_flags 42)))
 (let (($x71 (= tgetpass_flags 41)))
 (let (($x69 (= tgetpass_flags 40)))
 (let (($x67 (= tgetpass_flags 37)))
 (let (($x65 (= tgetpass_flags 36)))
 (let (($x63 (= tgetpass_flags 35)))
 (let (($x61 (= tgetpass_flags 34)))
 (let (($x59 (= tgetpass_flags 33)))
 (let (($x57 (= tgetpass_flags 32)))
 (let (($x55 (= tgetpass_flags 29)))
 (let (($x53 (= tgetpass_flags 28)))
 (let (($x51 (= tgetpass_flags 27)))
 (let (($x49 (= tgetpass_flags 26)))
 (let (($x47 (= tgetpass_flags 25)))
 (let (($x45 (= tgetpass_flags 24)))
 (let (($x43 (= tgetpass_flags 21)))
 (let (($x41 (= tgetpass_flags 20)))
 (let (($x39 (= tgetpass_flags 19)))
 (let (($x21 (= tgetpass_flags 18)))
 (let (($x19 (= tgetpass_flags 17)))
 (let (($x15 (= tgetpass_flags 16)))
 (let (($x8 (= tgetpass_flags 13)))
 (let (($x33 (= tgetpass_flags 12)))
 (let (($x35 (= tgetpass_flags 11)))
 (let (($x37 (= tgetpass_flags 10)))
 (let (($x9 (= tgetpass_flags 9)))
 (let (($x38 (= tgetpass_flags 8)))
 (let (($x24 (= tgetpass_flags 5)))
 (let (($x13 (= tgetpass_flags 4)))
 (let (($x34 (= tgetpass_flags 3)))
 (let (($x29 (= tgetpass_flags 2)))
 (let (($x12 (= tgetpass_flags 1)))
 (let (($x23 (= tgetpass_flags 0)))
 (or $x23 $x12 $x29 $x34 $x13 $x24 $x38 $x9 $x37 $x35 $x33 $x8 $x15 $x19 $x21 $x39 $x41 $x43 $x45 $x47 $x49 $x51 $x53 $x55 $x57 $x59 $x61 $x63 $x65 $x67 $x69 $x71 $x73 $x75 $x77 $x79 $x81 $x83 $x85 $x87 $x89 $x91 $x93 $x95 $x97 $x99 $x101 $x103))))))))))))))))))))))))))))))))))))))))))))))))))
(assert
 (and (and (distinct (_ bv0 32) (bvand ((_ int_to_bv 32) tgetpass_flags) (_ bv2 32))) true) (and (distinct (_ bv0 32) (bvand ((_ int_to_bv 32) tgetpass_flags) (_ bv4 32))) true)))
(check-sat)

Mode Selector Allowed Set (MODE_RUN/EDIT/VALIDATE/INVALIDATE/KILL/VERSION/HELP/LIST/CHECK)

🌳 tree-sitter VERIFIED

Function: parse_args · Z3 solved in 0.0ms

Final command mode selector must be a defined MODE_* value to avoid undefined dispatcher state in parse_args().

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun mode () Int)
(assert
 (let (($x13 (= mode 256)))
 (let (($x29 (= mode 128)))
 (let (($x130 (= mode 64)))
 (let (($x128 (= mode 32)))
 (let (($x126 (= mode 16)))
 (let (($x123 (= mode 8)))
 (let (($x122 (= mode 4)))
 (let (($x5 (= mode 2)))
 (let (($x125 (= mode 1)))
 (or $x125 $x5 $x122 $x123 $x126 $x128 $x130 $x29 $x13)))))))))))
(assert
 (let (($x13 (= mode 256)))
(let (($x29 (= mode 128)))
(let (($x130 (= mode 64)))
(let (($x128 (= mode 32)))
(let (($x126 (= mode 16)))
(let (($x123 (= mode 8)))
(let (($x122 (= mode 4)))
(let (($x5 (= mode 2)))
(let (($x125 (= mode 1)))
(let (($x24 (or $x125 $x5 $x122 $x123 $x126 $x128 $x130 $x29 $x13)))
(not $x24))))))))))))
(check-sat)

Mode Selector Single-Bit Invariant

🌳 tree-sitter VERIFIED

Function: parse_args · Z3 solved in 101.6ms

Mode selector must encode exactly one dispatcher bit (no mixed-mode bitsets) to keep command dispatch deterministic.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun mode () Int)
(assert
 (let (($x13 (= mode 256)))
 (let (($x29 (= mode 128)))
 (let (($x130 (= mode 64)))
 (let (($x128 (= mode 32)))
 (let (($x126 (= mode 16)))
 (let (($x123 (= mode 8)))
 (let (($x122 (= mode 4)))
 (let (($x5 (= mode 2)))
 (let (($x125 (= mode 1)))
 (or $x125 $x5 $x122 $x123 $x126 $x128 $x130 $x29 $x13)))))))))))
(assert
 (let (($x49 (and (distinct (_ bv0 32) (bvand ((_ int_to_bv 32) mode) (bvsub ((_ int_to_bv 32) mode) (_ bv1 32)))) true)))
(let (($x44 (= mode 0)))
(or $x44 $x49))))
(check-sat)

Shell Mode Flags Non-Conflict (-s vs -i)

🌳 tree-sitter VERIFIED

Function: parse_args · Z3 solved in 5199.9ms

MODE_SHELL and MODE_LOGIN_SHELL must never be set together in option flags (parse_args() enforces mutual exclusion).

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun flags () Int)
(assert
 (let (($x787 (= flags 33357824)))
 (let (($x785 (= flags 33292288)))
 (let (($x784 (= flags 33226752)))
 (let (($x781 (= flags 33161216)))
 (let (($x779 (= flags 33095680)))
 (let (($x777 (= flags 33030144)))
 (let (($x775 (= flags 32833536)))
 (let (($x773 (= flags 32768000)))
 (let (($x771 (= flags 32702464)))
 (let (($x770 (= flags 32636928)))
 (let (($x767 (= flags 32571392)))
 (let (($x764 (= flags 32505856)))
 (let (($x763 (= flags 32309248)))
 (let (($x761 (= flags 32243712)))
 (let (($x693 (= flags 32178176)))
 (let (($x759 (= flags 32112640)))
 (let (($x690 (= flags 32047104)))
 (let (($x756 (= flags 31981568)))
 (let (($x755 (= flags 31784960)))
 (let (($x688 (= flags 31719424)))
 (let (($x752 (= flags 31653888)))
 (let (($x751 (= flags 31588352)))
 (let (($x686 (= flags 31522816)))
 (let (($x748 (= flags 31457280)))
 (let (($x747 (= flags 31260672)))
 (let (($x684 (= flags 31195136)))
 (let (($x744 (= flags 31129600)))
 (let (($x743 (= flags 31064064)))
 (let (($x682 (= flags 30998528)))
 (let (($x740 (= flags 30932992)))
 (let (($x739 (= flags 30736384)))
 (let (($x680 (= flags 30670848)))
 (let (($x736 (= flags 30605312)))
 (let (($x735 (= flags 30539776)))
 (let (($x678 (= flags 30474240)))
 (let (($x732 (= flags 30408704)))
 (let (($x731 (= flags 30212096)))
 (let (($x676 (= flags 30146560)))
 (let (($x728 (= flags 30081024)))
 (let (($x727 (= flags 30015488)))
 (let (($x674 (= flags 29949952)))
 (let (($x723 (= flags 29884416)))
 (let (($x722 (= flags 29687808)))
 (let (($x672 (= flags 29622272)))
 (let (($x719 (= flags 29556736)))
 (let (($x718 (= flags 29491200)))
 (let (($x670 (= flags 29425664)))
 (let (($x715 (= flags 29360128)))
 (let (($x714 (= flags 29163520)))
 (let (($x668 (= flags 29097984)))
 (let (($x711 (= flags 29032448)))
 (let (($x710 (= flags 28966912)))
 (let (($x666 (= flags 28901376)))
 (let (($x706 (= flags 28835840)))
 (let (($x705 (= flags 28639232)))
 (let (($x664 (= flags 28573696)))
 (let (($x702 (= flags 28508160)))
 (let (($x701 (= flags 28442624)))
 (let (($x662 (= flags 28377088)))
 (let (($x698 (= flags 28311552)))
 (let (($x697 (= flags 28114944)))
 (let (($x660 (= flags 28049408)))
 (let (($x694 (= flags 27983872)))
 (let (($x659 (= flags 27918336)))
 (let (($x657 (= flags 27852800)))
 (let (($x654 (= flags 27787264)))
 (let (($x590 (= flags 27590656)))
 (let (($x653 (= flags 27525120)))
 (let (($x650 (= flags 27459584)))
 (let (($x649 (= flags 27394048)))
 (let (($x648 (= flags 27328512)))
 (let (($x584 (= flags 27262976)))
 (let (($x647 (= flags 27066368)))
 (let (($x583 (= flags 27000832)))
 (let (($x642 (= flags 26935296)))
 (let (($x641 (= flags 26869760)))
 (let (($x640 (= flags 26804224)))
 (let (($x580 (= flags 26738688)))
 (let (($x639 (= flags 26542080)))
 (let (($x579 (= flags 26476544)))
 (let (($x634 (= flags 26411008)))
 (let (($x633 (= flags 26345472)))
 (let (($x632 (= flags 26279936)))
 (let (($x576 (= flags 26214400)))
 (let (($x631 (= flags 26017792)))
 (let (($x575 (= flags 25952256)))
 (let (($x626 (= flags 25886720)))
 (let (($x625 (= flags 25821184)))
 (let (($x624 (= flags 25755648)))
 (let (($x572 (= flags 25690112)))
 (let (($x623 (= flags 25493504)))
 (let (($x571 (= flags 25427968)))
 (let (($x618 (= flags 25362432)))
 (let (($x617 (= flags 25296896)))
 (let (($x616 (= flags 25231360)))
 (let (($x568 (= flags 25165824)))
 (let (($x615 (= flags 24969216)))
 (let (($x567 (= flags 24903680)))
 (let (($x610 (= flags 24838144)))
 (let (($x609 (= flags 24772608)))
 (let (($x608 (= flags 24707072)))
 (let (($x564 (= flags 24641536)))
 (let (($x607 (= flags 24444928)))
 (let (($x563 (= flags 24379392)))
 (let (($x602 (= flags 24313856)))
 (let (($x601 (= flags 24248320)))
 (let (($x600 (= flags 24182784)))
 (let (($x560 (= flags 24117248)))
 (let (($x599 (= flags 23920640)))
 (let (($x559 (= flags 23855104)))
 (let (($x594 (= flags 23789568)))
 (let (($x593 (= flags 23724032)))
 (let (($x592 (= flags 23658496)))
 (let (($x556 (= flags 23592960)))
 (let (($x557 (= flags 23396352)))
 (let (($x552 (= flags 23330816)))
 (let (($x550 (= flags 23265280)))
 (let (($x548 (= flags 23199744)))
 (let (($x547 (= flags 23134208)))
 (let (($x543 (= flags 23068672)))
 (let (($x545 (= flags 22872064)))
 (let (($x541 (= flags 22806528)))
 (let (($x537 (= flags 22740992)))
 (let (($x533 (= flags 22675456)))
 (let (($x532 (= flags 22609920)))
 (let (($x529 (= flags 22544384)))
 (let (($x530 (= flags 22347776)))
 (let (($x524 (= flags 22282240)))
 (let (($x523 (= flags 22216704)))
 (let (($x521 (= flags 22151168)))
 (let (($x520 (= flags 22085632)))
 (let (($x517 (= flags 22020096)))
 (let (($x518 (= flags 21823488)))
 (let (($x512 (= flags 21757952)))
 (let (($x511 (= flags 21692416)))
 (let (($x509 (= flags 21626880)))
 (let (($x508 (= flags 21561344)))
 (let (($x505 (= flags 21495808)))
 (let (($x506 (= flags 21299200)))
 (let (($x500 (= flags 21233664)))
 (let (($x499 (= flags 21168128)))
 (let (($x497 (= flags 21102592)))
 (let (($x496 (= flags 21037056)))
 (let (($x493 (= flags 20971520)))
 (let (($x494 (= flags 20774912)))
 (let (($x488 (= flags 20709376)))
 (let (($x487 (= flags 20643840)))
 (let (($x485 (= flags 20578304)))
 (let (($x484 (= flags 20512768)))
 (let (($x481 (= flags 20447232)))
 (let (($x482 (= flags 20250624)))
 (let (($x476 (= flags 20185088)))
 (let (($x475 (= flags 20119552)))
 (let (($x473 (= flags 20054016)))
 (let (($x472 (= flags 19988480)))
 (let (($x469 (= flags 19922944)))
 (let (($x470 (= flags 19726336)))
 (let (($x464 (= flags 19660800)))
 (let (($x463 (= flags 19595264)))
 (let (($x461 (= flags 19529728)))
 (let (($x460 (= flags 19464192)))
 (let (($x457 (= flags 19398656)))
 (let (($x458 (= flags 19202048)))
 (let (($x452 (= flags 19136512)))
 (let (($x451 (= flags 19070976)))
 (let (($x449 (= flags 19005440)))
 (let (($x448 (= flags 18939904)))
 (let (($x445 (= flags 18874368)))
 (let (($x446 (= flags 18677760)))
 (let (($x440 (= flags 18612224)))
 (let (($x439 (= flags 18546688)))
 (let (($x437 (= flags 18481152)))
 (let (($x436 (= flags 18415616)))
 (let (($x433 (= flags 18350080)))
 (let (($x434 (= flags 18153472)))
 (let (($x428 (= flags 18087936)))
 (let (($x427 (= flags 18022400)))
 (let (($x425 (= flags 17956864)))
 (let (($x424 (= flags 17891328)))
 (let (($x421 (= flags 17825792)))
 (let (($x422 (= flags 17629184)))
 (let (($x416 (= flags 17563648)))
 (let (($x415 (= flags 17498112)))
 (let (($x413 (= flags 17432576)))
 (let (($x412 (= flags 17367040)))
 (let (($x409 (= flags 17301504)))
 (let (($x410 (= flags 17104896)))
 (let (($x404 (= flags 17039360)))
 (let (($x403 (= flags 16973824)))
 (let (($x401 (= flags 16908288)))
 (let (($x400 (= flags 16842752)))
 (let (($x397 (= flags 16777216)))
 (let (($x398 (= flags 16580608)))
 (let (($x392 (= flags 16515072)))
 (let (($x391 (= flags 16449536)))
 (let (($x389 (= flags 16384000)))
 (let (($x388 (= flags 16318464)))
 (let (($x385 (= flags 16252928)))
 (let (($x386 (= flags 16056320)))
 (let (($x380 (= flags 15990784)))
 (let (($x379 (= flags 15925248)))
 (let (($x377 (= flags 15859712)))
 (let (($x376 (= flags 15794176)))
 (let (($x373 (= flags 15728640)))
 (let (($x374 (= flags 15532032)))
 (let (($x368 (= flags 15466496)))
 (let (($x367 (= flags 15400960)))
 (let (($x362 (= flags 15335424)))
 (let (($x364 (= flags 15269888)))
 (let (($x361 (= flags 15204352)))
 (let (($x360 (= flags 15007744)))
 (let (($x356 (= flags 14942208)))
 (let (($x355 (= flags 14876672)))
 (let (($x354 (= flags 14811136)))
 (let (($x350 (= flags 14745600)))
 (let (($x352 (= flags 14680064)))
 (let (($x348 (= flags 14483456)))
 (let (($x344 (= flags 14417920)))
 (let (($x340 (= flags 14352384)))
 (let (($x342 (= flags 14286848)))
 (let (($x338 (= flags 14221312)))
 (let (($x334 (= flags 14155776)))
 (let (($x336 (= flags 13959168)))
 (let (($x332 (= flags 13893632)))
 (let (($x335 (= flags 13828096)))
 (let (($x328 (= flags 13762560)))
 (let (($x330 (= flags 13697024)))
 (let (($x325 (= flags 13631488)))
 (let (($x321 (= flags 13434880)))
 (let (($x320 (= flags 13369344)))
 (let (($x317 (= flags 13303808)))
 (let (($x319 (= flags 13238272)))
 (let (($x314 (= flags 13172736)))
 (let (($x189 (= flags 13107200)))
 (let (($x288 (= flags 12910592)))
 (let (($x284 (= flags 12845056)))
 (let (($x286 (= flags 12779520)))
 (let (($x290 (= flags 12713984)))
 (let (($x292 (= flags 12648448)))
 (let (($x294 (= flags 12582912)))
 (let (($x295 (= flags 12386304)))
 (let (($x297 (= flags 12320768)))
 (let (($x298 (= flags 12255232)))
 (let (($x305 (= flags 12189696)))
 (let (($x304 (= flags 12124160)))
 (let (($x307 (= flags 12058624)))
 (let (($x312 (= flags 11862016)))
 (let (($x309 (= flags 11796480)))
 (let (($x282 (= flags 11730944)))
 (let (($x252 (= flags 11665408)))
 (let (($x192 (= flags 11599872)))
 (let (($x280 (= flags 11534336)))
 (let (($x248 (= flags 11337728)))
 (let (($x196 (= flags 11272192)))
 (let (($x278 (= flags 11206656)))
 (let (($x247 (= flags 11141120)))
 (let (($x197 (= flags 11075584)))
 (let (($x277 (= flags 11010048)))
 (let (($x245 (= flags 10813440)))
 (let (($x199 (= flags 10747904)))
 (let (($x273 (= flags 10682368)))
 (let (($x243 (= flags 10616832)))
 (let (($x201 (= flags 10551296)))
 (let (($x275 (= flags 10485760)))
 (let (($x238 (= flags 10289152)))
 (let (($x202 (= flags 10223616)))
 (let (($x270 (= flags 10158080)))
 (let (($x240 (= flags 10092544)))
 (let (($x206 (= flags 10027008)))
 (let (($x268 (= flags 9961472)))
 (let (($x236 (= flags 9764864)))
 (let (($x204 (= flags 9699328)))
 (let (($x266 (= flags 9633792)))
 (let (($x235 (= flags 9568256)))
 (let (($x209 (= flags 9502720)))
 (let (($x265 (= flags 9437184)))
 (let (($x233 (= flags 9240576)))
 (let (($x211 (= flags 9175040)))
 (let (($x261 (= flags 9109504)))
 (let (($x231 (= flags 9043968)))
 (let (($x216 (= flags 8978432)))
 (let (($x263 (= flags 8912896)))
 (let (($x226 (= flags 8716288)))
 (let (($x214 (= flags 8650752)))
 (let (($x258 (= flags 8585216)))
 (let (($x228 (= flags 8519680)))
 (let (($x218 (= flags 8454144)))
 (let (($x256 (= flags 8388608)))
 (let (($x224 (= flags 8192000)))
 (let (($x219 (= flags 8126464)))
 (let (($x254 (= flags 8060928)))
 (let (($x223 (= flags 7995392)))
 (let (($x221 (= flags 7929856)))
 (let (($x253 (= flags 7864320)))
 (let (($x194 (= flags 7667712)))
 (let (($x188 (= flags 7602176)))
 (let (($x187 (= flags 7536640)))
 (let (($x156 (= flags 7471104)))
 (let (($x154 (= flags 7405568)))
 (let (($x153 (= flags 7340032)))
 (let (($x168 (= flags 7143424)))
 (let (($x166 (= flags 7077888)))
 (let (($x164 (= flags 7012352)))
 (let (($x181 (= flags 6946816)))
 (let (($x180 (= flags 6881280)))
 (let (($x179 (= flags 6815744)))
 (let (($x143 (= flags 6619136)))
 (let (($x142 (= flags 6553600)))
 (let (($x172 (= flags 6488064)))
 (let (($x169 (= flags 6422528)))
 (let (($x165 (= flags 6356992)))
 (let (($x167 (= flags 6291456)))
 (let (($x161 (= flags 6094848)))
 (let (($x160 (= flags 6029312)))
 (let (($x159 (= flags 5963776)))
 (let (($x149 (= flags 5898240)))
 (let (($x148 (= flags 5832704)))
 (let (($x147 (= flags 5767168)))
 (let (($x131 (= flags 5570560)))
 (let (($x141 (= flags 5505024)))
 (let (($x136 (= flags 5439488)))
 (let (($x157 (= flags 5373952)))
 (let (($x135 (= flags 5308416)))
 (let (($x186 (= flags 5242880)))
 (let (($x92 (= flags 5046272)))
 (let (($x93 (= flags 4980736)))
 (let (($x94 (= flags 4915200)))
 (let (($x98 (= flags 4849664)))
 (let (($x99 (= flags 4784128)))
 (let (($x100 (= flags 4718592)))
 (let (($x104 (= flags 4521984)))
 (let (($x105 (= flags 4456448)))
 (let (($x534 (= flags 4390912)))
 (let (($x112 (= flags 4325376)))
 (let (($x121 (= flags 4259840)))
 (let (($x106 (= flags 4194304)))
 (let (($x117 (= flags 3997696)))
 (let (($x116 (= flags 3932160)))
 (let (($x115 (= flags 3866624)))
 (let (($x110 (= flags 3801088)))
 (let (($x91 (= flags 3735552)))
 (let (($x89 (= flags 3670016)))
 (let (($x87 (= flags 3473408)))
 (let (($x85 (= flags 3407872)))
 (let (($x83 (= flags 3342336)))
 (let (($x81 (= flags 3276800)))
 (let (($x79 (= flags 3211264)))
 (let (($x77 (= flags 3145728)))
 (let (($x75 (= flags 2949120)))
 (let (($x73 (= flags 2883584)))
 (let (($x71 (= flags 2818048)))
 (let (($x69 (= flags 2752512)))
 (let (($x67 (= flags 2686976)))
 (let (($x65 (= flags 2621440)))
 (let (($x53 (= flags 2424832)))
 (let (($x60 (= flags 2359296)))
 (let (($x63 (= flags 2293760)))
 (let (($x61 (= flags 2228224)))
 (let (($x57 (= flags 2162688)))
 (let (($x54 (= flags 2097152)))
 (let (($x55 (= flags 1900544)))
 (let (($x15 (= flags 1835008)))
 (let (($x9 (= flags 1769472)))
 (let (($x39 (= flags 1703936)))
 (let (($x20 (= flags 1638400)))
 (let (($x26 (= flags 1572864)))
 (let (($x33 (= flags 1376256)))
 (let (($x35 (= flags 1310720)))
 (let (($x22 (= flags 1245184)))
 (let (($x825 (= flags 1179648)))
 (let (($x652 (= flags 1114112)))
 (let (($x587 (= flags 1048576)))
 (let (($x24 (= flags 851968)))
 (let (($x34 (= flags 786432)))
 (let (($x12 (= flags 720896)))
 (let (($x129 (= flags 655360)))
 (let (($x127 (= flags 589824)))
 (let (($x124 (= flags 524288)))
 (let (($x122 (= flags 327680)))
 (let (($x50 (= flags 262144)))
 (let (($x47 (= flags 196608)))
 (let (($x45 (= flags 131072)))
 (let (($x48 (= flags 65536)))
 (let (($x23 (= flags 0)))
 (or $x23 $x48 $x45 $x47 $x50 $x122 $x124 $x127 $x129 $x12 $x34 $x24 $x587 $x652 $x825 $x22 $x35 $x33 $x26 $x20 $x39 $x9 $x15 $x55 $x54 $x57 $x61 $x63 $x60 $x53 $x65 $x67 $x69 $x71 $x73 $x75 $x77 $x79 $x81 $x83 $x85 $x87 $x89 $x91 $x110 $x115 $x116 $x117 $x106 $x121 $x112 $x534 $x105 $x104 $x100 $x99 $x98 $x94 $x93 $x92 $x186 $x135 $x157 $x136 $x141 $x131 $x147 $x148 $x149 $x159 $x160 $x161 $x167 $x165 $x169 $x172 $x142 $x143 $x179 $x180 $x181 $x164 $x166 $x168 $x153 $x154 $x156 $x187 $x188 $x194 $x253 $x221 $x223 $x254 $x219 $x224 $x256 $x218 $x228 $x258 $x214 $x226 $x263 $x216 $x231 $x261 $x211 $x233 $x265 $x209 $x235 $x266 $x204 $x236 $x268 $x206 $x240 $x270 $x202 $x238 $x275 $x201 $x243 $x273 $x199 $x245 $x277 $x197 $x247 $x278 $x196 $x248 $x280 $x192 $x252 $x282 $x309 $x312 $x307 $x304 $x305 $x298 $x297 $x295 $x294 $x292 $x290 $x286 $x284 $x288 $x189 $x314 $x319 $x317 $x320 $x321 $x325 $x330 $x328 $x335 $x332 $x336 $x334 $x338 $x342 $x340 $x344 $x348 $x352 $x350 $x354 $x355 $x356 $x360 $x361 $x364 $x362 $x367 $x368 $x374 $x373 $x376 $x377 $x379 $x380 $x386 $x385 $x388 $x389 $x391 $x392 $x398 $x397 $x400 $x401 $x403 $x404 $x410 $x409 $x412 $x413 $x415 $x416 $x422 $x421 $x424 $x425 $x427 $x428 $x434 $x433 $x436 $x437 $x439 $x440 $x446 $x445 $x448 $x449 $x451 $x452 $x458 $x457 $x460 $x461 $x463 $x464 $x470 $x469 $x472 $x473 $x475 $x476 $x482 $x481 $x484 $x485 $x487 $x488 $x494 $x493 $x496 $x497 $x499 $x500 $x506 $x505 $x508 $x509 $x511 $x512 $x518 $x517 $x520 $x521 $x523 $x524 $x530 $x529 $x532 $x533 $x537 $x541 $x545 $x543 $x547 $x548 $x550 $x552 $x557 $x556 $x592 $x593 $x594 $x559 $x599 $x560 $x600 $x601 $x602 $x563 $x607 $x564 $x608 $x609 $x610 $x567 $x615 $x568 $x616 $x617 $x618 $x571 $x623 $x572 $x624 $x625 $x626 $x575 $x631 $x576 $x632 $x633 $x634 $x579 $x639 $x580 $x640 $x641 $x642 $x583 $x647 $x584 $x648 $x649 $x650 $x653 $x590 $x654 $x657 $x659 $x694 $x660 $x697 $x698 $x662 $x701 $x702 $x664 $x705 $x706 $x666 $x710 $x711 $x668 $x714 $x715 $x670 $x718 $x719 $x672 $x722 $x723 $x674 $x727 $x728 $x676 $x731 $x732 $x678 $x735 $x736 $x680 $x739 $x740 $x682 $x743 $x744 $x684 $x747 $x748 $x686 $x751 $x752 $x688 $x755 $x756 $x690 $x759 $x693 $x761 $x763 $x764 $x767 $x770 $x771 $x773 $x775 $x777 $x779 $x781 $x784 $x785 $x787))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert
 (let (($x1062 (= flags 33488896)))
(let (($x1060 (= flags 33423360)))
(let (($x1058 (= flags 32964608)))
(let (($x1056 (= flags 32899072)))
(let (($x1054 (= flags 32440320)))
(let (($x1052 (= flags 32374784)))
(let (($x1050 (= flags 31916032)))
(let (($x1048 (= flags 31850496)))
(let (($x1046 (= flags 31391744)))
(let (($x1044 (= flags 31326208)))
(let (($x1042 (= flags 30867456)))
(let (($x1040 (= flags 30801920)))
(let (($x1038 (= flags 30343168)))
(let (($x1036 (= flags 30277632)))
(let (($x1034 (= flags 29818880)))
(let (($x1032 (= flags 29753344)))
(let (($x1030 (= flags 29294592)))
(let (($x1028 (= flags 29229056)))
(let (($x1026 (= flags 28770304)))
(let (($x1024 (= flags 28704768)))
(let (($x1022 (= flags 28246016)))
(let (($x1020 (= flags 28180480)))
(let (($x1018 (= flags 27721728)))
(let (($x1016 (= flags 27656192)))
(let (($x1014 (= flags 27197440)))
(let (($x1012 (= flags 27131904)))
(let (($x1010 (= flags 26673152)))
(let (($x1008 (= flags 26607616)))
(let (($x1006 (= flags 26148864)))
(let (($x1004 (= flags 26083328)))
(let (($x1002 (= flags 25624576)))
(let (($x1000 (= flags 25559040)))
(let (($x998 (= flags 25100288)))
(let (($x996 (= flags 25034752)))
(let (($x994 (= flags 24576000)))
(let (($x992 (= flags 24510464)))
(let (($x990 (= flags 24051712)))
(let (($x988 (= flags 23986176)))
(let (($x986 (= flags 23527424)))
(let (($x984 (= flags 23461888)))
(let (($x982 (= flags 23003136)))
(let (($x980 (= flags 22937600)))
(let (($x978 (= flags 22478848)))
(let (($x976 (= flags 22413312)))
(let (($x974 (= flags 21954560)))
(let (($x972 (= flags 21889024)))
(let (($x970 (= flags 21430272)))
(let (($x968 (= flags 21364736)))
(let (($x966 (= flags 20905984)))
(let (($x964 (= flags 20840448)))
(let (($x962 (= flags 20381696)))
(let (($x960 (= flags 20316160)))
(let (($x958 (= flags 19857408)))
(let (($x956 (= flags 19791872)))
(let (($x954 (= flags 19333120)))
(let (($x952 (= flags 19267584)))
(let (($x950 (= flags 18808832)))
(let (($x948 (= flags 18743296)))
(let (($x946 (= flags 18284544)))
(let (($x944 (= flags 18219008)))
(let (($x942 (= flags 17760256)))
(let (($x940 (= flags 17694720)))
(let (($x938 (= flags 17235968)))
(let (($x936 (= flags 17170432)))
(let (($x934 (= flags 16711680)))
(let (($x932 (= flags 16646144)))
(let (($x930 (= flags 16187392)))
(let (($x928 (= flags 16121856)))
(let (($x926 (= flags 15663104)))
(let (($x924 (= flags 15597568)))
(let (($x922 (= flags 15138816)))
(let (($x920 (= flags 15073280)))
(let (($x918 (= flags 14614528)))
(let (($x916 (= flags 14548992)))
(let (($x914 (= flags 14090240)))
(let (($x912 (= flags 14024704)))
(let (($x910 (= flags 13565952)))
(let (($x908 (= flags 13500416)))
(let (($x906 (= flags 13041664)))
(let (($x904 (= flags 12976128)))
(let (($x902 (= flags 12517376)))
(let (($x900 (= flags 12451840)))
(let (($x898 (= flags 11993088)))
(let (($x896 (= flags 11927552)))
(let (($x894 (= flags 11468800)))
(let (($x892 (= flags 11403264)))
(let (($x890 (= flags 10944512)))
(let (($x888 (= flags 10878976)))
(let (($x886 (= flags 10420224)))
(let (($x884 (= flags 10354688)))
(let (($x882 (= flags 9895936)))
(let (($x880 (= flags 9830400)))
(let (($x878 (= flags 9371648)))
(let (($x876 (= flags 9306112)))
(let (($x874 (= flags 8847360)))
(let (($x872 (= flags 8781824)))
(let (($x870 (= flags 8323072)))
(let (($x868 (= flags 8257536)))
(let (($x866 (= flags 7798784)))
(let (($x864 (= flags 7733248)))
(let (($x862 (= flags 7274496)))
(let (($x860 (= flags 7208960)))
(let (($x858 (= flags 6750208)))
(let (($x856 (= flags 6684672)))
(let (($x854 (= flags 6225920)))
(let (($x852 (= flags 6160384)))
(let (($x850 (= flags 5701632)))
(let (($x848 (= flags 5636096)))
(let (($x846 (= flags 5177344)))
(let (($x844 (= flags 5111808)))
(let (($x842 (= flags 4653056)))
(let (($x841 (= flags 4587520)))
(let (($x838 (= flags 4128768)))
(let (($x836 (= flags 4063232)))
(let (($x834 (= flags 3604480)))
(let (($x832 (= flags 3538944)))
(let (($x830 (= flags 3080192)))
(let (($x828 (= flags 3014656)))
(let (($x826 (= flags 2555904)))
(let (($x823 (= flags 2490368)))
(let (($x822 (= flags 2031616)))
(let (($x819 (= flags 1966080)))
(let (($x817 (= flags 1507328)))
(let (($x815 (= flags 1441792)))
(let (($x813 (= flags 983040)))
(let (($x811 (= flags 917504)))
(let (($x809 (= flags 458752)))
(let (($x807 (= flags 393216)))
(or $x807 $x809 $x811 $x813 $x815 $x817 $x819 $x822 $x823 $x826 $x828 $x830 $x832 $x834 $x836 $x838 $x841 $x842 $x844 $x846 $x848 $x850 $x852 $x854 $x856 $x858 $x860 $x862 $x864 $x866 $x868 $x870 $x872 $x874 $x876 $x878 $x880 $x882 $x884 $x886 $x888 $x890 $x892 $x894 $x896 $x898 $x900 $x902 $x904 $x906 $x908 $x910 $x912 $x914 $x916 $x918 $x920 $x922 $x924 $x926 $x928 $x930 $x932 $x934 $x936 $x938 $x940 $x942 $x944 $x946 $x948 $x950 $x952 $x954 $x956 $x958 $x960 $x962 $x964 $x966 $x968 $x970 $x972 $x974 $x976 $x978 $x980 $x982 $x984 $x986 $x988 $x990 $x992 $x994 $x996 $x998 $x1000 $x1002 $x1004 $x1006 $x1008 $x1010 $x1012 $x1014 $x1016 $x1018 $x1020 $x1022 $x1024 $x1026 $x1028 $x1030 $x1032 $x1034 $x1036 $x1038 $x1040 $x1042 $x1044 $x1046 $x1048 $x1050 $x1052 $x1054 $x1056 $x1058 $x1060 $x1062))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

Login Shell Flag Implies Shell Flag

🌳 tree-sitter VERIFIED

Function: parse_args · Z3 solved in 4995.2ms

MODE_LOGIN_SHELL must imply MODE_SHELL in final option flags to preserve shell-mode consistency.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun flags () Int)
(assert
 (let (($x522 (= flags 33488896)))
 (let (($x514 (= flags 33423360)))
 (let (($x519 (= flags 33226752)))
 (let (($x516 (= flags 33161216)))
 (let (($x513 (= flags 33095680)))
 (let (($x515 (= flags 33030144)))
 (let (($x510 (= flags 32964608)))
 (let (($x502 (= flags 32899072)))
 (let (($x507 (= flags 32702464)))
 (let (($x504 (= flags 32636928)))
 (let (($x501 (= flags 32571392)))
 (let (($x503 (= flags 32505856)))
 (let (($x498 (= flags 32440320)))
 (let (($x490 (= flags 32374784)))
 (let (($x495 (= flags 32178176)))
 (let (($x492 (= flags 32112640)))
 (let (($x489 (= flags 32047104)))
 (let (($x491 (= flags 31981568)))
 (let (($x486 (= flags 31916032)))
 (let (($x478 (= flags 31850496)))
 (let (($x483 (= flags 31653888)))
 (let (($x480 (= flags 31588352)))
 (let (($x477 (= flags 31522816)))
 (let (($x479 (= flags 31457280)))
 (let (($x474 (= flags 31391744)))
 (let (($x466 (= flags 31326208)))
 (let (($x471 (= flags 31129600)))
 (let (($x468 (= flags 31064064)))
 (let (($x465 (= flags 30998528)))
 (let (($x467 (= flags 30932992)))
 (let (($x462 (= flags 30867456)))
 (let (($x454 (= flags 30801920)))
 (let (($x459 (= flags 30605312)))
 (let (($x456 (= flags 30539776)))
 (let (($x453 (= flags 30474240)))
 (let (($x455 (= flags 30408704)))
 (let (($x450 (= flags 30343168)))
 (let (($x442 (= flags 30277632)))
 (let (($x447 (= flags 30081024)))
 (let (($x444 (= flags 30015488)))
 (let (($x441 (= flags 29949952)))
 (let (($x443 (= flags 29884416)))
 (let (($x438 (= flags 29818880)))
 (let (($x430 (= flags 29753344)))
 (let (($x435 (= flags 29556736)))
 (let (($x432 (= flags 29491200)))
 (let (($x429 (= flags 29425664)))
 (let (($x431 (= flags 29360128)))
 (let (($x426 (= flags 29294592)))
 (let (($x418 (= flags 29229056)))
 (let (($x423 (= flags 29032448)))
 (let (($x420 (= flags 28966912)))
 (let (($x417 (= flags 28901376)))
 (let (($x419 (= flags 28835840)))
 (let (($x414 (= flags 28770304)))
 (let (($x406 (= flags 28704768)))
 (let (($x411 (= flags 28508160)))
 (let (($x408 (= flags 28442624)))
 (let (($x405 (= flags 28377088)))
 (let (($x407 (= flags 28311552)))
 (let (($x402 (= flags 28246016)))
 (let (($x394 (= flags 28180480)))
 (let (($x399 (= flags 27983872)))
 (let (($x396 (= flags 27918336)))
 (let (($x393 (= flags 27852800)))
 (let (($x395 (= flags 27787264)))
 (let (($x390 (= flags 27721728)))
 (let (($x382 (= flags 27656192)))
 (let (($x387 (= flags 27459584)))
 (let (($x384 (= flags 27394048)))
 (let (($x381 (= flags 27328512)))
 (let (($x383 (= flags 27262976)))
 (let (($x378 (= flags 27197440)))
 (let (($x370 (= flags 27131904)))
 (let (($x375 (= flags 26935296)))
 (let (($x372 (= flags 26869760)))
 (let (($x369 (= flags 26804224)))
 (let (($x371 (= flags 26738688)))
 (let (($x366 (= flags 26673152)))
 (let (($x365 (= flags 26607616)))
 (let (($x358 (= flags 26411008)))
 (let (($x363 (= flags 26345472)))
 (let (($x357 (= flags 26279936)))
 (let (($x359 (= flags 26214400)))
 (let (($x351 (= flags 26148864)))
 (let (($x353 (= flags 26083328)))
 (let (($x346 (= flags 25886720)))
 (let (($x349 (= flags 25821184)))
 (let (($x345 (= flags 25755648)))
 (let (($x347 (= flags 25690112)))
 (let (($x343 (= flags 25624576)))
 (let (($x339 (= flags 25559040)))
 (let (($x341 (= flags 25362432)))
 (let (($x337 (= flags 25296896)))
 (let (($x333 (= flags 25231360)))
 (let (($x329 (= flags 25165824)))
 (let (($x331 (= flags 25100288)))
 (let (($x327 (= flags 25034752)))
 (let (($x322 (= flags 24838144)))
 (let (($x324 (= flags 24772608)))
 (let (($x318 (= flags 24707072)))
 (let (($x323 (= flags 24641536)))
 (let (($x316 (= flags 24576000)))
 (let (($x315 (= flags 24510464)))
 (let (($x310 (= flags 24313856)))
 (let (($x283 (= flags 24248320)))
 (let (($x287 (= flags 24182784)))
 (let (($x289 (= flags 24117248)))
 (let (($x285 (= flags 24051712)))
 (let (($x291 (= flags 23986176)))
 (let (($x293 (= flags 23789568)))
 (let (($x296 (= flags 23724032)))
 (let (($x299 (= flags 23658496)))
 (let (($x300 (= flags 23592960)))
 (let (($x302 (= flags 23527424)))
 (let (($x303 (= flags 23461888)))
 (let (($x306 (= flags 23265280)))
 (let (($x311 (= flags 23199744)))
 (let (($x308 (= flags 23134208)))
 (let (($x313 (= flags 23068672)))
 (let (($x191 (= flags 23003136)))
 (let (($x281 (= flags 22937600)))
 (let (($x249 (= flags 22740992)))
 (let (($x195 (= flags 22675456)))
 (let (($x279 (= flags 22609920)))
 (let (($x251 (= flags 22544384)))
 (let (($x193 (= flags 22478848)))
 (let (($x274 (= flags 22413312)))
 (let (($x246 (= flags 22216704)))
 (let (($x198 (= flags 22151168)))
 (let (($x276 (= flags 22085632)))
 (let (($x244 (= flags 22020096)))
 (let (($x200 (= flags 21954560)))
 (let (($x272 (= flags 21889024)))
 (let (($x242 (= flags 21692416)))
 (let (($x205 (= flags 21626880)))
 (let (($x271 (= flags 21561344)))
 (let (($x241 (= flags 21495808)))
 (let (($x203 (= flags 21430272)))
 (let (($x269 (= flags 21364736)))
 (let (($x237 (= flags 21168128)))
 (let (($x207 (= flags 21102592)))
 (let (($x267 (= flags 21037056)))
 (let (($x239 (= flags 20971520)))
 (let (($x208 (= flags 20905984)))
 (let (($x262 (= flags 20840448)))
 (let (($x234 (= flags 20643840)))
 (let (($x210 (= flags 20578304)))
 (let (($x264 (= flags 20512768)))
 (let (($x232 (= flags 20447232)))
 (let (($x212 (= flags 20381696)))
 (let (($x260 (= flags 20316160)))
 (let (($x230 (= flags 20119552)))
 (let (($x213 (= flags 20054016)))
 (let (($x259 (= flags 19988480)))
 (let (($x229 (= flags 19922944)))
 (let (($x217 (= flags 19857408)))
 (let (($x257 (= flags 19791872)))
 (let (($x225 (= flags 19595264)))
 (let (($x215 (= flags 19529728)))
 (let (($x255 (= flags 19464192)))
 (let (($x227 (= flags 19398656)))
 (let (($x220 (= flags 19333120)))
 (let (($x250 (= flags 19267584)))
 (let (($x222 (= flags 19070976)))
 (let (($x108 (= flags 19005440)))
 (let (($x190 (= flags 18939904)))
 (let (($x177 (= flags 18874368)))
 (let (($x155 (= flags 18808832)))
 (let (($x176 (= flags 18743296)))
 (let (($x152 (= flags 18546688)))
 (let (($x151 (= flags 18481152)))
 (let (($x150 (= flags 18415616)))
 (let (($x184 (= flags 18350080)))
 (let (($x183 (= flags 18284544)))
 (let (($x182 (= flags 18219008)))
 (let (($x178 (= flags 18022400)))
 (let (($x145 (= flags 17956864)))
 (let (($x144 (= flags 17891328)))
 (let (($x171 (= flags 17825792)))
 (let (($x163 (= flags 17760256)))
 (let (($x170 (= flags 17694720)))
 (let (($x134 (= flags 17498112)))
 (let (($x133 (= flags 17432576)))
 (let (($x132 (= flags 17367040)))
 (let (($x175 (= flags 17301504)))
 (let (($x174 (= flags 17235968)))
 (let (($x173 (= flags 17170432)))
 (let (($x146 (= flags 16973824)))
 (let (($x139 (= flags 16908288)))
 (let (($x137 (= flags 16842752)))
 (let (($x140 (= flags 16777216)))
 (let (($x138 (= flags 16711680)))
 (let (($x158 (= flags 16646144)))
 (let (($x185 (= flags 16449536)))
 (let (($x162 (= flags 16384000)))
 (let (($x107 (= flags 16318464)))
 (let (($x95 (= flags 16252928)))
 (let (($x96 (= flags 16187392)))
 (let (($x97 (= flags 16121856)))
 (let (($x101 (= flags 15925248)))
 (let (($x102 (= flags 15859712)))
 (let (($x103 (= flags 15794176)))
 (let (($x539 (= flags 15728640)))
 (let (($x535 (= flags 15663104)))
 (let (($x114 (= flags 15597568)))
 (let (($x120 (= flags 15400960)))
 (let (($x119 (= flags 15335424)))
 (let (($x118 (= flags 15269888)))
 (let (($x113 (= flags 15204352)))
 (let (($x111 (= flags 15138816)))
 (let (($x109 (= flags 15073280)))
 (let (($x90 (= flags 14876672)))
 (let (($x88 (= flags 14811136)))
 (let (($x86 (= flags 14745600)))
 (let (($x84 (= flags 14680064)))
 (let (($x82 (= flags 14614528)))
 (let (($x80 (= flags 14548992)))
 (let (($x78 (= flags 14352384)))
 (let (($x76 (= flags 14286848)))
 (let (($x74 (= flags 14221312)))
 (let (($x72 (= flags 14155776)))
 (let (($x70 (= flags 14090240)))
 (let (($x68 (= flags 14024704)))
 (let (($x66 (= flags 13828096)))
 (let (($x64 (= flags 13762560)))
 (let (($x52 (= flags 13697024)))
 (let (($x59 (= flags 13631488)))
 (let (($x62 (= flags 13565952)))
 (let (($x58 (= flags 13500416)))
 (let (($x56 (= flags 13303808)))
 (let (($x51 (= flags 13238272)))
 (let (($x19 (= flags 13172736)))
 (let (($x42 (= flags 13107200)))
 (let (($x41 (= flags 13041664)))
 (let (($x21 (= flags 12976128)))
 (let (($x18 (= flags 12779520)))
 (let (($x8 (= flags 12713984)))
 (let (($x38 (= flags 12648448)))
 (let (($x40 (= flags 12582912)))
 (let (($x301 (= flags 12517376)))
 (let (($x326 (= flags 12451840)))
 (let (($x655 (= flags 12255232)))
 (let (($x43 (= flags 12189696)))
 (let (($x13 (= flags 12124160)))
 (let (($x29 (= flags 12058624)))
 (let (($x130 (= flags 11993088)))
 (let (($x128 (= flags 11927552)))
 (let (($x126 (= flags 11730944)))
 (let (($x123 (= flags 11665408)))
 (let (($x5 (= flags 11599872)))
 (let (($x49 (= flags 11534336)))
 (let (($x46 (= flags 11468800)))
 (let (($x37 (= flags 11403264)))
 (let (($x44 (= flags 11206656)))
 (let (($x1063 (= flags 11141120)))
 (let (($x1061 (= flags 11075584)))
 (let (($x1059 (= flags 11010048)))
 (let (($x1057 (= flags 10944512)))
 (let (($x1055 (= flags 10878976)))
 (let (($x1053 (= flags 10682368)))
 (let (($x1051 (= flags 10616832)))
 (let (($x1049 (= flags 10551296)))
 (let (($x1047 (= flags 10485760)))
 (let (($x1045 (= flags 10420224)))
 (let (($x1043 (= flags 10354688)))
 (let (($x1041 (= flags 10158080)))
 (let (($x1039 (= flags 10092544)))
 (let (($x1037 (= flags 10027008)))
 (let (($x1035 (= flags 9961472)))
 (let (($x1033 (= flags 9895936)))
 (let (($x1031 (= flags 9830400)))
 (let (($x1029 (= flags 9633792)))
 (let (($x1027 (= flags 9568256)))
 (let (($x1025 (= flags 9502720)))
 (let (($x1023 (= flags 9437184)))
 (let (($x1021 (= flags 9371648)))
 (let (($x1019 (= flags 9306112)))
 (let (($x1017 (= flags 9109504)))
 (let (($x1015 (= flags 9043968)))
 (let (($x1013 (= flags 8978432)))
 (let (($x1011 (= flags 8912896)))
 (let (($x1009 (= flags 8847360)))
 (let (($x1007 (= flags 8781824)))
 (let (($x1005 (= flags 8585216)))
 (let (($x1003 (= flags 8519680)))
 (let (($x1001 (= flags 8454144)))
 (let (($x999 (= flags 8388608)))
 (let (($x997 (= flags 8323072)))
 (let (($x995 (= flags 8257536)))
 (let (($x993 (= flags 8060928)))
 (let (($x991 (= flags 7995392)))
 (let (($x989 (= flags 7929856)))
 (let (($x987 (= flags 7864320)))
 (let (($x985 (= flags 7798784)))
 (let (($x983 (= flags 7733248)))
 (let (($x981 (= flags 7536640)))
 (let (($x979 (= flags 7471104)))
 (let (($x977 (= flags 7405568)))
 (let (($x975 (= flags 7340032)))
 (let (($x973 (= flags 7274496)))
 (let (($x971 (= flags 7208960)))
 (let (($x969 (= flags 7012352)))
 (let (($x967 (= flags 6946816)))
 (let (($x965 (= flags 6881280)))
 (let (($x963 (= flags 6815744)))
 (let (($x961 (= flags 6750208)))
 (let (($x959 (= flags 6684672)))
 (let (($x957 (= flags 6488064)))
 (let (($x955 (= flags 6422528)))
 (let (($x953 (= flags 6356992)))
 (let (($x951 (= flags 6291456)))
 (let (($x949 (= flags 6225920)))
 (let (($x947 (= flags 6160384)))
 (let (($x945 (= flags 5963776)))
 (let (($x943 (= flags 5898240)))
 (let (($x941 (= flags 5832704)))
 (let (($x939 (= flags 5767168)))
 (let (($x937 (= flags 5701632)))
 (let (($x935 (= flags 5636096)))
 (let (($x933 (= flags 5439488)))
 (let (($x931 (= flags 5373952)))
 (let (($x929 (= flags 5308416)))
 (let (($x927 (= flags 5242880)))
 (let (($x925 (= flags 5177344)))
 (let (($x923 (= flags 5111808)))
 (let (($x921 (= flags 4915200)))
 (let (($x919 (= flags 4849664)))
 (let (($x917 (= flags 4784128)))
 (let (($x915 (= flags 4718592)))
 (let (($x913 (= flags 4653056)))
 (let (($x911 (= flags 4587520)))
 (let (($x909 (= flags 4390912)))
 (let (($x907 (= flags 4325376)))
 (let (($x905 (= flags 4259840)))
 (let (($x903 (= flags 4194304)))
 (let (($x901 (= flags 4128768)))
 (let (($x899 (= flags 4063232)))
 (let (($x897 (= flags 3866624)))
 (let (($x895 (= flags 3801088)))
 (let (($x893 (= flags 3735552)))
 (let (($x891 (= flags 3670016)))
 (let (($x889 (= flags 3604480)))
 (let (($x887 (= flags 3538944)))
 (let (($x885 (= flags 3342336)))
 (let (($x883 (= flags 3276800)))
 (let (($x881 (= flags 3211264)))
 (let (($x879 (= flags 3145728)))
 (let (($x877 (= flags 3080192)))
 (let (($x875 (= flags 3014656)))
 (let (($x873 (= flags 2818048)))
 (let (($x871 (= flags 2752512)))
 (let (($x869 (= flags 2686976)))
 (let (($x867 (= flags 2621440)))
 (let (($x865 (= flags 2555904)))
 (let (($x863 (= flags 2490368)))
 (let (($x861 (= flags 2293760)))
 (let (($x859 (= flags 2228224)))
 (let (($x857 (= flags 2162688)))
 (let (($x855 (= flags 2097152)))
 (let (($x853 (= flags 2031616)))
 (let (($x851 (= flags 1966080)))
 (let (($x849 (= flags 1769472)))
 (let (($x847 (= flags 1703936)))
 (let (($x845 (= flags 1638400)))
 (let (($x843 (= flags 1572864)))
 (let (($x840 (= flags 1507328)))
 (let (($x839 (= flags 1441792)))
 (let (($x837 (= flags 1245184)))
 (let (($x835 (= flags 1179648)))
 (let (($x833 (= flags 1114112)))
 (let (($x831 (= flags 1048576)))
 (let (($x829 (= flags 983040)))
 (let (($x827 (= flags 917504)))
 (let (($x824 (= flags 720896)))
 (let (($x821 (= flags 655360)))
 (let (($x820 (= flags 589824)))
 (let (($x818 (= flags 524288)))
 (let (($x816 (= flags 458752)))
 (let (($x814 (= flags 393216)))
 (let (($x812 (= flags 196608)))
 (let (($x810 (= flags 131072)))
 (let (($x808 (= flags 65536)))
 (let (($x806 (= flags 0)))
 (or $x806 $x808 $x810 $x812 $x814 $x816 $x818 $x820 $x821 $x824 $x827 $x829 $x831 $x833 $x835 $x837 $x839 $x840 $x843 $x845 $x847 $x849 $x851 $x853 $x855 $x857 $x859 $x861 $x863 $x865 $x867 $x869 $x871 $x873 $x875 $x877 $x879 $x881 $x883 $x885 $x887 $x889 $x891 $x893 $x895 $x897 $x899 $x901 $x903 $x905 $x907 $x909 $x911 $x913 $x915 $x917 $x919 $x921 $x923 $x925 $x927 $x929 $x931 $x933 $x935 $x937 $x939 $x941 $x943 $x945 $x947 $x949 $x951 $x953 $x955 $x957 $x959 $x961 $x963 $x965 $x967 $x969 $x971 $x973 $x975 $x977 $x979 $x981 $x983 $x985 $x987 $x989 $x991 $x993 $x995 $x997 $x999 $x1001 $x1003 $x1005 $x1007 $x1009 $x1011 $x1013 $x1015 $x1017 $x1019 $x1021 $x1023 $x1025 $x1027 $x1029 $x1031 $x1033 $x1035 $x1037 $x1039 $x1041 $x1043 $x1045 $x1047 $x1049 $x1051 $x1053 $x1055 $x1057 $x1059 $x1061 $x1063 $x44 $x37 $x46 $x49 $x5 $x123 $x126 $x128 $x130 $x29 $x13 $x43 $x655 $x326 $x301 $x40 $x38 $x8 $x18 $x21 $x41 $x42 $x19 $x51 $x56 $x58 $x62 $x59 $x52 $x64 $x66 $x68 $x70 $x72 $x74 $x76 $x78 $x80 $x82 $x84 $x86 $x88 $x90 $x109 $x111 $x113 $x118 $x119 $x120 $x114 $x535 $x539 $x103 $x102 $x101 $x97 $x96 $x95 $x107 $x162 $x185 $x158 $x138 $x140 $x137 $x139 $x146 $x173 $x174 $x175 $x132 $x133 $x134 $x170 $x163 $x171 $x144 $x145 $x178 $x182 $x183 $x184 $x150 $x151 $x152 $x176 $x155 $x177 $x190 $x108 $x222 $x250 $x220 $x227 $x255 $x215 $x225 $x257 $x217 $x229 $x259 $x213 $x230 $x260 $x212 $x232 $x264 $x210 $x234 $x262 $x208 $x239 $x267 $x207 $x237 $x269 $x203 $x241 $x271 $x205 $x242 $x272 $x200 $x244 $x276 $x198 $x246 $x274 $x193 $x251 $x279 $x195 $x249 $x281 $x191 $x313 $x308 $x311 $x306 $x303 $x302 $x300 $x299 $x296 $x293 $x291 $x285 $x289 $x287 $x283 $x310 $x315 $x316 $x323 $x318 $x324 $x322 $x327 $x331 $x329 $x333 $x337 $x341 $x339 $x343 $x347 $x345 $x349 $x346 $x353 $x351 $x359 $x357 $x363 $x358 $x365 $x366 $x371 $x369 $x372 $x375 $x370 $x378 $x383 $x381 $x384 $x387 $x382 $x390 $x395 $x393 $x396 $x399 $x394 $x402 $x407 $x405 $x408 $x411 $x406 $x414 $x419 $x417 $x420 $x423 $x418 $x426 $x431 $x429 $x432 $x435 $x430 $x438 $x443 $x441 $x444 $x447 $x442 $x450 $x455 $x453 $x456 $x459 $x454 $x462 $x467 $x465 $x468 $x471 $x466 $x474 $x479 $x477 $x480 $x483 $x478 $x486 $x491 $x489 $x492 $x495 $x490 $x498 $x503 $x501 $x504 $x507 $x502 $x510 $x515 $x513 $x516 $x519 $x514 $x522))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert
 (let (($x792 (= flags 33357824)))
(let (($x794 (= flags 33292288)))
(let (($x797 (= flags 32833536)))
(let (($x800 (= flags 32768000)))
(let (($x803 (= flags 32309248)))
(let (($x804 (= flags 32243712)))
(let (($x805 (= flags 31784960)))
(let (($x798 (= flags 31719424)))
(let (($x788 (= flags 31260672)))
(let (($x786 (= flags 31195136)))
(let (($x783 (= flags 30736384)))
(let (($x782 (= flags 30670848)))
(let (($x780 (= flags 30212096)))
(let (($x778 (= flags 30146560)))
(let (($x776 (= flags 29687808)))
(let (($x774 (= flags 29622272)))
(let (($x772 (= flags 29163520)))
(let (($x769 (= flags 29097984)))
(let (($x768 (= flags 28639232)))
(let (($x766 (= flags 28573696)))
(let (($x765 (= flags 28114944)))
(let (($x762 (= flags 28049408)))
(let (($x760 (= flags 27590656)))
(let (($x692 (= flags 27525120)))
(let (($x758 (= flags 27066368)))
(let (($x757 (= flags 27000832)))
(let (($x689 (= flags 26542080)))
(let (($x754 (= flags 26476544)))
(let (($x753 (= flags 26017792)))
(let (($x687 (= flags 25952256)))
(let (($x750 (= flags 25493504)))
(let (($x749 (= flags 25427968)))
(let (($x685 (= flags 24969216)))
(let (($x745 (= flags 24903680)))
(let (($x746 (= flags 24444928)))
(let (($x683 (= flags 24379392)))
(let (($x742 (= flags 23920640)))
(let (($x741 (= flags 23855104)))
(let (($x681 (= flags 23396352)))
(let (($x738 (= flags 23330816)))
(let (($x737 (= flags 22872064)))
(let (($x679 (= flags 22806528)))
(let (($x734 (= flags 22347776)))
(let (($x733 (= flags 22282240)))
(let (($x677 (= flags 21823488)))
(let (($x730 (= flags 21757952)))
(let (($x729 (= flags 21299200)))
(let (($x675 (= flags 21233664)))
(let (($x725 (= flags 20774912)))
(let (($x724 (= flags 20709376)))
(let (($x673 (= flags 20250624)))
(let (($x721 (= flags 20185088)))
(let (($x720 (= flags 19726336)))
(let (($x671 (= flags 19660800)))
(let (($x717 (= flags 19202048)))
(let (($x716 (= flags 19136512)))
(let (($x669 (= flags 18677760)))
(let (($x713 (= flags 18612224)))
(let (($x712 (= flags 18153472)))
(let (($x667 (= flags 18087936)))
(let (($x709 (= flags 17629184)))
(let (($x708 (= flags 17563648)))
(let (($x665 (= flags 17104896)))
(let (($x704 (= flags 17039360)))
(let (($x703 (= flags 16580608)))
(let (($x663 (= flags 16515072)))
(let (($x700 (= flags 16056320)))
(let (($x699 (= flags 15990784)))
(let (($x661 (= flags 15532032)))
(let (($x696 (= flags 15466496)))
(let (($x695 (= flags 15007744)))
(let (($x691 (= flags 14942208)))
(let (($x658 (= flags 14483456)))
(let (($x656 (= flags 14417920)))
(let (($x591 (= flags 13959168)))
(let (($x588 (= flags 13893632)))
(let (($x651 (= flags 13434880)))
(let (($x586 (= flags 13369344)))
(let (($x646 (= flags 12910592)))
(let (($x585 (= flags 12845056)))
(let (($x645 (= flags 12386304)))
(let (($x644 (= flags 12320768)))
(let (($x643 (= flags 11862016)))
(let (($x582 (= flags 11796480)))
(let (($x638 (= flags 11337728)))
(let (($x581 (= flags 11272192)))
(let (($x637 (= flags 10813440)))
(let (($x636 (= flags 10747904)))
(let (($x635 (= flags 10289152)))
(let (($x578 (= flags 10223616)))
(let (($x630 (= flags 9764864)))
(let (($x577 (= flags 9699328)))
(let (($x629 (= flags 9240576)))
(let (($x628 (= flags 9175040)))
(let (($x627 (= flags 8716288)))
(let (($x574 (= flags 8650752)))
(let (($x622 (= flags 8192000)))
(let (($x573 (= flags 8126464)))
(let (($x621 (= flags 7667712)))
(let (($x620 (= flags 7602176)))
(let (($x619 (= flags 7143424)))
(let (($x570 (= flags 7077888)))
(let (($x614 (= flags 6619136)))
(let (($x569 (= flags 6553600)))
(let (($x613 (= flags 6094848)))
(let (($x612 (= flags 6029312)))
(let (($x611 (= flags 5570560)))
(let (($x566 (= flags 5505024)))
(let (($x606 (= flags 5046272)))
(let (($x565 (= flags 4980736)))
(let (($x605 (= flags 4521984)))
(let (($x604 (= flags 4456448)))
(let (($x603 (= flags 3997696)))
(let (($x562 (= flags 3932160)))
(let (($x598 (= flags 3473408)))
(let (($x561 (= flags 3407872)))
(let (($x597 (= flags 2949120)))
(let (($x596 (= flags 2883584)))
(let (($x595 (= flags 2424832)))
(let (($x558 (= flags 2359296)))
(let (($x555 (= flags 1900544)))
(let (($x589 (= flags 1835008)))
(let (($x554 (= flags 1376256)))
(let (($x553 (= flags 1310720)))
(let (($x551 (= flags 851968)))
(let (($x549 (= flags 786432)))
(let (($x544 (= flags 327680)))
(let (($x546 (= flags 262144)))
(or $x546 $x544 $x549 $x551 $x553 $x554 $x589 $x555 $x558 $x595 $x596 $x597 $x561 $x598 $x562 $x603 $x604 $x605 $x565 $x606 $x566 $x611 $x612 $x613 $x569 $x614 $x570 $x619 $x620 $x621 $x573 $x622 $x574 $x627 $x628 $x629 $x577 $x630 $x578 $x635 $x636 $x637 $x581 $x638 $x582 $x643 $x644 $x645 $x585 $x646 $x586 $x651 $x588 $x591 $x656 $x658 $x691 $x695 $x696 $x661 $x699 $x700 $x663 $x703 $x704 $x665 $x708 $x709 $x667 $x712 $x713 $x669 $x716 $x717 $x671 $x720 $x721 $x673 $x724 $x725 $x675 $x729 $x730 $x677 $x733 $x734 $x679 $x737 $x738 $x681 $x741 $x742 $x683 $x746 $x745 $x685 $x749 $x750 $x687 $x753 $x754 $x689 $x757 $x758 $x692 $x760 $x762 $x765 $x766 $x768 $x769 $x772 $x774 $x776 $x778 $x780 $x782 $x783 $x786 $x788 $x798 $x805 $x804 $x803 $x800 $x797 $x794 $x792))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

Login Shell vs Preserve-Env Non-Conflict (-i vs -E)

🌳 tree-sitter VERIFIED

Function: parse_args · Z3 solved in 5403.6ms

MODE_LOGIN_SHELL and MODE_PRESERVE_ENV must not both be set in final option flags (parse_args() rejects -i with -E).

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun flags () Int)
(assert
 (let (($x277 (= flags 33226752)))
 (let (($x245 (= flags 33161216)))
 (let (($x199 (= flags 33095680)))
 (let (($x273 (= flags 33030144)))
 (let (($x243 (= flags 32702464)))
 (let (($x201 (= flags 32636928)))
 (let (($x275 (= flags 32571392)))
 (let (($x238 (= flags 32505856)))
 (let (($x202 (= flags 32178176)))
 (let (($x270 (= flags 32112640)))
 (let (($x240 (= flags 32047104)))
 (let (($x206 (= flags 31981568)))
 (let (($x268 (= flags 31653888)))
 (let (($x236 (= flags 31588352)))
 (let (($x204 (= flags 31522816)))
 (let (($x266 (= flags 31457280)))
 (let (($x235 (= flags 31129600)))
 (let (($x209 (= flags 31064064)))
 (let (($x265 (= flags 30998528)))
 (let (($x233 (= flags 30932992)))
 (let (($x211 (= flags 30605312)))
 (let (($x261 (= flags 30539776)))
 (let (($x231 (= flags 30474240)))
 (let (($x216 (= flags 30408704)))
 (let (($x263 (= flags 30081024)))
 (let (($x226 (= flags 30015488)))
 (let (($x214 (= flags 29949952)))
 (let (($x258 (= flags 29884416)))
 (let (($x228 (= flags 29556736)))
 (let (($x218 (= flags 29491200)))
 (let (($x256 (= flags 29425664)))
 (let (($x224 (= flags 29360128)))
 (let (($x219 (= flags 29294592)))
 (let (($x254 (= flags 29229056)))
 (let (($x223 (= flags 29163520)))
 (let (($x221 (= flags 29097984)))
 (let (($x253 (= flags 29032448)))
 (let (($x194 (= flags 28966912)))
 (let (($x188 (= flags 28901376)))
 (let (($x187 (= flags 28835840)))
 (let (($x156 (= flags 28770304)))
 (let (($x154 (= flags 28704768)))
 (let (($x153 (= flags 28639232)))
 (let (($x168 (= flags 28573696)))
 (let (($x166 (= flags 28508160)))
 (let (($x164 (= flags 28442624)))
 (let (($x181 (= flags 28377088)))
 (let (($x180 (= flags 28311552)))
 (let (($x179 (= flags 28246016)))
 (let (($x143 (= flags 28180480)))
 (let (($x142 (= flags 28114944)))
 (let (($x172 (= flags 28049408)))
 (let (($x169 (= flags 27983872)))
 (let (($x165 (= flags 27918336)))
 (let (($x167 (= flags 27852800)))
 (let (($x161 (= flags 27787264)))
 (let (($x160 (= flags 27721728)))
 (let (($x159 (= flags 27656192)))
 (let (($x149 (= flags 27590656)))
 (let (($x148 (= flags 27525120)))
 (let (($x147 (= flags 27459584)))
 (let (($x131 (= flags 27394048)))
 (let (($x141 (= flags 27328512)))
 (let (($x136 (= flags 27262976)))
 (let (($x157 (= flags 27197440)))
 (let (($x135 (= flags 27131904)))
 (let (($x186 (= flags 27066368)))
 (let (($x92 (= flags 27000832)))
 (let (($x93 (= flags 26935296)))
 (let (($x94 (= flags 26869760)))
 (let (($x98 (= flags 26804224)))
 (let (($x99 (= flags 26738688)))
 (let (($x100 (= flags 26673152)))
 (let (($x104 (= flags 26607616)))
 (let (($x105 (= flags 26542080)))
 (let (($x534 (= flags 26476544)))
 (let (($x112 (= flags 26411008)))
 (let (($x121 (= flags 26345472)))
 (let (($x106 (= flags 26279936)))
 (let (($x117 (= flags 26214400)))
 (let (($x116 (= flags 26148864)))
 (let (($x115 (= flags 26083328)))
 (let (($x110 (= flags 26017792)))
 (let (($x91 (= flags 25952256)))
 (let (($x89 (= flags 25886720)))
 (let (($x87 (= flags 25821184)))
 (let (($x85 (= flags 25755648)))
 (let (($x83 (= flags 25690112)))
 (let (($x81 (= flags 25624576)))
 (let (($x79 (= flags 25559040)))
 (let (($x77 (= flags 25493504)))
 (let (($x75 (= flags 25427968)))
 (let (($x73 (= flags 25362432)))
 (let (($x71 (= flags 25296896)))
 (let (($x69 (= flags 25231360)))
 (let (($x67 (= flags 25165824)))
 (let (($x65 (= flags 24838144)))
 (let (($x53 (= flags 24772608)))
 (let (($x60 (= flags 24707072)))
 (let (($x63 (= flags 24641536)))
 (let (($x61 (= flags 24313856)))
 (let (($x57 (= flags 24248320)))
 (let (($x54 (= flags 24182784)))
 (let (($x55 (= flags 24117248)))
 (let (($x15 (= flags 23789568)))
 (let (($x9 (= flags 23724032)))
 (let (($x39 (= flags 23658496)))
 (let (($x20 (= flags 23592960)))
 (let (($x26 (= flags 23265280)))
 (let (($x33 (= flags 23199744)))
 (let (($x35 (= flags 23134208)))
 (let (($x22 (= flags 23068672)))
 (let (($x825 (= flags 22740992)))
 (let (($x652 (= flags 22675456)))
 (let (($x587 (= flags 22609920)))
 (let (($x24 (= flags 22544384)))
 (let (($x34 (= flags 22216704)))
 (let (($x12 (= flags 22151168)))
 (let (($x129 (= flags 22085632)))
 (let (($x127 (= flags 22020096)))
 (let (($x124 (= flags 21692416)))
 (let (($x122 (= flags 21626880)))
 (let (($x50 (= flags 21561344)))
 (let (($x47 (= flags 21495808)))
 (let (($x45 (= flags 21168128)))
 (let (($x48 (= flags 21102592)))
 (let (($x23 (= flags 21037056)))
 (let (($x1062 (= flags 20971520)))
 (let (($x1060 (= flags 20905984)))
 (let (($x1058 (= flags 20840448)))
 (let (($x1056 (= flags 20774912)))
 (let (($x1054 (= flags 20709376)))
 (let (($x1052 (= flags 20643840)))
 (let (($x1050 (= flags 20578304)))
 (let (($x1048 (= flags 20512768)))
 (let (($x1046 (= flags 20447232)))
 (let (($x1044 (= flags 20381696)))
 (let (($x1042 (= flags 20316160)))
 (let (($x1040 (= flags 20250624)))
 (let (($x1038 (= flags 20185088)))
 (let (($x1036 (= flags 20119552)))
 (let (($x1034 (= flags 20054016)))
 (let (($x1032 (= flags 19988480)))
 (let (($x1030 (= flags 19922944)))
 (let (($x1028 (= flags 19857408)))
 (let (($x1026 (= flags 19791872)))
 (let (($x1024 (= flags 19726336)))
 (let (($x1022 (= flags 19660800)))
 (let (($x1020 (= flags 19595264)))
 (let (($x1018 (= flags 19529728)))
 (let (($x1016 (= flags 19464192)))
 (let (($x1014 (= flags 19398656)))
 (let (($x1012 (= flags 19333120)))
 (let (($x1010 (= flags 19267584)))
 (let (($x1008 (= flags 19202048)))
 (let (($x1006 (= flags 19136512)))
 (let (($x1004 (= flags 19070976)))
 (let (($x1002 (= flags 19005440)))
 (let (($x1000 (= flags 18939904)))
 (let (($x998 (= flags 18874368)))
 (let (($x996 (= flags 18808832)))
 (let (($x994 (= flags 18743296)))
 (let (($x992 (= flags 18677760)))
 (let (($x990 (= flags 18612224)))
 (let (($x988 (= flags 18546688)))
 (let (($x986 (= flags 18481152)))
 (let (($x984 (= flags 18415616)))
 (let (($x982 (= flags 18350080)))
 (let (($x980 (= flags 18284544)))
 (let (($x978 (= flags 18219008)))
 (let (($x976 (= flags 18153472)))
 (let (($x974 (= flags 18087936)))
 (let (($x972 (= flags 18022400)))
 (let (($x970 (= flags 17956864)))
 (let (($x968 (= flags 17891328)))
 (let (($x966 (= flags 17825792)))
 (let (($x964 (= flags 17760256)))
 (let (($x962 (= flags 17694720)))
 (let (($x960 (= flags 17629184)))
 (let (($x958 (= flags 17563648)))
 (let (($x956 (= flags 17498112)))
 (let (($x954 (= flags 17432576)))
 (let (($x952 (= flags 17367040)))
 (let (($x950 (= flags 17301504)))
 (let (($x948 (= flags 17235968)))
 (let (($x946 (= flags 17170432)))
 (let (($x944 (= flags 17104896)))
 (let (($x942 (= flags 17039360)))
 (let (($x940 (= flags 16973824)))
 (let (($x938 (= flags 16908288)))
 (let (($x936 (= flags 16842752)))
 (let (($x934 (= flags 16777216)))
 (let (($x932 (= flags 16449536)))
 (let (($x930 (= flags 16384000)))
 (let (($x928 (= flags 16318464)))
 (let (($x926 (= flags 16252928)))
 (let (($x924 (= flags 15925248)))
 (let (($x922 (= flags 15859712)))
 (let (($x920 (= flags 15794176)))
 (let (($x918 (= flags 15728640)))
 (let (($x916 (= flags 15400960)))
 (let (($x914 (= flags 15335424)))
 (let (($x912 (= flags 15269888)))
 (let (($x910 (= flags 15204352)))
 (let (($x908 (= flags 14876672)))
 (let (($x906 (= flags 14811136)))
 (let (($x904 (= flags 14745600)))
 (let (($x902 (= flags 14680064)))
 (let (($x900 (= flags 14352384)))
 (let (($x898 (= flags 14286848)))
 (let (($x896 (= flags 14221312)))
 (let (($x894 (= flags 14155776)))
 (let (($x892 (= flags 13828096)))
 (let (($x890 (= flags 13762560)))
 (let (($x888 (= flags 13697024)))
 (let (($x886 (= flags 13631488)))
 (let (($x884 (= flags 13303808)))
 (let (($x882 (= flags 13238272)))
 (let (($x880 (= flags 13172736)))
 (let (($x878 (= flags 13107200)))
 (let (($x876 (= flags 12779520)))
 (let (($x874 (= flags 12713984)))
 (let (($x872 (= flags 12648448)))
 (let (($x870 (= flags 12582912)))
 (let (($x868 (= flags 12517376)))
 (let (($x866 (= flags 12451840)))
 (let (($x864 (= flags 12386304)))
 (let (($x862 (= flags 12320768)))
 (let (($x860 (= flags 12255232)))
 (let (($x858 (= flags 12189696)))
 (let (($x856 (= flags 12124160)))
 (let (($x854 (= flags 12058624)))
 (let (($x852 (= flags 11993088)))
 (let (($x850 (= flags 11927552)))
 (let (($x848 (= flags 11862016)))
 (let (($x846 (= flags 11796480)))
 (let (($x844 (= flags 11730944)))
 (let (($x842 (= flags 11665408)))
 (let (($x841 (= flags 11599872)))
 (let (($x838 (= flags 11534336)))
 (let (($x836 (= flags 11468800)))
 (let (($x834 (= flags 11403264)))
 (let (($x832 (= flags 11337728)))
 (let (($x830 (= flags 11272192)))
 (let (($x828 (= flags 11206656)))
 (let (($x826 (= flags 11141120)))
 (let (($x823 (= flags 11075584)))
 (let (($x822 (= flags 11010048)))
 (let (($x819 (= flags 10944512)))
 (let (($x817 (= flags 10878976)))
 (let (($x815 (= flags 10813440)))
 (let (($x813 (= flags 10747904)))
 (let (($x811 (= flags 10682368)))
 (let (($x809 (= flags 10616832)))
 (let (($x807 (= flags 10551296)))
 (let (($x791 (= flags 10485760)))
 (let (($x793 (= flags 10420224)))
 (let (($x795 (= flags 10354688)))
 (let (($x799 (= flags 10289152)))
 (let (($x801 (= flags 10223616)))
 (let (($x802 (= flags 10158080)))
 (let (($x790 (= flags 10092544)))
 (let (($x796 (= flags 10027008)))
 (let (($x789 (= flags 9961472)))
 (let (($x787 (= flags 9895936)))
 (let (($x785 (= flags 9830400)))
 (let (($x784 (= flags 9764864)))
 (let (($x781 (= flags 9699328)))
 (let (($x779 (= flags 9633792)))
 (let (($x777 (= flags 9568256)))
 (let (($x775 (= flags 9502720)))
 (let (($x773 (= flags 9437184)))
 (let (($x771 (= flags 9371648)))
 (let (($x770 (= flags 9306112)))
 (let (($x767 (= flags 9240576)))
 (let (($x764 (= flags 9175040)))
 (let (($x763 (= flags 9109504)))
 (let (($x761 (= flags 9043968)))
 (let (($x693 (= flags 8978432)))
 (let (($x759 (= flags 8912896)))
 (let (($x690 (= flags 8847360)))
 (let (($x756 (= flags 8781824)))
 (let (($x755 (= flags 8716288)))
 (let (($x688 (= flags 8650752)))
 (let (($x752 (= flags 8585216)))
 (let (($x751 (= flags 8519680)))
 (let (($x686 (= flags 8454144)))
 (let (($x748 (= flags 8388608)))
 (let (($x747 (= flags 8060928)))
 (let (($x684 (= flags 7995392)))
 (let (($x744 (= flags 7929856)))
 (let (($x743 (= flags 7864320)))
 (let (($x682 (= flags 7536640)))
 (let (($x740 (= flags 7471104)))
 (let (($x739 (= flags 7405568)))
 (let (($x680 (= flags 7340032)))
 (let (($x736 (= flags 7012352)))
 (let (($x735 (= flags 6946816)))
 (let (($x678 (= flags 6881280)))
 (let (($x732 (= flags 6815744)))
 (let (($x731 (= flags 6488064)))
 (let (($x676 (= flags 6422528)))
 (let (($x728 (= flags 6356992)))
 (let (($x727 (= flags 6291456)))
 (let (($x674 (= flags 5963776)))
 (let (($x723 (= flags 5898240)))
 (let (($x722 (= flags 5832704)))
 (let (($x672 (= flags 5767168)))
 (let (($x719 (= flags 5439488)))
 (let (($x718 (= flags 5373952)))
 (let (($x670 (= flags 5308416)))
 (let (($x715 (= flags 5242880)))
 (let (($x714 (= flags 4915200)))
 (let (($x668 (= flags 4849664)))
 (let (($x711 (= flags 4784128)))
 (let (($x710 (= flags 4718592)))
 (let (($x666 (= flags 4390912)))
 (let (($x706 (= flags 4325376)))
 (let (($x705 (= flags 4259840)))
 (let (($x664 (= flags 4194304)))
 (let (($x702 (= flags 4128768)))
 (let (($x701 (= flags 4063232)))
 (let (($x662 (= flags 3997696)))
 (let (($x698 (= flags 3932160)))
 (let (($x697 (= flags 3866624)))
 (let (($x660 (= flags 3801088)))
 (let (($x694 (= flags 3735552)))
 (let (($x659 (= flags 3670016)))
 (let (($x657 (= flags 3604480)))
 (let (($x654 (= flags 3538944)))
 (let (($x590 (= flags 3473408)))
 (let (($x653 (= flags 3407872)))
 (let (($x650 (= flags 3342336)))
 (let (($x649 (= flags 3276800)))
 (let (($x648 (= flags 3211264)))
 (let (($x584 (= flags 3145728)))
 (let (($x647 (= flags 3080192)))
 (let (($x583 (= flags 3014656)))
 (let (($x642 (= flags 2949120)))
 (let (($x641 (= flags 2883584)))
 (let (($x640 (= flags 2818048)))
 (let (($x580 (= flags 2752512)))
 (let (($x639 (= flags 2686976)))
 (let (($x579 (= flags 2621440)))
 (let (($x634 (= flags 2555904)))
 (let (($x633 (= flags 2490368)))
 (let (($x632 (= flags 2424832)))
 (let (($x576 (= flags 2359296)))
 (let (($x631 (= flags 2293760)))
 (let (($x575 (= flags 2228224)))
 (let (($x626 (= flags 2162688)))
 (let (($x625 (= flags 2097152)))
 (let (($x624 (= flags 2031616)))
 (let (($x572 (= flags 1966080)))
 (let (($x623 (= flags 1900544)))
 (let (($x571 (= flags 1835008)))
 (let (($x618 (= flags 1769472)))
 (let (($x617 (= flags 1703936)))
 (let (($x616 (= flags 1638400)))
 (let (($x568 (= flags 1572864)))
 (let (($x615 (= flags 1507328)))
 (let (($x567 (= flags 1441792)))
 (let (($x610 (= flags 1376256)))
 (let (($x609 (= flags 1310720)))
 (let (($x608 (= flags 1245184)))
 (let (($x564 (= flags 1179648)))
 (let (($x607 (= flags 1114112)))
 (let (($x563 (= flags 1048576)))
 (let (($x602 (= flags 983040)))
 (let (($x601 (= flags 917504)))
 (let (($x600 (= flags 851968)))
 (let (($x560 (= flags 786432)))
 (let (($x599 (= flags 720896)))
 (let (($x559 (= flags 655360)))
 (let (($x594 (= flags 589824)))
 (let (($x593 (= flags 524288)))
 (let (($x592 (= flags 458752)))
 (let (($x556 (= flags 393216)))
 (let (($x557 (= flags 327680)))
 (let (($x552 (= flags 262144)))
 (let (($x550 (= flags 196608)))
 (let (($x548 (= flags 131072)))
 (let (($x547 (= flags 65536)))
 (let (($x543 (= flags 0)))
 (or $x543 $x547 $x548 $x550 $x552 $x557 $x556 $x592 $x593 $x594 $x559 $x599 $x560 $x600 $x601 $x602 $x563 $x607 $x564 $x608 $x609 $x610 $x567 $x615 $x568 $x616 $x617 $x618 $x571 $x623 $x572 $x624 $x625 $x626 $x575 $x631 $x576 $x632 $x633 $x634 $x579 $x639 $x580 $x640 $x641 $x642 $x583 $x647 $x584 $x648 $x649 $x650 $x653 $x590 $x654 $x657 $x659 $x694 $x660 $x697 $x698 $x662 $x701 $x702 $x664 $x705 $x706 $x666 $x710 $x711 $x668 $x714 $x715 $x670 $x718 $x719 $x672 $x722 $x723 $x674 $x727 $x728 $x676 $x731 $x732 $x678 $x735 $x736 $x680 $x739 $x740 $x682 $x743 $x744 $x684 $x747 $x748 $x686 $x751 $x752 $x688 $x755 $x756 $x690 $x759 $x693 $x761 $x763 $x764 $x767 $x770 $x771 $x773 $x775 $x777 $x779 $x781 $x784 $x785 $x787 $x789 $x796 $x790 $x802 $x801 $x799 $x795 $x793 $x791 $x807 $x809 $x811 $x813 $x815 $x817 $x819 $x822 $x823 $x826 $x828 $x830 $x832 $x834 $x836 $x838 $x841 $x842 $x844 $x846 $x848 $x850 $x852 $x854 $x856 $x858 $x860 $x862 $x864 $x866 $x868 $x870 $x872 $x874 $x876 $x878 $x880 $x882 $x884 $x886 $x888 $x890 $x892 $x894 $x896 $x898 $x900 $x902 $x904 $x906 $x908 $x910 $x912 $x914 $x916 $x918 $x920 $x922 $x924 $x926 $x928 $x930 $x932 $x934 $x936 $x938 $x940 $x942 $x944 $x946 $x948 $x950 $x952 $x954 $x956 $x958 $x960 $x962 $x964 $x966 $x968 $x970 $x972 $x974 $x976 $x978 $x980 $x982 $x984 $x986 $x988 $x990 $x992 $x994 $x996 $x998 $x1000 $x1002 $x1004 $x1006 $x1008 $x1010 $x1012 $x1014 $x1016 $x1018 $x1020 $x1022 $x1024 $x1026 $x1028 $x1030 $x1032 $x1034 $x1036 $x1038 $x1040 $x1042 $x1044 $x1046 $x1048 $x1050 $x1052 $x1054 $x1056 $x1058 $x1060 $x1062 $x23 $x48 $x45 $x47 $x50 $x122 $x124 $x127 $x129 $x12 $x34 $x24 $x587 $x652 $x825 $x22 $x35 $x33 $x26 $x20 $x39 $x9 $x15 $x55 $x54 $x57 $x61 $x63 $x60 $x53 $x65 $x67 $x69 $x71 $x73 $x75 $x77 $x79 $x81 $x83 $x85 $x87 $x89 $x91 $x110 $x115 $x116 $x117 $x106 $x121 $x112 $x534 $x105 $x104 $x100 $x99 $x98 $x94 $x93 $x92 $x186 $x135 $x157 $x136 $x141 $x131 $x147 $x148 $x149 $x159 $x160 $x161 $x167 $x165 $x169 $x172 $x142 $x143 $x179 $x180 $x181 $x164 $x166 $x168 $x153 $x154 $x156 $x187 $x188 $x194 $x253 $x221 $x223 $x254 $x219 $x224 $x256 $x218 $x228 $x258 $x214 $x226 $x263 $x216 $x231 $x261 $x211 $x233 $x265 $x209 $x235 $x266 $x204 $x236 $x268 $x206 $x240 $x270 $x202 $x238 $x275 $x201 $x243 $x273 $x199 $x245 $x277))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert
 (let (($x530 (= flags 33488896)))
(let (($x529 (= flags 33423360)))
(let (($x526 (= flags 33357824)))
(let (($x537 (= flags 33292288)))
(let (($x541 (= flags 32964608)))
(let (($x545 (= flags 32899072)))
(let (($x542 (= flags 32833536)))
(let (($x533 (= flags 32768000)))
(let (($x523 (= flags 32440320)))
(let (($x521 (= flags 32374784)))
(let (($x520 (= flags 32309248)))
(let (($x517 (= flags 32243712)))
(let (($x518 (= flags 31916032)))
(let (($x512 (= flags 31850496)))
(let (($x511 (= flags 31784960)))
(let (($x509 (= flags 31719424)))
(let (($x508 (= flags 31391744)))
(let (($x505 (= flags 31326208)))
(let (($x506 (= flags 31260672)))
(let (($x500 (= flags 31195136)))
(let (($x499 (= flags 30867456)))
(let (($x497 (= flags 30801920)))
(let (($x496 (= flags 30736384)))
(let (($x493 (= flags 30670848)))
(let (($x494 (= flags 30343168)))
(let (($x488 (= flags 30277632)))
(let (($x487 (= flags 30212096)))
(let (($x485 (= flags 30146560)))
(let (($x484 (= flags 29818880)))
(let (($x481 (= flags 29753344)))
(let (($x482 (= flags 29687808)))
(let (($x476 (= flags 29622272)))
(let (($x475 (= flags 25100288)))
(let (($x473 (= flags 25034752)))
(let (($x472 (= flags 24969216)))
(let (($x469 (= flags 24903680)))
(let (($x470 (= flags 24576000)))
(let (($x464 (= flags 24510464)))
(let (($x463 (= flags 24444928)))
(let (($x461 (= flags 24379392)))
(let (($x460 (= flags 24051712)))
(let (($x457 (= flags 23986176)))
(let (($x458 (= flags 23920640)))
(let (($x452 (= flags 23855104)))
(let (($x451 (= flags 23527424)))
(let (($x449 (= flags 23461888)))
(let (($x448 (= flags 23396352)))
(let (($x445 (= flags 23330816)))
(let (($x446 (= flags 23003136)))
(let (($x440 (= flags 22937600)))
(let (($x439 (= flags 22872064)))
(let (($x437 (= flags 22806528)))
(let (($x436 (= flags 22478848)))
(let (($x433 (= flags 22413312)))
(let (($x434 (= flags 22347776)))
(let (($x428 (= flags 22282240)))
(let (($x427 (= flags 21954560)))
(let (($x425 (= flags 21889024)))
(let (($x424 (= flags 21823488)))
(let (($x421 (= flags 21757952)))
(let (($x422 (= flags 21430272)))
(let (($x416 (= flags 21364736)))
(let (($x415 (= flags 21299200)))
(let (($x413 (= flags 21233664)))
(let (($x412 (= flags 16711680)))
(let (($x409 (= flags 16646144)))
(let (($x410 (= flags 16580608)))
(let (($x404 (= flags 16515072)))
(let (($x403 (= flags 16187392)))
(let (($x401 (= flags 16121856)))
(let (($x400 (= flags 16056320)))
(let (($x397 (= flags 15990784)))
(let (($x398 (= flags 15663104)))
(let (($x392 (= flags 15597568)))
(let (($x391 (= flags 15532032)))
(let (($x389 (= flags 15466496)))
(let (($x388 (= flags 15138816)))
(let (($x385 (= flags 15073280)))
(let (($x386 (= flags 15007744)))
(let (($x380 (= flags 14942208)))
(let (($x379 (= flags 14614528)))
(let (($x377 (= flags 14548992)))
(let (($x376 (= flags 14483456)))
(let (($x373 (= flags 14417920)))
(let (($x374 (= flags 14090240)))
(let (($x368 (= flags 14024704)))
(let (($x367 (= flags 13959168)))
(let (($x362 (= flags 13893632)))
(let (($x364 (= flags 13565952)))
(let (($x361 (= flags 13500416)))
(let (($x360 (= flags 13434880)))
(let (($x356 (= flags 13369344)))
(let (($x355 (= flags 13041664)))
(let (($x354 (= flags 12976128)))
(let (($x350 (= flags 12910592)))
(let (($x352 (= flags 12845056)))
(let (($x348 (= flags 8323072)))
(let (($x344 (= flags 8257536)))
(let (($x340 (= flags 8192000)))
(let (($x342 (= flags 8126464)))
(let (($x338 (= flags 7798784)))
(let (($x334 (= flags 7733248)))
(let (($x336 (= flags 7667712)))
(let (($x332 (= flags 7602176)))
(let (($x335 (= flags 7274496)))
(let (($x328 (= flags 7208960)))
(let (($x330 (= flags 7143424)))
(let (($x325 (= flags 7077888)))
(let (($x321 (= flags 6750208)))
(let (($x320 (= flags 6684672)))
(let (($x317 (= flags 6619136)))
(let (($x319 (= flags 6553600)))
(let (($x314 (= flags 6225920)))
(let (($x189 (= flags 6160384)))
(let (($x288 (= flags 6094848)))
(let (($x284 (= flags 6029312)))
(let (($x286 (= flags 5701632)))
(let (($x290 (= flags 5636096)))
(let (($x292 (= flags 5570560)))
(let (($x294 (= flags 5505024)))
(let (($x295 (= flags 5177344)))
(let (($x297 (= flags 5111808)))
(let (($x298 (= flags 5046272)))
(let (($x305 (= flags 4980736)))
(let (($x304 (= flags 4653056)))
(let (($x307 (= flags 4587520)))
(let (($x312 (= flags 4521984)))
(let (($x309 (= flags 4456448)))
(or $x309 $x312 $x307 $x304 $x305 $x298 $x297 $x295 $x294 $x292 $x290 $x286 $x284 $x288 $x189 $x314 $x319 $x317 $x320 $x321 $x325 $x330 $x328 $x335 $x332 $x336 $x334 $x338 $x342 $x340 $x344 $x348 $x352 $x350 $x354 $x355 $x356 $x360 $x361 $x364 $x362 $x367 $x368 $x374 $x373 $x376 $x377 $x379 $x380 $x386 $x385 $x388 $x389 $x391 $x392 $x398 $x397 $x400 $x401 $x403 $x404 $x410 $x409 $x412 $x413 $x415 $x416 $x422 $x421 $x424 $x425 $x427 $x428 $x434 $x433 $x436 $x437 $x439 $x440 $x446 $x445 $x448 $x449 $x451 $x452 $x458 $x457 $x460 $x461 $x463 $x464 $x470 $x469 $x472 $x473 $x475 $x476 $x482 $x481 $x484 $x485 $x487 $x488 $x494 $x493 $x496 $x497 $x499 $x500 $x506 $x505 $x508 $x509 $x511 $x512 $x518 $x517 $x520 $x521 $x523 $x533 $x542 $x545 $x541 $x537 $x526 $x529 $x530))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

Implied Shell Flag Requires Shell Flag

🌳 tree-sitter VERIFIED

Function: parse_args · Z3 solved in 6595.1ms

MODE_IMPLIED_SHELL must not appear without MODE_SHELL in final option flags to preserve consistent shell-mode semantics.

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun flags () Int)
(assert
 (let (($x1059 (= flags 33488896)))
 (let (($x1057 (= flags 33423360)))
 (let (($x1055 (= flags 33226752)))
 (let (($x1053 (= flags 33161216)))
 (let (($x1051 (= flags 32964608)))
 (let (($x1049 (= flags 32899072)))
 (let (($x1047 (= flags 32833536)))
 (let (($x1045 (= flags 32768000)))
 (let (($x1043 (= flags 32702464)))
 (let (($x1041 (= flags 32636928)))
 (let (($x1039 (= flags 32571392)))
 (let (($x1037 (= flags 32505856)))
 (let (($x1035 (= flags 32440320)))
 (let (($x1033 (= flags 32374784)))
 (let (($x1031 (= flags 32178176)))
 (let (($x1029 (= flags 32112640)))
 (let (($x1027 (= flags 31916032)))
 (let (($x1025 (= flags 31850496)))
 (let (($x1023 (= flags 31784960)))
 (let (($x1021 (= flags 31719424)))
 (let (($x1019 (= flags 31653888)))
 (let (($x1017 (= flags 31588352)))
 (let (($x1015 (= flags 31522816)))
 (let (($x1013 (= flags 31457280)))
 (let (($x1011 (= flags 31391744)))
 (let (($x1009 (= flags 31326208)))
 (let (($x1007 (= flags 31129600)))
 (let (($x1005 (= flags 31064064)))
 (let (($x1003 (= flags 30867456)))
 (let (($x1001 (= flags 30801920)))
 (let (($x999 (= flags 30736384)))
 (let (($x997 (= flags 30670848)))
 (let (($x995 (= flags 30605312)))
 (let (($x993 (= flags 30539776)))
 (let (($x991 (= flags 30474240)))
 (let (($x989 (= flags 30408704)))
 (let (($x987 (= flags 30343168)))
 (let (($x985 (= flags 30277632)))
 (let (($x983 (= flags 30081024)))
 (let (($x981 (= flags 30015488)))
 (let (($x979 (= flags 29818880)))
 (let (($x977 (= flags 29753344)))
 (let (($x975 (= flags 29687808)))
 (let (($x973 (= flags 29622272)))
 (let (($x971 (= flags 29556736)))
 (let (($x969 (= flags 29491200)))
 (let (($x967 (= flags 29425664)))
 (let (($x965 (= flags 29360128)))
 (let (($x963 (= flags 29294592)))
 (let (($x961 (= flags 29229056)))
 (let (($x959 (= flags 29032448)))
 (let (($x957 (= flags 28966912)))
 (let (($x955 (= flags 28770304)))
 (let (($x953 (= flags 28704768)))
 (let (($x951 (= flags 28639232)))
 (let (($x949 (= flags 28573696)))
 (let (($x947 (= flags 28508160)))
 (let (($x945 (= flags 28442624)))
 (let (($x943 (= flags 28377088)))
 (let (($x941 (= flags 28311552)))
 (let (($x939 (= flags 28246016)))
 (let (($x937 (= flags 28180480)))
 (let (($x935 (= flags 27983872)))
 (let (($x933 (= flags 27918336)))
 (let (($x931 (= flags 27721728)))
 (let (($x929 (= flags 27656192)))
 (let (($x927 (= flags 27590656)))
 (let (($x925 (= flags 27525120)))
 (let (($x923 (= flags 27459584)))
 (let (($x921 (= flags 27394048)))
 (let (($x919 (= flags 27328512)))
 (let (($x917 (= flags 27262976)))
 (let (($x915 (= flags 27197440)))
 (let (($x913 (= flags 27131904)))
 (let (($x911 (= flags 26935296)))
 (let (($x909 (= flags 26869760)))
 (let (($x907 (= flags 26673152)))
 (let (($x905 (= flags 26607616)))
 (let (($x903 (= flags 26542080)))
 (let (($x901 (= flags 26476544)))
 (let (($x899 (= flags 26411008)))
 (let (($x897 (= flags 26345472)))
 (let (($x895 (= flags 26279936)))
 (let (($x893 (= flags 26214400)))
 (let (($x891 (= flags 26148864)))
 (let (($x889 (= flags 26083328)))
 (let (($x887 (= flags 25886720)))
 (let (($x885 (= flags 25821184)))
 (let (($x883 (= flags 25624576)))
 (let (($x881 (= flags 25559040)))
 (let (($x879 (= flags 25493504)))
 (let (($x877 (= flags 25427968)))
 (let (($x875 (= flags 25362432)))
 (let (($x873 (= flags 25296896)))
 (let (($x871 (= flags 25231360)))
 (let (($x869 (= flags 25165824)))
 (let (($x867 (= flags 25100288)))
 (let (($x865 (= flags 25034752)))
 (let (($x863 (= flags 24838144)))
 (let (($x861 (= flags 24772608)))
 (let (($x859 (= flags 24576000)))
 (let (($x857 (= flags 24510464)))
 (let (($x855 (= flags 24444928)))
 (let (($x853 (= flags 24379392)))
 (let (($x851 (= flags 24313856)))
 (let (($x849 (= flags 24248320)))
 (let (($x847 (= flags 24182784)))
 (let (($x845 (= flags 24117248)))
 (let (($x843 (= flags 24051712)))
 (let (($x840 (= flags 23986176)))
 (let (($x839 (= flags 23789568)))
 (let (($x837 (= flags 23724032)))
 (let (($x835 (= flags 23527424)))
 (let (($x833 (= flags 23461888)))
 (let (($x831 (= flags 23396352)))
 (let (($x829 (= flags 23330816)))
 (let (($x827 (= flags 23265280)))
 (let (($x824 (= flags 23199744)))
 (let (($x821 (= flags 23134208)))
 (let (($x820 (= flags 23068672)))
 (let (($x818 (= flags 23003136)))
 (let (($x816 (= flags 22937600)))
 (let (($x814 (= flags 22740992)))
 (let (($x812 (= flags 22675456)))
 (let (($x810 (= flags 22478848)))
 (let (($x808 (= flags 22413312)))
 (let (($x806 (= flags 22347776)))
 (let (($x792 (= flags 22282240)))
 (let (($x794 (= flags 22216704)))
 (let (($x797 (= flags 22151168)))
 (let (($x800 (= flags 22085632)))
 (let (($x803 (= flags 22020096)))
 (let (($x804 (= flags 21954560)))
 (let (($x805 (= flags 21889024)))
 (let (($x798 (= flags 21692416)))
 (let (($x788 (= flags 21626880)))
 (let (($x786 (= flags 21430272)))
 (let (($x783 (= flags 21364736)))
 (let (($x782 (= flags 21299200)))
 (let (($x780 (= flags 21233664)))
 (let (($x778 (= flags 21168128)))
 (let (($x776 (= flags 21102592)))
 (let (($x774 (= flags 21037056)))
 (let (($x772 (= flags 20971520)))
 (let (($x769 (= flags 20905984)))
 (let (($x768 (= flags 20840448)))
 (let (($x766 (= flags 20643840)))
 (let (($x765 (= flags 20578304)))
 (let (($x762 (= flags 20381696)))
 (let (($x760 (= flags 20316160)))
 (let (($x692 (= flags 20250624)))
 (let (($x758 (= flags 20185088)))
 (let (($x757 (= flags 20119552)))
 (let (($x689 (= flags 20054016)))
 (let (($x754 (= flags 19988480)))
 (let (($x753 (= flags 19922944)))
 (let (($x687 (= flags 19857408)))
 (let (($x750 (= flags 19791872)))
 (let (($x749 (= flags 19595264)))
 (let (($x685 (= flags 19529728)))
 (let (($x745 (= flags 19333120)))
 (let (($x746 (= flags 19267584)))
 (let (($x683 (= flags 19202048)))
 (let (($x742 (= flags 19136512)))
 (let (($x741 (= flags 19070976)))
 (let (($x681 (= flags 19005440)))
 (let (($x738 (= flags 18939904)))
 (let (($x737 (= flags 18874368)))
 (let (($x679 (= flags 18808832)))
 (let (($x734 (= flags 18743296)))
 (let (($x733 (= flags 18546688)))
 (let (($x677 (= flags 18481152)))
 (let (($x730 (= flags 18284544)))
 (let (($x729 (= flags 18219008)))
 (let (($x675 (= flags 18153472)))
 (let (($x725 (= flags 18087936)))
 (let (($x724 (= flags 18022400)))
 (let (($x673 (= flags 17956864)))
 (let (($x721 (= flags 17891328)))
 (let (($x720 (= flags 17825792)))
 (let (($x671 (= flags 17760256)))
 (let (($x717 (= flags 17694720)))
 (let (($x716 (= flags 17498112)))
 (let (($x669 (= flags 17432576)))
 (let (($x713 (= flags 17235968)))
 (let (($x712 (= flags 17170432)))
 (let (($x667 (= flags 17104896)))
 (let (($x709 (= flags 17039360)))
 (let (($x708 (= flags 16973824)))
 (let (($x665 (= flags 16908288)))
 (let (($x704 (= flags 16842752)))
 (let (($x703 (= flags 16777216)))
 (let (($x663 (= flags 16711680)))
 (let (($x700 (= flags 16646144)))
 (let (($x699 (= flags 16449536)))
 (let (($x661 (= flags 16384000)))
 (let (($x696 (= flags 16187392)))
 (let (($x695 (= flags 16121856)))
 (let (($x691 (= flags 16056320)))
 (let (($x658 (= flags 15990784)))
 (let (($x656 (= flags 15925248)))
 (let (($x591 (= flags 15859712)))
 (let (($x588 (= flags 15794176)))
 (let (($x651 (= flags 15728640)))
 (let (($x586 (= flags 15663104)))
 (let (($x646 (= flags 15597568)))
 (let (($x585 (= flags 15400960)))
 (let (($x645 (= flags 15335424)))
 (let (($x644 (= flags 15138816)))
 (let (($x643 (= flags 15073280)))
 (let (($x582 (= flags 15007744)))
 (let (($x638 (= flags 14942208)))
 (let (($x581 (= flags 14876672)))
 (let (($x637 (= flags 14811136)))
 (let (($x636 (= flags 14745600)))
 (let (($x635 (= flags 14680064)))
 (let (($x578 (= flags 14614528)))
 (let (($x630 (= flags 14548992)))
 (let (($x577 (= flags 14352384)))
 (let (($x629 (= flags 14286848)))
 (let (($x628 (= flags 14090240)))
 (let (($x627 (= flags 14024704)))
 (let (($x574 (= flags 13959168)))
 (let (($x622 (= flags 13893632)))
 (let (($x573 (= flags 13828096)))
 (let (($x621 (= flags 13762560)))
 (let (($x620 (= flags 13697024)))
 (let (($x619 (= flags 13631488)))
 (let (($x570 (= flags 13565952)))
 (let (($x614 (= flags 13500416)))
 (let (($x569 (= flags 13303808)))
 (let (($x613 (= flags 13238272)))
 (let (($x612 (= flags 13041664)))
 (let (($x611 (= flags 12976128)))
 (let (($x566 (= flags 12910592)))
 (let (($x606 (= flags 12845056)))
 (let (($x565 (= flags 12779520)))
 (let (($x605 (= flags 12713984)))
 (let (($x604 (= flags 12648448)))
 (let (($x603 (= flags 12582912)))
 (let (($x562 (= flags 12517376)))
 (let (($x598 (= flags 12451840)))
 (let (($x561 (= flags 12255232)))
 (let (($x597 (= flags 12189696)))
 (let (($x596 (= flags 11993088)))
 (let (($x595 (= flags 11927552)))
 (let (($x558 (= flags 11862016)))
 (let (($x555 (= flags 11796480)))
 (let (($x589 (= flags 11730944)))
 (let (($x554 (= flags 11665408)))
 (let (($x553 (= flags 11599872)))
 (let (($x551 (= flags 11534336)))
 (let (($x549 (= flags 11468800)))
 (let (($x544 (= flags 11403264)))
 (let (($x546 (= flags 11206656)))
 (let (($x525 (= flags 11141120)))
 (let (($x528 (= flags 10944512)))
 (let (($x531 (= flags 10878976)))
 (let (($x536 (= flags 10813440)))
 (let (($x540 (= flags 10747904)))
 (let (($x538 (= flags 10682368)))
 (let (($x524 (= flags 10616832)))
 (let (($x532 (= flags 10551296)))
 (let (($x527 (= flags 10485760)))
 (let (($x522 (= flags 10420224)))
 (let (($x514 (= flags 10354688)))
 (let (($x519 (= flags 10158080)))
 (let (($x516 (= flags 10092544)))
 (let (($x513 (= flags 9895936)))
 (let (($x515 (= flags 9830400)))
 (let (($x510 (= flags 9764864)))
 (let (($x502 (= flags 9699328)))
 (let (($x507 (= flags 9633792)))
 (let (($x504 (= flags 9568256)))
 (let (($x501 (= flags 9502720)))
 (let (($x503 (= flags 9437184)))
 (let (($x498 (= flags 9371648)))
 (let (($x490 (= flags 9306112)))
 (let (($x495 (= flags 9109504)))
 (let (($x492 (= flags 9043968)))
 (let (($x489 (= flags 8847360)))
 (let (($x491 (= flags 8781824)))
 (let (($x486 (= flags 8716288)))
 (let (($x478 (= flags 8650752)))
 (let (($x483 (= flags 8585216)))
 (let (($x480 (= flags 8519680)))
 (let (($x477 (= flags 8454144)))
 (let (($x479 (= flags 8388608)))
 (let (($x474 (= flags 8323072)))
 (let (($x466 (= flags 8257536)))
 (let (($x471 (= flags 8060928)))
 (let (($x468 (= flags 7995392)))
 (let (($x465 (= flags 7798784)))
 (let (($x467 (= flags 7733248)))
 (let (($x462 (= flags 7667712)))
 (let (($x454 (= flags 7602176)))
 (let (($x459 (= flags 7536640)))
 (let (($x456 (= flags 7471104)))
 (let (($x453 (= flags 7405568)))
 (let (($x455 (= flags 7340032)))
 (let (($x450 (= flags 7274496)))
 (let (($x442 (= flags 7208960)))
 (let (($x447 (= flags 7012352)))
 (let (($x444 (= flags 6946816)))
 (let (($x441 (= flags 6750208)))
 (let (($x443 (= flags 6684672)))
 (let (($x438 (= flags 6619136)))
 (let (($x430 (= flags 6553600)))
 (let (($x435 (= flags 6488064)))
 (let (($x432 (= flags 6422528)))
 (let (($x429 (= flags 6356992)))
 (let (($x431 (= flags 6291456)))
 (let (($x426 (= flags 6225920)))
 (let (($x418 (= flags 6160384)))
 (let (($x423 (= flags 5963776)))
 (let (($x420 (= flags 5898240)))
 (let (($x417 (= flags 5701632)))
 (let (($x419 (= flags 5636096)))
 (let (($x414 (= flags 5570560)))
 (let (($x406 (= flags 5505024)))
 (let (($x411 (= flags 5439488)))
 (let (($x408 (= flags 5373952)))
 (let (($x405 (= flags 5308416)))
 (let (($x407 (= flags 5242880)))
 (let (($x402 (= flags 5177344)))
 (let (($x394 (= flags 5111808)))
 (let (($x399 (= flags 4915200)))
 (let (($x396 (= flags 4849664)))
 (let (($x393 (= flags 4653056)))
 (let (($x395 (= flags 4587520)))
 (let (($x390 (= flags 4521984)))
 (let (($x382 (= flags 4456448)))
 (let (($x387 (= flags 4390912)))
 (let (($x384 (= flags 4325376)))
 (let (($x381 (= flags 4259840)))
 (let (($x383 (= flags 4194304)))
 (let (($x378 (= flags 4128768)))
 (let (($x370 (= flags 4063232)))
 (let (($x375 (= flags 3866624)))
 (let (($x372 (= flags 3801088)))
 (let (($x369 (= flags 3604480)))
 (let (($x371 (= flags 3538944)))
 (let (($x366 (= flags 3473408)))
 (let (($x365 (= flags 3407872)))
 (let (($x358 (= flags 3342336)))
 (let (($x363 (= flags 3276800)))
 (let (($x357 (= flags 3211264)))
 (let (($x359 (= flags 3145728)))
 (let (($x351 (= flags 3080192)))
 (let (($x353 (= flags 3014656)))
 (let (($x346 (= flags 2818048)))
 (let (($x349 (= flags 2752512)))
 (let (($x345 (= flags 2555904)))
 (let (($x347 (= flags 2490368)))
 (let (($x343 (= flags 2424832)))
 (let (($x339 (= flags 2359296)))
 (let (($x341 (= flags 2293760)))
 (let (($x337 (= flags 2228224)))
 (let (($x333 (= flags 2162688)))
 (let (($x329 (= flags 2097152)))
 (let (($x331 (= flags 2031616)))
 (let (($x327 (= flags 1966080)))
 (let (($x322 (= flags 1769472)))
 (let (($x324 (= flags 1703936)))
 (let (($x318 (= flags 1507328)))
 (let (($x323 (= flags 1441792)))
 (let (($x316 (= flags 1376256)))
 (let (($x315 (= flags 1310720)))
 (let (($x310 (= flags 1245184)))
 (let (($x283 (= flags 1179648)))
 (let (($x287 (= flags 1114112)))
 (let (($x289 (= flags 1048576)))
 (let (($x285 (= flags 983040)))
 (let (($x291 (= flags 917504)))
 (let (($x293 (= flags 720896)))
 (let (($x296 (= flags 655360)))
 (let (($x299 (= flags 458752)))
 (let (($x300 (= flags 393216)))
 (let (($x302 (= flags 327680)))
 (let (($x303 (= flags 262144)))
 (let (($x306 (= flags 196608)))
 (let (($x311 (= flags 131072)))
 (let (($x308 (= flags 65536)))
 (let (($x313 (= flags 0)))
 (or $x313 $x308 $x311 $x306 $x303 $x302 $x300 $x299 $x296 $x293 $x291 $x285 $x289 $x287 $x283 $x310 $x315 $x316 $x323 $x318 $x324 $x322 $x327 $x331 $x329 $x333 $x337 $x341 $x339 $x343 $x347 $x345 $x349 $x346 $x353 $x351 $x359 $x357 $x363 $x358 $x365 $x366 $x371 $x369 $x372 $x375 $x370 $x378 $x383 $x381 $x384 $x387 $x382 $x390 $x395 $x393 $x396 $x399 $x394 $x402 $x407 $x405 $x408 $x411 $x406 $x414 $x419 $x417 $x420 $x423 $x418 $x426 $x431 $x429 $x432 $x435 $x430 $x438 $x443 $x441 $x444 $x447 $x442 $x450 $x455 $x453 $x456 $x459 $x454 $x462 $x467 $x465 $x468 $x471 $x466 $x474 $x479 $x477 $x480 $x483 $x478 $x486 $x491 $x489 $x492 $x495 $x490 $x498 $x503 $x501 $x504 $x507 $x502 $x510 $x515 $x513 $x516 $x519 $x514 $x522 $x527 $x532 $x524 $x538 $x540 $x536 $x531 $x528 $x525 $x546 $x544 $x549 $x551 $x553 $x554 $x589 $x555 $x558 $x595 $x596 $x597 $x561 $x598 $x562 $x603 $x604 $x605 $x565 $x606 $x566 $x611 $x612 $x613 $x569 $x614 $x570 $x619 $x620 $x621 $x573 $x622 $x574 $x627 $x628 $x629 $x577 $x630 $x578 $x635 $x636 $x637 $x581 $x638 $x582 $x643 $x644 $x645 $x585 $x646 $x586 $x651 $x588 $x591 $x656 $x658 $x691 $x695 $x696 $x661 $x699 $x700 $x663 $x703 $x704 $x665 $x708 $x709 $x667 $x712 $x713 $x669 $x716 $x717 $x671 $x720 $x721 $x673 $x724 $x725 $x675 $x729 $x730 $x677 $x733 $x734 $x679 $x737 $x738 $x681 $x741 $x742 $x683 $x746 $x745 $x685 $x749 $x750 $x687 $x753 $x754 $x689 $x757 $x758 $x692 $x760 $x762 $x765 $x766 $x768 $x769 $x772 $x774 $x776 $x778 $x780 $x782 $x783 $x786 $x788 $x798 $x805 $x804 $x803 $x800 $x797 $x794 $x792 $x806 $x808 $x810 $x812 $x814 $x816 $x818 $x820 $x821 $x824 $x827 $x829 $x831 $x833 $x835 $x837 $x839 $x840 $x843 $x845 $x847 $x849 $x851 $x853 $x855 $x857 $x859 $x861 $x863 $x865 $x867 $x869 $x871 $x873 $x875 $x877 $x879 $x881 $x883 $x885 $x887 $x889 $x891 $x893 $x895 $x897 $x899 $x901 $x903 $x905 $x907 $x909 $x911 $x913 $x915 $x917 $x919 $x921 $x923 $x925 $x927 $x929 $x931 $x933 $x935 $x937 $x939 $x941 $x943 $x945 $x947 $x949 $x951 $x953 $x955 $x957 $x959 $x961 $x963 $x965 $x967 $x969 $x971 $x973 $x975 $x977 $x979 $x981 $x983 $x985 $x987 $x989 $x991 $x993 $x995 $x997 $x999 $x1001 $x1003 $x1005 $x1007 $x1009 $x1011 $x1013 $x1015 $x1017 $x1019 $x1021 $x1023 $x1025 $x1027 $x1029 $x1031 $x1033 $x1035 $x1037 $x1039 $x1041 $x1043 $x1045 $x1047 $x1049 $x1051 $x1053 $x1055 $x1057 $x1059))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert
 (let (($x193 (= flags 33357824)))
(let (($x251 (= flags 33292288)))
(let (($x248 (= flags 33095680)))
(let (($x249 (= flags 33030144)))
(let (($x281 (= flags 32309248)))
(let (($x191 (= flags 32243712)))
(let (($x282 (= flags 32047104)))
(let (($x195 (= flags 31981568)))
(let (($x246 (= flags 31260672)))
(let (($x198 (= flags 31195136)))
(let (($x276 (= flags 30998528)))
(let (($x244 (= flags 30932992)))
(let (($x200 (= flags 30212096)))
(let (($x272 (= flags 30146560)))
(let (($x242 (= flags 29949952)))
(let (($x205 (= flags 29884416)))
(let (($x271 (= flags 29163520)))
(let (($x241 (= flags 29097984)))
(let (($x203 (= flags 28901376)))
(let (($x269 (= flags 28835840)))
(let (($x237 (= flags 28114944)))
(let (($x207 (= flags 28049408)))
(let (($x267 (= flags 27852800)))
(let (($x239 (= flags 27787264)))
(let (($x208 (= flags 27066368)))
(let (($x262 (= flags 27000832)))
(let (($x234 (= flags 26804224)))
(let (($x210 (= flags 26738688)))
(let (($x264 (= flags 26017792)))
(let (($x232 (= flags 25952256)))
(let (($x212 (= flags 25755648)))
(let (($x260 (= flags 25690112)))
(let (($x230 (= flags 24969216)))
(let (($x213 (= flags 24903680)))
(let (($x259 (= flags 24707072)))
(let (($x229 (= flags 24641536)))
(let (($x217 (= flags 23920640)))
(let (($x257 (= flags 23855104)))
(let (($x225 (= flags 23658496)))
(let (($x215 (= flags 23592960)))
(let (($x255 (= flags 22872064)))
(let (($x227 (= flags 22806528)))
(let (($x220 (= flags 22609920)))
(let (($x250 (= flags 22544384)))
(let (($x222 (= flags 21823488)))
(let (($x108 (= flags 21757952)))
(let (($x190 (= flags 21561344)))
(let (($x177 (= flags 21495808)))
(let (($x155 (= flags 20774912)))
(let (($x176 (= flags 20709376)))
(let (($x152 (= flags 20512768)))
(let (($x151 (= flags 20447232)))
(let (($x150 (= flags 19726336)))
(let (($x184 (= flags 19660800)))
(let (($x183 (= flags 19464192)))
(let (($x182 (= flags 19398656)))
(let (($x178 (= flags 18677760)))
(let (($x145 (= flags 18612224)))
(let (($x144 (= flags 18415616)))
(let (($x171 (= flags 18350080)))
(let (($x163 (= flags 17629184)))
(let (($x170 (= flags 17563648)))
(let (($x134 (= flags 17367040)))
(let (($x133 (= flags 17301504)))
(let (($x132 (= flags 16580608)))
(let (($x175 (= flags 16515072)))
(let (($x174 (= flags 16318464)))
(let (($x173 (= flags 16252928)))
(let (($x146 (= flags 15532032)))
(let (($x139 (= flags 15466496)))
(let (($x137 (= flags 15269888)))
(let (($x140 (= flags 15204352)))
(let (($x138 (= flags 14483456)))
(let (($x158 (= flags 14417920)))
(let (($x185 (= flags 14221312)))
(let (($x162 (= flags 14155776)))
(let (($x107 (= flags 13434880)))
(let (($x95 (= flags 13369344)))
(let (($x96 (= flags 13172736)))
(let (($x97 (= flags 13107200)))
(let (($x101 (= flags 12386304)))
(let (($x102 (= flags 12320768)))
(let (($x103 (= flags 12124160)))
(let (($x539 (= flags 12058624)))
(let (($x535 (= flags 11337728)))
(let (($x114 (= flags 11272192)))
(let (($x120 (= flags 11075584)))
(let (($x119 (= flags 11010048)))
(let (($x118 (= flags 10289152)))
(let (($x113 (= flags 10223616)))
(let (($x111 (= flags 10027008)))
(let (($x109 (= flags 9961472)))
(let (($x90 (= flags 9240576)))
(let (($x88 (= flags 9175040)))
(let (($x86 (= flags 8978432)))
(let (($x84 (= flags 8912896)))
(let (($x82 (= flags 8192000)))
(let (($x80 (= flags 8126464)))
(let (($x78 (= flags 7929856)))
(let (($x76 (= flags 7864320)))
(let (($x74 (= flags 7143424)))
(let (($x72 (= flags 7077888)))
(let (($x70 (= flags 6881280)))
(let (($x68 (= flags 6815744)))
(let (($x66 (= flags 6094848)))
(let (($x64 (= flags 6029312)))
(let (($x52 (= flags 5832704)))
(let (($x59 (= flags 5767168)))
(let (($x62 (= flags 5046272)))
(let (($x58 (= flags 4980736)))
(let (($x56 (= flags 4784128)))
(let (($x51 (= flags 4718592)))
(let (($x19 (= flags 3997696)))
(let (($x42 (= flags 3932160)))
(let (($x41 (= flags 3735552)))
(let (($x21 (= flags 3670016)))
(let (($x18 (= flags 2949120)))
(let (($x8 (= flags 2883584)))
(let (($x38 (= flags 2686976)))
(let (($x40 (= flags 2621440)))
(let (($x301 (= flags 1900544)))
(let (($x326 (= flags 1835008)))
(let (($x655 (= flags 1638400)))
(let (($x43 (= flags 1572864)))
(let (($x13 (= flags 851968)))
(let (($x29 (= flags 786432)))
(let (($x130 (= flags 589824)))
(let (($x128 (= flags 524288)))
(or $x128 $x130 $x29 $x13 $x43 $x655 $x326 $x301 $x40 $x38 $x8 $x18 $x21 $x41 $x42 $x19 $x51 $x56 $x58 $x62 $x59 $x52 $x64 $x66 $x68 $x70 $x72 $x74 $x76 $x78 $x80 $x82 $x84 $x86 $x88 $x90 $x109 $x111 $x113 $x118 $x119 $x120 $x114 $x535 $x539 $x103 $x102 $x101 $x97 $x96 $x95 $x107 $x162 $x185 $x158 $x138 $x140 $x137 $x139 $x146 $x173 $x174 $x175 $x132 $x133 $x134 $x170 $x163 $x171 $x144 $x145 $x178 $x182 $x183 $x184 $x150 $x151 $x152 $x176 $x155 $x177 $x190 $x108 $x222 $x250 $x220 $x227 $x255 $x215 $x225 $x257 $x217 $x229 $x259 $x213 $x230 $x260 $x212 $x232 $x264 $x210 $x234 $x262 $x208 $x239 $x267 $x207 $x237 $x269 $x203 $x241 $x271 $x205 $x242 $x272 $x200 $x244 $x276 $x198 $x246 $x195 $x282 $x191 $x281 $x249 $x248 $x251 $x193))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

Option Flags Known-Bit Set (MODE_BACKGROUND..MODE_LONG_LIST)

🌳 tree-sitter VERIFIED

Function: parse_args · Z3 solved in 0.1ms

Option flags must not contain undefined bits outside the canonical MODE_* option-flag range in parse_args().

View SMT2 Constraints

; benchmark generated from python API
(set-info :status unknown)
(declare-fun flags () Int)
(assert
 (let (($x1058 (= flags 33488896)))
 (let (($x1056 (= flags 33423360)))
 (let (($x1054 (= flags 33357824)))
 (let (($x1052 (= flags 33292288)))
 (let (($x1050 (= flags 33226752)))
 (let (($x1048 (= flags 33161216)))
 (let (($x1046 (= flags 33095680)))
 (let (($x1044 (= flags 33030144)))
 (let (($x1042 (= flags 32964608)))
 (let (($x1040 (= flags 32899072)))
 (let (($x1038 (= flags 32833536)))
 (let (($x1036 (= flags 32768000)))
 (let (($x1034 (= flags 32702464)))
 (let (($x1032 (= flags 32636928)))
 (let (($x1030 (= flags 32571392)))
 (let (($x1028 (= flags 32505856)))
 (let (($x1026 (= flags 32440320)))
 (let (($x1024 (= flags 32374784)))
 (let (($x1022 (= flags 32309248)))
 (let (($x1020 (= flags 32243712)))
 (let (($x1018 (= flags 32178176)))
 (let (($x1016 (= flags 32112640)))
 (let (($x1014 (= flags 32047104)))
 (let (($x1012 (= flags 31981568)))
 (let (($x1010 (= flags 31916032)))
 (let (($x1008 (= flags 31850496)))
 (let (($x1006 (= flags 31784960)))
 (let (($x1004 (= flags 31719424)))
 (let (($x1002 (= flags 31653888)))
 (let (($x1000 (= flags 31588352)))
 (let (($x998 (= flags 31522816)))
 (let (($x996 (= flags 31457280)))
 (let (($x994 (= flags 31391744)))
 (let (($x992 (= flags 31326208)))
 (let (($x990 (= flags 31260672)))
 (let (($x988 (= flags 31195136)))
 (let (($x986 (= flags 31129600)))
 (let (($x984 (= flags 31064064)))
 (let (($x982 (= flags 30998528)))
 (let (($x980 (= flags 30932992)))
 (let (($x978 (= flags 30867456)))
 (let (($x976 (= flags 30801920)))
 (let (($x974 (= flags 30736384)))
 (let (($x972 (= flags 30670848)))
 (let (($x970 (= flags 30605312)))
 (let (($x968 (= flags 30539776)))
 (let (($x966 (= flags 30474240)))
 (let (($x964 (= flags 30408704)))
 (let (($x962 (= flags 30343168)))
 (let (($x960 (= flags 30277632)))
 (let (($x958 (= flags 30212096)))
 (let (($x956 (= flags 30146560)))
 (let (($x954 (= flags 30081024)))
 (let (($x952 (= flags 30015488)))
 (let (($x950 (= flags 29949952)))
 (let (($x948 (= flags 29884416)))
 (let (($x946 (= flags 29818880)))
 (let (($x944 (= flags 29753344)))
 (let (($x942 (= flags 29687808)))
 (let (($x940 (= flags 29622272)))
 (let (($x938 (= flags 29556736)))
 (let (($x936 (= flags 29491200)))
 (let (($x934 (= flags 29425664)))
 (let (($x932 (= flags 29360128)))
 (let (($x930 (= flags 29294592)))
 (let (($x928 (= flags 29229056)))
 (let (($x926 (= flags 29163520)))
 (let (($x924 (= flags 29097984)))
 (let (($x922 (= flags 29032448)))
 (let (($x920 (= flags 28966912)))
 (let (($x918 (= flags 28901376)))
 (let (($x916 (= flags 28835840)))
 (let (($x914 (= flags 28770304)))
 (let (($x912 (= flags 28704768)))
 (let (($x910 (= flags 28639232)))
 (let (($x908 (= flags 28573696)))
 (let (($x906 (= flags 28508160)))
 (let (($x904 (= flags 28442624)))
 (let (($x902 (= flags 28377088)))
 (let (($x900 (= flags 28311552)))
 (let (($x898 (= flags 28246016)))
 (let (($x896 (= flags 28180480)))
 (let (($x894 (= flags 28114944)))
 (let (($x892 (= flags 28049408)))
 (let (($x890 (= flags 27983872)))
 (let (($x888 (= flags 27918336)))
 (let (($x886 (= flags 27852800)))
 (let (($x884 (= flags 27787264)))
 (let (($x882 (= flags 27721728)))
 (let (($x880 (= flags 27656192)))
 (let (($x878 (= flags 27590656)))
 (let (($x876 (= flags 27525120)))
 (let (($x874 (= flags 27459584)))
 (let (($x872 (= flags 27394048)))
 (let (($x870 (= flags 27328512)))
 (let (($x868 (= flags 27262976)))
 (let (($x866 (= flags 27197440)))
 (let (($x864 (= flags 27131904)))
 (let (($x862 (= flags 27066368)))
 (let (($x860 (= flags 27000832)))
 (let (($x858 (= flags 26935296)))
 (let (($x856 (= flags 26869760)))
 (let (($x854 (= flags 26804224)))
 (let (($x852 (= flags 26738688)))
 (let (($x850 (= flags 26673152)))
 (let (($x848 (= flags 26607616)))
 (let (($x846 (= flags 26542080)))
 (let (($x844 (= flags 26476544)))
 (let (($x842 (= flags 26411008)))
 (let (($x841 (= flags 26345472)))
 (let (($x838 (= flags 26279936)))
 (let (($x836 (= flags 26214400)))
 (let (($x834 (= flags 26148864)))
 (let (($x832 (= flags 26083328)))
 (let (($x830 (= flags 26017792)))
 (let (($x828 (= flags 25952256)))
 (let (($x826 (= flags 25886720)))
 (let (($x823 (= flags 25821184)))
 (let (($x822 (= flags 25755648)))
 (let (($x819 (= flags 25690112)))
 (let (($x817 (= flags 25624576)))
 (let (($x815 (= flags 25559040)))
 (let (($x813 (= flags 25493504)))
 (let (($x811 (= flags 25427968)))
 (let (($x809 (= flags 25362432)))
 (let (($x807 (= flags 25296896)))
 (let (($x791 (= flags 25231360)))
 (let (($x793 (= flags 25165824)))
 (let (($x795 (= flags 25100288)))
 (let (($x799 (= flags 25034752)))
 (let (($x801 (= flags 24969216)))
 (let (($x802 (= flags 24903680)))
 (let (($x790 (= flags 24838144)))
 (let (($x796 (= flags 24772608)))
 (let (($x789 (= flags 24707072)))
 (let (($x787 (= flags 24641536)))
 (let (($x785 (= flags 24576000)))
 (let (($x784 (= flags 24510464)))
 (let (($x781 (= flags 24444928)))
 (let (($x779 (= flags 24379392)))
 (let (($x777 (= flags 24313856)))
 (let (($x775 (= flags 24248320)))
 (let (($x773 (= flags 24182784)))
 (let (($x771 (= flags 24117248)))
 (let (($x770 (= flags 24051712)))
 (let (($x767 (= flags 23986176)))
 (let (($x764 (= flags 23920640)))
 (let (($x763 (= flags 23855104)))
 (let (($x761 (= flags 23789568)))
 (let (($x693 (= flags 23724032)))
 (let (($x759 (= flags 23658496)))
 (let (($x690 (= flags 23592960)))
 (let (($x756 (= flags 23527424)))
 (let (($x755 (= flags 23461888)))
 (let (($x688 (= flags 23396352)))
 (let (($x752 (= flags 23330816)))
 (let (($x751 (= flags 23265280)))
 (let (($x686 (= flags 23199744)))
 (let (($x748 (= flags 23134208)))
 (let (($x747 (= flags 23068672)))
 (let (($x684 (= flags 23003136)))
 (let (($x744 (= flags 22937600)))
 (let (($x743 (= flags 22872064)))
 (let (($x682 (= flags 22806528)))
 (let (($x740 (= flags 22740992)))
 (let (($x739 (= flags 22675456)))
 (let (($x680 (= flags 22609920)))
 (let (($x736 (= flags 22544384)))
 (let (($x735 (= flags 22478848)))
 (let (($x678 (= flags 22413312)))
 (let (($x732 (= flags 22347776)))
 (let (($x731 (= flags 22282240)))
 (let (($x676 (= flags 22216704)))
 (let (($x728 (= flags 22151168)))
 (let (($x727 (= flags 22085632)))
 (let (($x674 (= flags 22020096)))
 (let (($x723 (= flags 21954560)))
 (let (($x722 (= flags 21889024)))
 (let (($x672 (= flags 21823488)))
 (let (($x719 (= flags 21757952)))
 (let (($x718 (= flags 21692416)))
 (let (($x670 (= flags 21626880)))
 (let (($x715 (= flags 21561344)))
 (let (($x714 (= flags 21495808)))
 (let (($x668 (= flags 21430272)))
 (let (($x711 (= flags 21364736)))
 (let (($x710 (= flags 21299200)))
 (let (($x666 (= flags 21233664)))
 (let (($x706 (= flags 21168128)))
 (let (($x705 (= flags 21102592)))
 (let (($x664 (= flags 21037056)))
 (let (($x702 (= flags 20971520)))
 (let (($x701 (= flags 20905984)))
 (let (($x662 (= flags 20840448)))
 (let (($x698 (= flags 20774912)))
 (let (($x697 (= flags 20709376)))
 (let (($x660 (= flags 20643840)))
 (let (($x694 (= flags 20578304)))
 (let (($x659 (= flags 20512768)))
 (let (($x657 (= flags 20447232)))
 (let (($x654 (= flags 20381696)))
 (let (($x590 (= flags 20316160)))
 (let (($x653 (= flags 20250624)))
 (let (($x650 (= flags 20185088)))
 (let (($x649 (= flags 20119552)))
 (let (($x648 (= flags 20054016)))
 (let (($x584 (= flags 19988480)))
 (let (($x647 (= flags 19922944)))
 (let (($x583 (= flags 19857408)))
 (let (($x642 (= flags 19791872)))
 (let (($x641 (= flags 19726336)))
 (let (($x640 (= flags 19660800)))
 (let (($x580 (= flags 19595264)))
 (let (($x639 (= flags 19529728)))
 (let (($x579 (= flags 19464192)))
 (let (($x634 (= flags 19398656)))
 (let (($x633 (= flags 19333120)))
 (let (($x632 (= flags 19267584)))
 (let (($x576 (= flags 19202048)))
 (let (($x631 (= flags 19136512)))
 (let (($x575 (= flags 19070976)))
 (let (($x626 (= flags 19005440)))
 (let (($x625 (= flags 18939904)))
 (let (($x624 (= flags 18874368)))
 (let (($x572 (= flags 18808832)))
 (let (($x623 (= flags 18743296)))
 (let (($x571 (= flags 18677760)))
 (let (($x618 (= flags 18612224)))
 (let (($x617 (= flags 18546688)))
 (let (($x616 (= flags 18481152)))
 (let (($x568 (= flags 18415616)))
 (let (($x615 (= flags 18350080)))
 (let (($x567 (= flags 18284544)))
 (let (($x610 (= flags 18219008)))
 (let (($x609 (= flags 18153472)))
 (let (($x608 (= flags 18087936)))
 (let (($x564 (= flags 18022400)))
 (let (($x607 (= flags 17956864)))
 (let (($x563 (= flags 17891328)))
 (let (($x602 (= flags 17825792)))
 (let (($x601 (= flags 17760256)))
 (let (($x600 (= flags 17694720)))
 (let (($x560 (= flags 17629184)))
 (let (($x599 (= flags 17563648)))
 (let (($x559 (= flags 17498112)))
 (let (($x594 (= flags 17432576)))
 (let (($x593 (= flags 17367040)))
 (let (($x592 (= flags 17301504)))
 (let (($x556 (= flags 17235968)))
 (let (($x557 (= flags 17170432)))
 (let (($x552 (= flags 17104896)))
 (let (($x550 (= flags 17039360)))
 (let (($x548 (= flags 16973824)))
 (let (($x547 (= flags 16908288)))
 (let (($x543 (= flags 16842752)))
 (let (($x530 (= flags 16777216)))
 (let (($x529 (= flags 16711680)))
 (let (($x526 (= flags 16646144)))
 (let (($x537 (= flags 16580608)))
 (let (($x541 (= flags 16515072)))
 (let (($x545 (= flags 16449536)))
 (let (($x542 (= flags 16384000)))
 (let (($x533 (= flags 16318464)))
 (let (($x523 (= flags 16252928)))
 (let (($x521 (= flags 16187392)))
 (let (($x520 (= flags 16121856)))
 (let (($x517 (= flags 16056320)))
 (let (($x518 (= flags 15990784)))
 (let (($x512 (= flags 15925248)))
 (let (($x511 (= flags 15859712)))
 (let (($x509 (= flags 15794176)))
 (let (($x508 (= flags 15728640)))
 (let (($x505 (= flags 15663104)))
 (let (($x506 (= flags 15597568)))
 (let (($x500 (= flags 15532032)))
 (let (($x499 (= flags 15466496)))
 (let (($x497 (= flags 15400960)))
 (let (($x496 (= flags 15335424)))
 (let (($x493 (= flags 15269888)))
 (let (($x494 (= flags 15204352)))
 (let (($x488 (= flags 15138816)))
 (let (($x487 (= flags 15073280)))
 (let (($x485 (= flags 15007744)))
 (let (($x484 (= flags 14942208)))
 (let (($x481 (= flags 14876672)))
 (let (($x482 (= flags 14811136)))
 (let (($x476 (= flags 14745600)))
 (let (($x475 (= flags 14680064)))
 (let (($x473 (= flags 14614528)))
 (let (($x472 (= flags 14548992)))
 (let (($x469 (= flags 14483456)))
 (let (($x470 (= flags 14417920)))
 (let (($x464 (= flags 14352384)))
 (let (($x463 (= flags 14286848)))
 (let (($x461 (= flags 14221312)))
 (let (($x460 (= flags 14155776)))
 (let (($x457 (= flags 14090240)))
 (let (($x458 (= flags 14024704)))
 (let (($x452 (= flags 13959168)))
 (let (($x451 (= flags 13893632)))
 (let (($x449 (= flags 13828096)))
 (let (($x448 (= flags 13762560)))
 (let (($x445 (= flags 13697024)))
 (let (($x446 (= flags 13631488)))
 (let (($x440 (= flags 13565952)))
 (let (($x439 (= flags 13500416)))
 (let (($x437 (= flags 13434880)))
 (let (($x436 (= flags 13369344)))
 (let (($x433 (= flags 13303808)))
 (let (($x434 (= flags 13238272)))
 (let (($x428 (= flags 13172736)))
 (let (($x427 (= flags 13107200)))
 (let (($x425 (= flags 13041664)))
 (let (($x424 (= flags 12976128)))
 (let (($x421 (= flags 12910592)))
 (let (($x422 (= flags 12845056)))
 (let (($x416 (= flags 12779520)))
 (let (($x415 (= flags 12713984)))
 (let (($x413 (= flags 12648448)))
 (let (($x412 (= flags 12582912)))
 (let (($x409 (= flags 12517376)))
 (let (($x410 (= flags 12451840)))
 (let (($x404 (= flags 12386304)))
 (let (($x403 (= flags 12320768)))
 (let (($x401 (= flags 12255232)))
 (let (($x400 (= flags 12189696)))
 (let (($x397 (= flags 12124160)))
 (let (($x398 (= flags 12058624)))
 (let (($x392 (= flags 11993088)))
 (let (($x391 (= flags 11927552)))
 (let (($x389 (= flags 11862016)))
 (let (($x388 (= flags 11796480)))
 (let (($x385 (= flags 11730944)))
 (let (($x386 (= flags 11665408)))
 (let (($x380 (= flags 11599872)))
 (let (($x379 (= flags 11534336)))
 (let (($x377 (= flags 11468800)))
 (let (($x376 (= flags 11403264)))
 (let (($x373 (= flags 11337728)))
 (let (($x374 (= flags 11272192)))
 (let (($x368 (= flags 11206656)))
 (let (($x367 (= flags 11141120)))
 (let (($x362 (= flags 11075584)))
 (let (($x364 (= flags 11010048)))
 (let (($x361 (= flags 10944512)))
 (let (($x360 (= flags 10878976)))
 (let (($x356 (= flags 10813440)))
 (let (($x355 (= flags 10747904)))
 (let (($x354 (= flags 10682368)))
 (let (($x350 (= flags 10616832)))
 (let (($x352 (= flags 10551296)))
 (let (($x348 (= flags 10485760)))
 (let (($x344 (= flags 10420224)))
 (let (($x340 (= flags 10354688)))
 (let (($x342 (= flags 10289152)))
 (let (($x338 (= flags 10223616)))
 (let (($x334 (= flags 10158080)))
 (let (($x336 (= flags 10092544)))
 (let (($x332 (= flags 10027008)))
 (let (($x335 (= flags 9961472)))
 (let (($x328 (= flags 9895936)))
 (let (($x330 (= flags 9830400)))
 (let (($x325 (= flags 9764864)))
 (let (($x321 (= flags 9699328)))
 (let (($x320 (= flags 9633792)))
 (let (($x317 (= flags 9568256)))
 (let (($x319 (= flags 9502720)))
 (let (($x314 (= flags 9437184)))
 (let (($x189 (= flags 9371648)))
 (let (($x288 (= flags 9306112)))
 (let (($x284 (= flags 9240576)))
 (let (($x286 (= flags 9175040)))
 (let (($x290 (= flags 9109504)))
 (let (($x292 (= flags 9043968)))
 (let (($x294 (= flags 8978432)))
 (let (($x295 (= flags 8912896)))
 (let (($x297 (= flags 8847360)))
 (let (($x298 (= flags 8781824)))
 (let (($x305 (= flags 8716288)))
 (let (($x304 (= flags 8650752)))
 (let (($x307 (= flags 8585216)))
 (let (($x312 (= flags 8519680)))
 (let (($x309 (= flags 8454144)))
 (let (($x247 (= flags 8388608)))
 (let (($x278 (= flags 8323072)))
 (let (($x196 (= flags 8257536)))
 (let (($x280 (= flags 8192000)))
 (let (($x192 (= flags 8126464)))
 (let (($x252 (= flags 8060928)))
 (let (($x274 (= flags 7995392)))
 (let (($x279 (= flags 7929856)))
 (let (($x197 (= flags 7864320)))
 (let (($x277 (= flags 7798784)))
 (let (($x245 (= flags 7733248)))
 (let (($x199 (= flags 7667712)))
 (let (($x273 (= flags 7602176)))
 (let (($x243 (= flags 7536640)))
 (let (($x201 (= flags 7471104)))
 (let (($x275 (= flags 7405568)))
 (let (($x238 (= flags 7340032)))
 (let (($x202 (= flags 7274496)))
 (let (($x270 (= flags 7208960)))
 (let (($x240 (= flags 7143424)))
 (let (($x206 (= flags 7077888)))
 (let (($x268 (= flags 7012352)))
 (let (($x236 (= flags 6946816)))
 (let (($x204 (= flags 6881280)))
 (let (($x266 (= flags 6815744)))
 (let (($x235 (= flags 6750208)))
 (let (($x209 (= flags 6684672)))
 (let (($x265 (= flags 6619136)))
 (let (($x233 (= flags 6553600)))
 (let (($x211 (= flags 6488064)))
 (let (($x261 (= flags 6422528)))
 (let (($x231 (= flags 6356992)))
 (let (($x216 (= flags 6291456)))
 (let (($x263 (= flags 6225920)))
 (let (($x226 (= flags 6160384)))
 (let (($x214 (= flags 6094848)))
 (let (($x258 (= flags 6029312)))
 (let (($x228 (= flags 5963776)))
 (let (($x218 (= flags 5898240)))
 (let (($x256 (= flags 5832704)))
 (let (($x224 (= flags 5767168)))
 (let (($x219 (= flags 5701632)))
 (let (($x254 (= flags 5636096)))
 (let (($x223 (= flags 5570560)))
 (let (($x221 (= flags 5505024)))
 (let (($x253 (= flags 5439488)))
 (let (($x194 (= flags 5373952)))
 (let (($x188 (= flags 5308416)))
 (let (($x187 (= flags 5242880)))
 (let (($x156 (= flags 5177344)))
 (let (($x154 (= flags 5111808)))
 (let (($x153 (= flags 5046272)))
 (let (($x168 (= flags 4980736)))
 (let (($x166 (= flags 4915200)))
 (let (($x164 (= flags 4849664)))
 (let (($x181 (= flags 4784128)))
 (let (($x180 (= flags 4718592)))
 (let (($x179 (= flags 4653056)))
 (let (($x143 (= flags 4587520)))
 (let (($x142 (= flags 4521984)))
 (let (($x172 (= flags 4456448)))
 (let (($x169 (= flags 4390912)))
 (let (($x165 (= flags 4325376)))
 (let (($x167 (= flags 4259840)))
 (let (($x161 (= flags 4194304)))
 (let (($x160 (= flags 4128768)))
 (let (($x159 (= flags 4063232)))
 (let (($x149 (= flags 3997696)))
 (let (($x148 (= flags 3932160)))
 (let (($x147 (= flags 3866624)))
 (let (($x131 (= flags 3801088)))
 (let (($x141 (= flags 3735552)))
 (let (($x136 (= flags 3670016)))
 (let (($x157 (= flags 3604480)))
 (let (($x135 (= flags 3538944)))
 (let (($x186 (= flags 3473408)))
 (let (($x92 (= flags 3407872)))
 (let (($x93 (= flags 3342336)))
 (let (($x94 (= flags 3276800)))
 (let (($x98 (= flags 3211264)))
 (let (($x99 (= flags 3145728)))
 (let (($x100 (= flags 3080192)))
 (let (($x104 (= flags 3014656)))
 (let (($x105 (= flags 2949120)))
 (let (($x534 (= flags 2883584)))
 (let (($x112 (= flags 2818048)))
 (let (($x121 (= flags 2752512)))
 (let (($x106 (= flags 2686976)))
 (let (($x117 (= flags 2621440)))
 (let (($x116 (= flags 2555904)))
 (let (($x115 (= flags 2490368)))
 (let (($x110 (= flags 2424832)))
 (let (($x91 (= flags 2359296)))
 (let (($x89 (= flags 2293760)))
 (let (($x87 (= flags 2228224)))
 (let (($x85 (= flags 2162688)))
 (let (($x83 (= flags 2097152)))
 (let (($x81 (= flags 2031616)))
 (let (($x79 (= flags 1966080)))
 (let (($x77 (= flags 1900544)))
 (let (($x75 (= flags 1835008)))
 (let (($x73 (= flags 1769472)))
 (let (($x71 (= flags 1703936)))
 (let (($x69 (= flags 1638400)))
 (let (($x67 (= flags 1572864)))
 (let (($x65 (= flags 1507328)))
 (let (($x53 (= flags 1441792)))
 (let (($x60 (= flags 1376256)))
 (let (($x63 (= flags 1310720)))
 (let (($x61 (= flags 1245184)))
 (let (($x57 (= flags 1179648)))
 (let (($x54 (= flags 1114112)))
 (let (($x55 (= flags 1048576)))
 (let (($x15 (= flags 983040)))
 (let (($x9 (= flags 917504)))
 (let (($x39 (= flags 851968)))
 (let (($x20 (= flags 786432)))
 (let (($x26 (= flags 720896)))
 (let (($x33 (= flags 655360)))
 (let (($x35 (= flags 589824)))
 (let (($x22 (= flags 524288)))
 (let (($x825 (= flags 458752)))
 (let (($x652 (= flags 393216)))
 (let (($x587 (= flags 327680)))
 (let (($x24 (= flags 262144)))
 (let (($x34 (= flags 196608)))
 (let (($x12 (= flags 131072)))
 (let (($x129 (= flags 65536)))
 (let (($x127 (= flags 0)))
 (or $x127 $x129 $x12 $x34 $x24 $x587 $x652 $x825 $x22 $x35 $x33 $x26 $x20 $x39 $x9 $x15 $x55 $x54 $x57 $x61 $x63 $x60 $x53 $x65 $x67 $x69 $x71 $x73 $x75 $x77 $x79 $x81 $x83 $x85 $x87 $x89 $x91 $x110 $x115 $x116 $x117 $x106 $x121 $x112 $x534 $x105 $x104 $x100 $x99 $x98 $x94 $x93 $x92 $x186 $x135 $x157 $x136 $x141 $x131 $x147 $x148 $x149 $x159 $x160 $x161 $x167 $x165 $x169 $x172 $x142 $x143 $x179 $x180 $x181 $x164 $x166 $x168 $x153 $x154 $x156 $x187 $x188 $x194 $x253 $x221 $x223 $x254 $x219 $x224 $x256 $x218 $x228 $x258 $x214 $x226 $x263 $x216 $x231 $x261 $x211 $x233 $x265 $x209 $x235 $x266 $x204 $x236 $x268 $x206 $x240 $x270 $x202 $x238 $x275 $x201 $x243 $x273 $x199 $x245 $x277 $x197 $x279 $x274 $x252 $x192 $x280 $x196 $x278 $x247 $x309 $x312 $x307 $x304 $x305 $x298 $x297 $x295 $x294 $x292 $x290 $x286 $x284 $x288 $x189 $x314 $x319 $x317 $x320 $x321 $x325 $x330 $x328 $x335 $x332 $x336 $x334 $x338 $x342 $x340 $x344 $x348 $x352 $x350 $x354 $x355 $x356 $x360 $x361 $x364 $x362 $x367 $x368 $x374 $x373 $x376 $x377 $x379 $x380 $x386 $x385 $x388 $x389 $x391 $x392 $x398 $x397 $x400 $x401 $x403 $x404 $x410 $x409 $x412 $x413 $x415 $x416 $x422 $x421 $x424 $x425 $x427 $x428 $x434 $x433 $x436 $x437 $x439 $x440 $x446 $x445 $x448 $x449 $x451 $x452 $x458 $x457 $x460 $x461 $x463 $x464 $x470 $x469 $x472 $x473 $x475 $x476 $x482 $x481 $x484 $x485 $x487 $x488 $x494 $x493 $x496 $x497 $x499 $x500 $x506 $x505 $x508 $x509 $x511 $x512 $x518 $x517 $x520 $x521 $x523 $x533 $x542 $x545 $x541 $x537 $x526 $x529 $x530 $x543 $x547 $x548 $x550 $x552 $x557 $x556 $x592 $x593 $x594 $x559 $x599 $x560 $x600 $x601 $x602 $x563 $x607 $x564 $x608 $x609 $x610 $x567 $x615 $x568 $x616 $x617 $x618 $x571 $x623 $x572 $x624 $x625 $x626 $x575 $x631 $x576 $x632 $x633 $x634 $x579 $x639 $x580 $x640 $x641 $x642 $x583 $x647 $x584 $x648 $x649 $x650 $x653 $x590 $x654 $x657 $x659 $x694 $x660 $x697 $x698 $x662 $x701 $x702 $x664 $x705 $x706 $x666 $x710 $x711 $x668 $x714 $x715 $x670 $x718 $x719 $x672 $x722 $x723 $x674 $x727 $x728 $x676 $x731 $x732 $x678 $x735 $x736 $x680 $x739 $x740 $x682 $x743 $x744 $x684 $x747 $x748 $x686 $x751 $x752 $x688 $x755 $x756 $x690 $x759 $x693 $x761 $x763 $x764 $x767 $x770 $x771 $x773 $x775 $x777 $x779 $x781 $x784 $x785 $x787 $x789 $x796 $x790 $x802 $x801 $x799 $x795 $x793 $x791 $x807 $x809 $x811 $x813 $x815 $x817 $x819 $x822 $x823 $x826 $x828 $x830 $x832 $x834 $x836 $x838 $x841 $x842 $x844 $x846 $x848 $x850 $x852 $x854 $x856 $x858 $x860 $x862 $x864 $x866 $x868 $x870 $x872 $x874 $x876 $x878 $x880 $x882 $x884 $x886 $x888 $x890 $x892 $x894 $x896 $x898 $x900 $x902 $x904 $x906 $x908 $x910 $x912 $x914 $x916 $x918 $x920 $x922 $x924 $x926 $x928 $x930 $x932 $x934 $x936 $x938 $x940 $x942 $x944 $x946 $x948 $x950 $x952 $x954 $x956 $x958 $x960 $x962 $x964 $x966 $x968 $x970 $x972 $x974 $x976 $x978 $x980 $x982 $x984 $x986 $x988 $x990 $x992 $x994 $x996 $x998 $x1000 $x1002 $x1004 $x1006 $x1008 $x1010 $x1012 $x1014 $x1016 $x1018 $x1020 $x1022 $x1024 $x1026 $x1028 $x1030 $x1032 $x1034 $x1036 $x1038 $x1040 $x1042 $x1044 $x1046 $x1048 $x1050 $x1052 $x1054 $x1056 $x1058))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert
 (let (($x1058 (= flags 33488896)))
(let (($x1056 (= flags 33423360)))
(let (($x1054 (= flags 33357824)))
(let (($x1052 (= flags 33292288)))
(let (($x1050 (= flags 33226752)))
(let (($x1048 (= flags 33161216)))
(let (($x1046 (= flags 33095680)))
(let (($x1044 (= flags 33030144)))
(let (($x1042 (= flags 32964608)))
(let (($x1040 (= flags 32899072)))
(let (($x1038 (= flags 32833536)))
(let (($x1036 (= flags 32768000)))
(let (($x1034 (= flags 32702464)))
(let (($x1032 (= flags 32636928)))
(let (($x1030 (= flags 32571392)))
(let (($x1028 (= flags 32505856)))
(let (($x1026 (= flags 32440320)))
(let (($x1024 (= flags 32374784)))
(let (($x1022 (= flags 32309248)))
(let (($x1020 (= flags 32243712)))
(let (($x1018 (= flags 32178176)))
(let (($x1016 (= flags 32112640)))
(let (($x1014 (= flags 32047104)))
(let (($x1012 (= flags 31981568)))
(let (($x1010 (= flags 31916032)))
(let (($x1008 (= flags 31850496)))
(let (($x1006 (= flags 31784960)))
(let (($x1004 (= flags 31719424)))
(let (($x1002 (= flags 31653888)))
(let (($x1000 (= flags 31588352)))
(let (($x998 (= flags 31522816)))
(let (($x996 (= flags 31457280)))
(let (($x994 (= flags 31391744)))
(let (($x992 (= flags 31326208)))
(let (($x990 (= flags 31260672)))
(let (($x988 (= flags 31195136)))
(let (($x986 (= flags 31129600)))
(let (($x984 (= flags 31064064)))
(let (($x982 (= flags 30998528)))
(let (($x980 (= flags 30932992)))
(let (($x978 (= flags 30867456)))
(let (($x976 (= flags 30801920)))
(let (($x974 (= flags 30736384)))
(let (($x972 (= flags 30670848)))
(let (($x970 (= flags 30605312)))
(let (($x968 (= flags 30539776)))
(let (($x966 (= flags 30474240)))
(let (($x964 (= flags 30408704)))
(let (($x962 (= flags 30343168)))
(let (($x960 (= flags 30277632)))
(let (($x958 (= flags 30212096)))
(let (($x956 (= flags 30146560)))
(let (($x954 (= flags 30081024)))
(let (($x952 (= flags 30015488)))
(let (($x950 (= flags 29949952)))
(let (($x948 (= flags 29884416)))
(let (($x946 (= flags 29818880)))
(let (($x944 (= flags 29753344)))
(let (($x942 (= flags 29687808)))
(let (($x940 (= flags 29622272)))
(let (($x938 (= flags 29556736)))
(let (($x936 (= flags 29491200)))
(let (($x934 (= flags 29425664)))
(let (($x932 (= flags 29360128)))
(let (($x930 (= flags 29294592)))
(let (($x928 (= flags 29229056)))
(let (($x926 (= flags 29163520)))
(let (($x924 (= flags 29097984)))
(let (($x922 (= flags 29032448)))
(let (($x920 (= flags 28966912)))
(let (($x918 (= flags 28901376)))
(let (($x916 (= flags 28835840)))
(let (($x914 (= flags 28770304)))
(let (($x912 (= flags 28704768)))
(let (($x910 (= flags 28639232)))
(let (($x908 (= flags 28573696)))
(let (($x906 (= flags 28508160)))
(let (($x904 (= flags 28442624)))
(let (($x902 (= flags 28377088)))
(let (($x900 (= flags 28311552)))
(let (($x898 (= flags 28246016)))
(let (($x896 (= flags 28180480)))
(let (($x894 (= flags 28114944)))
(let (($x892 (= flags 28049408)))
(let (($x890 (= flags 27983872)))
(let (($x888 (= flags 27918336)))
(let (($x886 (= flags 27852800)))
(let (($x884 (= flags 27787264)))
(let (($x882 (= flags 27721728)))
(let (($x880 (= flags 27656192)))
(let (($x878 (= flags 27590656)))
(let (($x876 (= flags 27525120)))
(let (($x874 (= flags 27459584)))
(let (($x872 (= flags 27394048)))
(let (($x870 (= flags 27328512)))
(let (($x868 (= flags 27262976)))
(let (($x866 (= flags 27197440)))
(let (($x864 (= flags 27131904)))
(let (($x862 (= flags 27066368)))
(let (($x860 (= flags 27000832)))
(let (($x858 (= flags 26935296)))
(let (($x856 (= flags 26869760)))
(let (($x854 (= flags 26804224)))
(let (($x852 (= flags 26738688)))
(let (($x850 (= flags 26673152)))
(let (($x848 (= flags 26607616)))
(let (($x846 (= flags 26542080)))
(let (($x844 (= flags 26476544)))
(let (($x842 (= flags 26411008)))
(let (($x841 (= flags 26345472)))
(let (($x838 (= flags 26279936)))
(let (($x836 (= flags 26214400)))
(let (($x834 (= flags 26148864)))
(let (($x832 (= flags 26083328)))
(let (($x830 (= flags 26017792)))
(let (($x828 (= flags 25952256)))
(let (($x826 (= flags 25886720)))
(let (($x823 (= flags 25821184)))
(let (($x822 (= flags 25755648)))
(let (($x819 (= flags 25690112)))
(let (($x817 (= flags 25624576)))
(let (($x815 (= flags 25559040)))
(let (($x813 (= flags 25493504)))
(let (($x811 (= flags 25427968)))
(let (($x809 (= flags 25362432)))
(let (($x807 (= flags 25296896)))
(let (($x791 (= flags 25231360)))
(let (($x793 (= flags 25165824)))
(let (($x795 (= flags 25100288)))
(let (($x799 (= flags 25034752)))
(let (($x801 (= flags 24969216)))
(let (($x802 (= flags 24903680)))
(let (($x790 (= flags 24838144)))
(let (($x796 (= flags 24772608)))
(let (($x789 (= flags 24707072)))
(let (($x787 (= flags 24641536)))
(let (($x785 (= flags 24576000)))
(let (($x784 (= flags 24510464)))
(let (($x781 (= flags 24444928)))
(let (($x779 (= flags 24379392)))
(let (($x777 (= flags 24313856)))
(let (($x775 (= flags 24248320)))
(let (($x773 (= flags 24182784)))
(let (($x771 (= flags 24117248)))
(let (($x770 (= flags 24051712)))
(let (($x767 (= flags 23986176)))
(let (($x764 (= flags 23920640)))
(let (($x763 (= flags 23855104)))
(let (($x761 (= flags 23789568)))
(let (($x693 (= flags 23724032)))
(let (($x759 (= flags 23658496)))
(let (($x690 (= flags 23592960)))
(let (($x756 (= flags 23527424)))
(let (($x755 (= flags 23461888)))
(let (($x688 (= flags 23396352)))
(let (($x752 (= flags 23330816)))
(let (($x751 (= flags 23265280)))
(let (($x686 (= flags 23199744)))
(let (($x748 (= flags 23134208)))
(let (($x747 (= flags 23068672)))
(let (($x684 (= flags 23003136)))
(let (($x744 (= flags 22937600)))
(let (($x743 (= flags 22872064)))
(let (($x682 (= flags 22806528)))
(let (($x740 (= flags 22740992)))
(let (($x739 (= flags 22675456)))
(let (($x680 (= flags 22609920)))
(let (($x736 (= flags 22544384)))
(let (($x735 (= flags 22478848)))
(let (($x678 (= flags 22413312)))
(let (($x732 (= flags 22347776)))
(let (($x731 (= flags 22282240)))
(let (($x676 (= flags 22216704)))
(let (($x728 (= flags 22151168)))
(let (($x727 (= flags 22085632)))
(let (($x674 (= flags 22020096)))
(let (($x723 (= flags 21954560)))
(let (($x722 (= flags 21889024)))
(let (($x672 (= flags 21823488)))
(let (($x719 (= flags 21757952)))
(let (($x718 (= flags 21692416)))
(let (($x670 (= flags 21626880)))
(let (($x715 (= flags 21561344)))
(let (($x714 (= flags 21495808)))
(let (($x668 (= flags 21430272)))
(let (($x711 (= flags 21364736)))
(let (($x710 (= flags 21299200)))
(let (($x666 (= flags 21233664)))
(let (($x706 (= flags 21168128)))
(let (($x705 (= flags 21102592)))
(let (($x664 (= flags 21037056)))
(let (($x702 (= flags 20971520)))
(let (($x701 (= flags 20905984)))
(let (($x662 (= flags 20840448)))
(let (($x698 (= flags 20774912)))
(let (($x697 (= flags 20709376)))
(let (($x660 (= flags 20643840)))
(let (($x694 (= flags 20578304)))
(let (($x659 (= flags 20512768)))
(let (($x657 (= flags 20447232)))
(let (($x654 (= flags 20381696)))
(let (($x590 (= flags 20316160)))
(let (($x653 (= flags 20250624)))
(let (($x650 (= flags 20185088)))
(let (($x649 (= flags 20119552)))
(let (($x648 (= flags 20054016)))
(let (($x584 (= flags 19988480)))
(let (($x647 (= flags 19922944)))
(let (($x583 (= flags 19857408)))
(let (($x642 (= flags 19791872)))
(let (($x641 (= flags 19726336)))
(let (($x640 (= flags 19660800)))
(let (($x580 (= flags 19595264)))
(let (($x639 (= flags 19529728)))
(let (($x579 (= flags 19464192)))
(let (($x634 (= flags 19398656)))
(let (($x633 (= flags 19333120)))
(let (($x632 (= flags 19267584)))
(let (($x576 (= flags 19202048)))
(let (($x631 (= flags 19136512)))
(let (($x575 (= flags 19070976)))
(let (($x626 (= flags 19005440)))
(let (($x625 (= flags 18939904)))
(let (($x624 (= flags 18874368)))
(let (($x572 (= flags 18808832)))
(let (($x623 (= flags 18743296)))
(let (($x571 (= flags 18677760)))
(let (($x618 (= flags 18612224)))
(let (($x617 (= flags 18546688)))
(let (($x616 (= flags 18481152)))
(let (($x568 (= flags 18415616)))
(let (($x615 (= flags 18350080)))
(let (($x567 (= flags 18284544)))
(let (($x610 (= flags 18219008)))
(let (($x609 (= flags 18153472)))
(let (($x608 (= flags 18087936)))
(let (($x564 (= flags 18022400)))
(let (($x607 (= flags 17956864)))
(let (($x563 (= flags 17891328)))
(let (($x602 (= flags 17825792)))
(let (($x601 (= flags 17760256)))
(let (($x600 (= flags 17694720)))
(let (($x560 (= flags 17629184)))
(let (($x599 (= flags 17563648)))
(let (($x559 (= flags 17498112)))
(let (($x594 (= flags 17432576)))
(let (($x593 (= flags 17367040)))
(let (($x592 (= flags 17301504)))
(let (($x556 (= flags 17235968)))
(let (($x557 (= flags 17170432)))
(let (($x552 (= flags 17104896)))
(let (($x550 (= flags 17039360)))
(let (($x548 (= flags 16973824)))
(let (($x547 (= flags 16908288)))
(let (($x543 (= flags 16842752)))
(let (($x530 (= flags 16777216)))
(let (($x529 (= flags 16711680)))
(let (($x526 (= flags 16646144)))
(let (($x537 (= flags 16580608)))
(let (($x541 (= flags 16515072)))
(let (($x545 (= flags 16449536)))
(let (($x542 (= flags 16384000)))
(let (($x533 (= flags 16318464)))
(let (($x523 (= flags 16252928)))
(let (($x521 (= flags 16187392)))
(let (($x520 (= flags 16121856)))
(let (($x517 (= flags 16056320)))
(let (($x518 (= flags 15990784)))
(let (($x512 (= flags 15925248)))
(let (($x511 (= flags 15859712)))
(let (($x509 (= flags 15794176)))
(let (($x508 (= flags 15728640)))
(let (($x505 (= flags 15663104)))
(let (($x506 (= flags 15597568)))
(let (($x500 (= flags 15532032)))
(let (($x499 (= flags 15466496)))
(let (($x497 (= flags 15400960)))
(let (($x496 (= flags 15335424)))
(let (($x493 (= flags 15269888)))
(let (($x494 (= flags 15204352)))
(let (($x488 (= flags 15138816)))
(let (($x487 (= flags 15073280)))
(let (($x485 (= flags 15007744)))
(let (($x484 (= flags 14942208)))
(let (($x481 (= flags 14876672)))
(let (($x482 (= flags 14811136)))
(let (($x476 (= flags 14745600)))
(let (($x475 (= flags 14680064)))
(let (($x473 (= flags 14614528)))
(let (($x472 (= flags 14548992)))
(let (($x469 (= flags 14483456)))
(let (($x470 (= flags 14417920)))
(let (($x464 (= flags 14352384)))
(let (($x463 (= flags 14286848)))
(let (($x461 (= flags 14221312)))
(let (($x460 (= flags 14155776)))
(let (($x457 (= flags 14090240)))
(let (($x458 (= flags 14024704)))
(let (($x452 (= flags 13959168)))
(let (($x451 (= flags 13893632)))
(let (($x449 (= flags 13828096)))
(let (($x448 (= flags 13762560)))
(let (($x445 (= flags 13697024)))
(let (($x446 (= flags 13631488)))
(let (($x440 (= flags 13565952)))
(let (($x439 (= flags 13500416)))
(let (($x437 (= flags 13434880)))
(let (($x436 (= flags 13369344)))
(let (($x433 (= flags 13303808)))
(let (($x434 (= flags 13238272)))
(let (($x428 (= flags 13172736)))
(let (($x427 (= flags 13107200)))
(let (($x425 (= flags 13041664)))
(let (($x424 (= flags 12976128)))
(let (($x421 (= flags 12910592)))
(let (($x422 (= flags 12845056)))
(let (($x416 (= flags 12779520)))
(let (($x415 (= flags 12713984)))
(let (($x413 (= flags 12648448)))
(let (($x412 (= flags 12582912)))
(let (($x409 (= flags 12517376)))
(let (($x410 (= flags 12451840)))
(let (($x404 (= flags 12386304)))
(let (($x403 (= flags 12320768)))
(let (($x401 (= flags 12255232)))
(let (($x400 (= flags 12189696)))
(let (($x397 (= flags 12124160)))
(let (($x398 (= flags 12058624)))
(let (($x392 (= flags 11993088)))
(let (($x391 (= flags 11927552)))
(let (($x389 (= flags 11862016)))
(let (($x388 (= flags 11796480)))
(let (($x385 (= flags 11730944)))
(let (($x386 (= flags 11665408)))
(let (($x380 (= flags 11599872)))
(let (($x379 (= flags 11534336)))
(let (($x377 (= flags 11468800)))
(let (($x376 (= flags 11403264)))
(let (($x373 (= flags 11337728)))
(let (($x374 (= flags 11272192)))
(let (($x368 (= flags 11206656)))
(let (($x367 (= flags 11141120)))
(let (($x362 (= flags 11075584)))
(let (($x364 (= flags 11010048)))
(let (($x361 (= flags 10944512)))
(let (($x360 (= flags 10878976)))
(let (($x356 (= flags 10813440)))
(let (($x355 (= flags 10747904)))
(let (($x354 (= flags 10682368)))
(let (($x350 (= flags 10616832)))
(let (($x352 (= flags 10551296)))
(let (($x348 (= flags 10485760)))
(let (($x344 (= flags 10420224)))
(let (($x340 (= flags 10354688)))
(let (($x342 (= flags 10289152)))
(let (($x338 (= flags 10223616)))
(let (($x334 (= flags 10158080)))
(let (($x336 (= flags 10092544)))
(let (($x332 (= flags 10027008)))
(let (($x335 (= flags 9961472)))
(let (($x328 (= flags 9895936)))
(let (($x330 (= flags 9830400)))
(let (($x325 (= flags 9764864)))
(let (($x321 (= flags 9699328)))
(let (($x320 (= flags 9633792)))
(let (($x317 (= flags 9568256)))
(let (($x319 (= flags 9502720)))
(let (($x314 (= flags 9437184)))
(let (($x189 (= flags 9371648)))
(let (($x288 (= flags 9306112)))
(let (($x284 (= flags 9240576)))
(let (($x286 (= flags 9175040)))
(let (($x290 (= flags 9109504)))
(let (($x292 (= flags 9043968)))
(let (($x294 (= flags 8978432)))
(let (($x295 (= flags 8912896)))
(let (($x297 (= flags 8847360)))
(let (($x298 (= flags 8781824)))
(let (($x305 (= flags 8716288)))
(let (($x304 (= flags 8650752)))
(let (($x307 (= flags 8585216)))
(let (($x312 (= flags 8519680)))
(let (($x309 (= flags 8454144)))
(let (($x247 (= flags 8388608)))
(let (($x278 (= flags 8323072)))
(let (($x196 (= flags 8257536)))
(let (($x280 (= flags 8192000)))
(let (($x192 (= flags 8126464)))
(let (($x252 (= flags 8060928)))
(let (($x274 (= flags 7995392)))
(let (($x279 (= flags 7929856)))
(let (($x197 (= flags 7864320)))
(let (($x277 (= flags 7798784)))
(let (($x245 (= flags 7733248)))
(let (($x199 (= flags 7667712)))
(let (($x273 (= flags 7602176)))
(let (($x243 (= flags 7536640)))
(let (($x201 (= flags 7471104)))
(let (($x275 (= flags 7405568)))
(let (($x238 (= flags 7340032)))
(let (($x202 (= flags 7274496)))
(let (($x270 (= flags 7208960)))
(let (($x240 (= flags 7143424)))
(let (($x206 (= flags 7077888)))
(let (($x268 (= flags 7012352)))
(let (($x236 (= flags 6946816)))
(let (($x204 (= flags 6881280)))
(let (($x266 (= flags 6815744)))
(let (($x235 (= flags 6750208)))
(let (($x209 (= flags 6684672)))
(let (($x265 (= flags 6619136)))
(let (($x233 (= flags 6553600)))
(let (($x211 (= flags 6488064)))
(let (($x261 (= flags 6422528)))
(let (($x231 (= flags 6356992)))
(let (($x216 (= flags 6291456)))
(let (($x263 (= flags 6225920)))
(let (($x226 (= flags 6160384)))
(let (($x214 (= flags 6094848)))
(let (($x258 (= flags 6029312)))
(let (($x228 (= flags 5963776)))
(let (($x218 (= flags 5898240)))
(let (($x256 (= flags 5832704)))
(let (($x224 (= flags 5767168)))
(let (($x219 (= flags 5701632)))
(let (($x254 (= flags 5636096)))
(let (($x223 (= flags 5570560)))
(let (($x221 (= flags 5505024)))
(let (($x253 (= flags 5439488)))
(let (($x194 (= flags 5373952)))
(let (($x188 (= flags 5308416)))
(let (($x187 (= flags 5242880)))
(let (($x156 (= flags 5177344)))
(let (($x154 (= flags 5111808)))
(let (($x153 (= flags 5046272)))
(let (($x168 (= flags 4980736)))
(let (($x166 (= flags 4915200)))
(let (($x164 (= flags 4849664)))
(let (($x181 (= flags 4784128)))
(let (($x180 (= flags 4718592)))
(let (($x179 (= flags 4653056)))
(let (($x143 (= flags 4587520)))
(let (($x142 (= flags 4521984)))
(let (($x172 (= flags 4456448)))
(let (($x169 (= flags 4390912)))
(let (($x165 (= flags 4325376)))
(let (($x167 (= flags 4259840)))
(let (($x161 (= flags 4194304)))
(let (($x160 (= flags 4128768)))
(let (($x159 (= flags 4063232)))
(let (($x149 (= flags 3997696)))
(let (($x148 (= flags 3932160)))
(let (($x147 (= flags 3866624)))
(let (($x131 (= flags 3801088)))
(let (($x141 (= flags 3735552)))
(let (($x136 (= flags 3670016)))
(let (($x157 (= flags 3604480)))
(let (($x135 (= flags 3538944)))
(let (($x186 (= flags 3473408)))
(let (($x92 (= flags 3407872)))
(let (($x93 (= flags 3342336)))
(let (($x94 (= flags 3276800)))
(let (($x98 (= flags 3211264)))
(let (($x99 (= flags 3145728)))
(let (($x100 (= flags 3080192)))
(let (($x104 (= flags 3014656)))
(let (($x105 (= flags 2949120)))
(let (($x534 (= flags 2883584)))
(let (($x112 (= flags 2818048)))
(let (($x121 (= flags 2752512)))
(let (($x106 (= flags 2686976)))
(let (($x117 (= flags 2621440)))
(let (($x116 (= flags 2555904)))
(let (($x115 (= flags 2490368)))
(let (($x110 (= flags 2424832)))
(let (($x91 (= flags 2359296)))
(let (($x89 (= flags 2293760)))
(let (($x87 (= flags 2228224)))
(let (($x85 (= flags 2162688)))
(let (($x83 (= flags 2097152)))
(let (($x81 (= flags 2031616)))
(let (($x79 (= flags 1966080)))
(let (($x77 (= flags 1900544)))
(let (($x75 (= flags 1835008)))
(let (($x73 (= flags 1769472)))
(let (($x71 (= flags 1703936)))
(let (($x69 (= flags 1638400)))
(let (($x67 (= flags 1572864)))
(let (($x65 (= flags 1507328)))
(let (($x53 (= flags 1441792)))
(let (($x60 (= flags 1376256)))
(let (($x63 (= flags 1310720)))
(let (($x61 (= flags 1245184)))
(let (($x57 (= flags 1179648)))
(let (($x54 (= flags 1114112)))
(let (($x55 (= flags 1048576)))
(let (($x15 (= flags 983040)))
(let (($x9 (= flags 917504)))
(let (($x39 (= flags 851968)))
(let (($x20 (= flags 786432)))
(let (($x26 (= flags 720896)))
(let (($x33 (= flags 655360)))
(let (($x35 (= flags 589824)))
(let (($x22 (= flags 524288)))
(let (($x825 (= flags 458752)))
(let (($x652 (= flags 393216)))
(let (($x587 (= flags 327680)))
(let (($x24 (= flags 262144)))
(let (($x34 (= flags 196608)))
(let (($x12 (= flags 131072)))
(let (($x129 (= flags 65536)))
(let (($x127 (= flags 0)))
(let (($x1059 (or $x127 $x129 $x12 $x34 $x24 $x587 $x652 $x825 $x22 $x35 $x33 $x26 $x20 $x39 $x9 $x15 $x55 $x54 $x57 $x61 $x63 $x60 $x53 $x65 $x67 $x69 $x71 $x73 $x75 $x77 $x79 $x81 $x83 $x85 $x87 $x89 $x91 $x110 $x115 $x116 $x117 $x106 $x121 $x112 $x534 $x105 $x104 $x100 $x99 $x98 $x94 $x93 $x92 $x186 $x135 $x157 $x136 $x141 $x131 $x147 $x148 $x149 $x159 $x160 $x161 $x167 $x165 $x169 $x172 $x142 $x143 $x179 $x180 $x181 $x164 $x166 $x168 $x153 $x154 $x156 $x187 $x188 $x194 $x253 $x221 $x223 $x254 $x219 $x224 $x256 $x218 $x228 $x258 $x214 $x226 $x263 $x216 $x231 $x261 $x211 $x233 $x265 $x209 $x235 $x266 $x204 $x236 $x268 $x206 $x240 $x270 $x202 $x238 $x275 $x201 $x243 $x273 $x199 $x245 $x277 $x197 $x279 $x274 $x252 $x192 $x280 $x196 $x278 $x247 $x309 $x312 $x307 $x304 $x305 $x298 $x297 $x295 $x294 $x292 $x290 $x286 $x284 $x288 $x189 $x314 $x319 $x317 $x320 $x321 $x325 $x330 $x328 $x335 $x332 $x336 $x334 $x338 $x342 $x340 $x344 $x348 $x352 $x350 $x354 $x355 $x356 $x360 $x361 $x364 $x362 $x367 $x368 $x374 $x373 $x376 $x377 $x379 $x380 $x386 $x385 $x388 $x389 $x391 $x392 $x398 $x397 $x400 $x401 $x403 $x404 $x410 $x409 $x412 $x413 $x415 $x416 $x422 $x421 $x424 $x425 $x427 $x428 $x434 $x433 $x436 $x437 $x439 $x440 $x446 $x445 $x448 $x449 $x451 $x452 $x458 $x457 $x460 $x461 $x463 $x464 $x470 $x469 $x472 $x473 $x475 $x476 $x482 $x481 $x484 $x485 $x487 $x488 $x494 $x493 $x496 $x497 $x499 $x500 $x506 $x505 $x508 $x509 $x511 $x512 $x518 $x517 $x520 $x521 $x523 $x533 $x542 $x545 $x541 $x537 $x526 $x529 $x530 $x543 $x547 $x548 $x550 $x552 $x557 $x556 $x592 $x593 $x594 $x559 $x599 $x560 $x600 $x601 $x602 $x563 $x607 $x564 $x608 $x609 $x610 $x567 $x615 $x568 $x616 $x617 $x618 $x571 $x623 $x572 $x624 $x625 $x626 $x575 $x631 $x576 $x632 $x633 $x634 $x579 $x639 $x580 $x640 $x641 $x642 $x583 $x647 $x584 $x648 $x649 $x650 $x653 $x590 $x654 $x657 $x659 $x694 $x660 $x697 $x698 $x662 $x701 $x702 $x664 $x705 $x706 $x666 $x710 $x711 $x668 $x714 $x715 $x670 $x718 $x719 $x672 $x722 $x723 $x674 $x727 $x728 $x676 $x731 $x732 $x678 $x735 $x736 $x680 $x739 $x740 $x682 $x743 $x744 $x684 $x747 $x748 $x686 $x751 $x752 $x688 $x755 $x756 $x690 $x759 $x693 $x761 $x763 $x764 $x767 $x770 $x771 $x773 $x775 $x777 $x779 $x781 $x784 $x785 $x787 $x789 $x796 $x790 $x802 $x801 $x799 $x795 $x793 $x791 $x807 $x809 $x811 $x813 $x815 $x817 $x819 $x822 $x823 $x826 $x828 $x830 $x832 $x834 $x836 $x838 $x841 $x842 $x844 $x846 $x848 $x850 $x852 $x854 $x856 $x858 $x860 $x862 $x864 $x866 $x868 $x870 $x872 $x874 $x876 $x878 $x880 $x882 $x884 $x886 $x888 $x890 $x892 $x894 $x896 $x898 $x900 $x902 $x904 $x906 $x908 $x910 $x912 $x914 $x916 $x918 $x920 $x922 $x924 $x926 $x928 $x930 $x932 $x934 $x936 $x938 $x940 $x942 $x944 $x946 $x948 $x950 $x952 $x954 $x956 $x958 $x960 $x962 $x964 $x966 $x968 $x970 $x972 $x974 $x976 $x978 $x980 $x982 $x984 $x986 $x988 $x990 $x992 $x994 $x996 $x998 $x1000 $x1002 $x1004 $x1006 $x1008 $x1010 $x1012 $x1014 $x1016 $x1018 $x1020 $x1022 $x1024 $x1026 $x1028 $x1030 $x1032 $x1034 $x1036 $x1038 $x1040 $x1042 $x1044 $x1046 $x1048 $x1050 $x1052 $x1054 $x1056 $x1058)))
(not $x1059)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

Last verified: 2026-03-25 08:06:06 UTC · Solver: Z3 4.16.0