SMT2 formal verification of security-critical code paths
PNG IHDR width must be positive and ≤ INT_MAX. From png_handle_IHDR() in pngrutil.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun width () Int)
(assert
(<= width 2147483647))
(assert
(>= width 1))
(assert
(or (< width 1) (> width 2147483647)))
(check-sat)
PNG IHDR height must be positive and ≤ INT_MAX. From png_handle_IHDR().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun height () Int)
(assert
(<= height 2147483647))
(assert
(>= height 1))
(assert
(or (< height 1) (> height 2147483647)))
(check-sat)
PNG bit depth must be 1-16. From png_handle_IHDR().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun bit_depth () Int)
(assert
(<= bit_depth 16))
(assert
(>= bit_depth 1))
(assert
(or (< bit_depth 1) (> bit_depth 16)))
(check-sat)
PNG IHDR color type is bounded to 0-6. From png_handle_IHDR().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun color_type () Int)
(assert
(<= color_type 6))
(assert
(>= color_type 0))
(assert
(or (< color_type 0) (> color_type 6)))
(check-sat)
PNG IHDR color type must be one of {0,2,3,4,6}; reserved values 1 and 5 are invalid per PNG specification.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun color_type () Int)
(assert
(let (($x15 (= color_type 6)))
(let (($x9 (= color_type 4)))
(let (($x8 (= color_type 3)))
(let (($x10 (= color_type 2)))
(let (($x6 (= color_type 0)))
(or $x6 $x10 $x8 $x9 $x15)))))))
(assert
(let (($x15 (= color_type 6)))
(let (($x9 (= color_type 4)))
(let (($x8 (= color_type 3)))
(let (($x10 (= color_type 2)))
(let (($x6 (= color_type 0)))
(let (($x24 (or $x6 $x10 $x8 $x9 $x15)))
(not $x24))))))))
(check-sat)
PNG IHDR bit depth must be compatible with color type per PNG spec (e.g., RGB allows 8/16 only).
; benchmark generated from python API
(set-info :status unknown)
(declare-fun bit_depth () Int)
(declare-fun color_type () Int)
(assert
(or (and (= color_type 0) (= bit_depth 1)) (and (= color_type 0) (= bit_depth 2)) (and (= color_type 0) (= bit_depth 4)) (and (= color_type 0) (= bit_depth 8)) (and (= color_type 0) (= bit_depth 16)) (and (= color_type 2) (= bit_depth 8)) (and (= color_type 2) (= bit_depth 16)) (and (= color_type 3) (= bit_depth 1)) (and (= color_type 3) (= bit_depth 2)) (and (= color_type 3) (= bit_depth 4)) (and (= color_type 3) (= bit_depth 8)) (and (= color_type 4) (= bit_depth 8)) (and (= color_type 4) (= bit_depth 16)) (and (= color_type 6) (= bit_depth 8)) (and (= color_type 6) (= bit_depth 16))))
(assert
(let (($x36 (= bit_depth 16)))
(let (($x11 (= bit_depth 8)))
(let (($x62 (or $x11 $x36)))
(let (($x39 (= color_type 6)))
(let (($x37 (= bit_depth 4)))
(let (($x15 (= bit_depth 2)))
(let (($x8 (= bit_depth 1)))
(let (($x64 (or $x8 $x15 $x37 $x11)))
(let (($x5 (= color_type 3)))
(let (($x68 (or (and (= color_type 0) (or $x8 $x15 $x37 $x11 $x36)) (and (= color_type 2) $x62) (and $x5 $x64) (and (= color_type 4) $x62) (and $x39 $x62))))
(not $x68))))))))))))
(check-sat)
PNG IHDR compression method must be 0 (deflate/inflate) per PNG specification. From png_handle_IHDR().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun compression_type () Int)
(assert
(<= compression_type 0))
(assert
(>= compression_type 0))
(assert
(or (< compression_type 0) (> compression_type 0)))
(check-sat)
PNG IHDR filter method must be 0 (adaptive filtering) per PNG specification. From png_handle_IHDR().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun filter_type () Int)
(assert
(<= filter_type 0))
(assert
(>= filter_type 0))
(assert
(or (< filter_type 0) (> filter_type 0)))
(check-sat)
PNG IHDR interlace method must be 0 (no interlace) or 1 (Adam7) per PNG specification. From png_handle_IHDR().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun interlace_type () Int)
(assert
(<= interlace_type 1))
(assert
(>= interlace_type 0))
(assert
(or (< interlace_type 0) (> interlace_type 1)))
(check-sat)
PNG chunk length ≤ INT_MAX. From png_read_chunk_header() in pngrutil.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun chunk_length () Int)
(assert
(<= chunk_length 2147483647))
(assert
(>= chunk_length 0))
(assert
(or (< chunk_length 0) (> chunk_length 2147483647)))
(check-sat)
PNG PLTE chunk length must be <= 768 bytes (256 RGB entries); oversized or malformed palette chunks are rejected in png_handle_PLTE().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun length () Int)
(assert
(<= length 768))
(assert
(>= length 0))
(assert
(or (< length 0) (> length 768)))
(check-sat)
PNG PLTE chunk length must be divisible by 3 (RGB triplets); libpng rejects non-triplet lengths via (length % 3) != 0 in png_handle_PLTE().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun length () Int)
(assert
(let (($x525 (= length 768)))
(let (($x523 (= length 765)))
(let (($x521 (= length 762)))
(let (($x519 (= length 759)))
(let (($x517 (= length 756)))
(let (($x515 (= length 753)))
(let (($x513 (= length 750)))
(let (($x511 (= length 747)))
(let (($x509 (= length 744)))
(let (($x507 (= length 741)))
(let (($x505 (= length 738)))
(let (($x503 (= length 735)))
(let (($x501 (= length 732)))
(let (($x499 (= length 729)))
(let (($x497 (= length 726)))
(let (($x495 (= length 723)))
(let (($x493 (= length 720)))
(let (($x491 (= length 717)))
(let (($x489 (= length 714)))
(let (($x487 (= length 711)))
(let (($x485 (= length 708)))
(let (($x483 (= length 705)))
(let (($x481 (= length 702)))
(let (($x479 (= length 699)))
(let (($x477 (= length 696)))
(let (($x475 (= length 693)))
(let (($x473 (= length 690)))
(let (($x471 (= length 687)))
(let (($x469 (= length 684)))
(let (($x467 (= length 681)))
(let (($x465 (= length 678)))
(let (($x463 (= length 675)))
(let (($x461 (= length 672)))
(let (($x459 (= length 669)))
(let (($x457 (= length 666)))
(let (($x455 (= length 663)))
(let (($x453 (= length 660)))
(let (($x451 (= length 657)))
(let (($x449 (= length 654)))
(let (($x447 (= length 651)))
(let (($x445 (= length 648)))
(let (($x443 (= length 645)))
(let (($x441 (= length 642)))
(let (($x439 (= length 639)))
(let (($x437 (= length 636)))
(let (($x435 (= length 633)))
(let (($x433 (= length 630)))
(let (($x431 (= length 627)))
(let (($x429 (= length 624)))
(let (($x427 (= length 621)))
(let (($x425 (= length 618)))
(let (($x423 (= length 615)))
(let (($x421 (= length 612)))
(let (($x419 (= length 609)))
(let (($x417 (= length 606)))
(let (($x415 (= length 603)))
(let (($x413 (= length 600)))
(let (($x411 (= length 597)))
(let (($x409 (= length 594)))
(let (($x407 (= length 591)))
(let (($x405 (= length 588)))
(let (($x403 (= length 585)))
(let (($x401 (= length 582)))
(let (($x399 (= length 579)))
(let (($x397 (= length 576)))
(let (($x395 (= length 573)))
(let (($x393 (= length 570)))
(let (($x391 (= length 567)))
(let (($x389 (= length 564)))
(let (($x387 (= length 561)))
(let (($x385 (= length 558)))
(let (($x383 (= length 555)))
(let (($x381 (= length 552)))
(let (($x379 (= length 549)))
(let (($x377 (= length 546)))
(let (($x375 (= length 543)))
(let (($x373 (= length 540)))
(let (($x371 (= length 537)))
(let (($x369 (= length 534)))
(let (($x367 (= length 531)))
(let (($x365 (= length 528)))
(let (($x363 (= length 525)))
(let (($x361 (= length 522)))
(let (($x359 (= length 519)))
(let (($x357 (= length 516)))
(let (($x355 (= length 513)))
(let (($x353 (= length 510)))
(let (($x351 (= length 507)))
(let (($x349 (= length 504)))
(let (($x347 (= length 501)))
(let (($x345 (= length 498)))
(let (($x343 (= length 495)))
(let (($x341 (= length 492)))
(let (($x339 (= length 489)))
(let (($x337 (= length 486)))
(let (($x335 (= length 483)))
(let (($x333 (= length 480)))
(let (($x331 (= length 477)))
(let (($x329 (= length 474)))
(let (($x327 (= length 471)))
(let (($x325 (= length 468)))
(let (($x323 (= length 465)))
(let (($x321 (= length 462)))
(let (($x319 (= length 459)))
(let (($x317 (= length 456)))
(let (($x315 (= length 453)))
(let (($x313 (= length 450)))
(let (($x311 (= length 447)))
(let (($x309 (= length 444)))
(let (($x307 (= length 441)))
(let (($x305 (= length 438)))
(let (($x303 (= length 435)))
(let (($x301 (= length 432)))
(let (($x299 (= length 429)))
(let (($x297 (= length 426)))
(let (($x295 (= length 423)))
(let (($x293 (= length 420)))
(let (($x291 (= length 417)))
(let (($x289 (= length 414)))
(let (($x287 (= length 411)))
(let (($x285 (= length 408)))
(let (($x283 (= length 405)))
(let (($x281 (= length 402)))
(let (($x279 (= length 399)))
(let (($x277 (= length 396)))
(let (($x275 (= length 393)))
(let (($x273 (= length 390)))
(let (($x271 (= length 387)))
(let (($x269 (= length 384)))
(let (($x267 (= length 381)))
(let (($x265 (= length 378)))
(let (($x263 (= length 375)))
(let (($x261 (= length 372)))
(let (($x259 (= length 369)))
(let (($x257 (= length 366)))
(let (($x255 (= length 363)))
(let (($x253 (= length 360)))
(let (($x251 (= length 357)))
(let (($x249 (= length 354)))
(let (($x247 (= length 351)))
(let (($x245 (= length 348)))
(let (($x243 (= length 345)))
(let (($x241 (= length 342)))
(let (($x239 (= length 339)))
(let (($x237 (= length 336)))
(let (($x235 (= length 333)))
(let (($x233 (= length 330)))
(let (($x231 (= length 327)))
(let (($x229 (= length 324)))
(let (($x227 (= length 321)))
(let (($x225 (= length 318)))
(let (($x223 (= length 315)))
(let (($x221 (= length 312)))
(let (($x219 (= length 309)))
(let (($x217 (= length 306)))
(let (($x215 (= length 303)))
(let (($x213 (= length 300)))
(let (($x211 (= length 297)))
(let (($x209 (= length 294)))
(let (($x207 (= length 291)))
(let (($x205 (= length 288)))
(let (($x203 (= length 285)))
(let (($x201 (= length 282)))
(let (($x199 (= length 279)))
(let (($x197 (= length 276)))
(let (($x195 (= length 273)))
(let (($x193 (= length 270)))
(let (($x191 (= length 267)))
(let (($x189 (= length 264)))
(let (($x187 (= length 261)))
(let (($x185 (= length 258)))
(let (($x183 (= length 255)))
(let (($x181 (= length 252)))
(let (($x179 (= length 249)))
(let (($x177 (= length 246)))
(let (($x175 (= length 243)))
(let (($x173 (= length 240)))
(let (($x171 (= length 237)))
(let (($x169 (= length 234)))
(let (($x167 (= length 231)))
(let (($x165 (= length 228)))
(let (($x163 (= length 225)))
(let (($x161 (= length 222)))
(let (($x159 (= length 219)))
(let (($x157 (= length 216)))
(let (($x155 (= length 213)))
(let (($x153 (= length 210)))
(let (($x151 (= length 207)))
(let (($x149 (= length 204)))
(let (($x147 (= length 201)))
(let (($x145 (= length 198)))
(let (($x143 (= length 195)))
(let (($x141 (= length 192)))
(let (($x139 (= length 189)))
(let (($x129 (= length 186)))
(let (($x131 (= length 183)))
(let (($x118 (= length 180)))
(let (($x116 (= length 177)))
(let (($x126 (= length 174)))
(let (($x124 (= length 171)))
(let (($x122 (= length 168)))
(let (($x134 (= length 165)))
(let (($x120 (= length 162)))
(let (($x136 (= length 159)))
(let (($x125 (= length 156)))
(let (($x45 (= length 153)))
(let (($x47 (= length 150)))
(let (($x49 (= length 147)))
(let (($x53 (= length 144)))
(let (($x55 (= length 141)))
(let (($x57 (= length 138)))
(let (($x44 (= length 135)))
(let (($x50 (= length 132)))
(let (($x43 (= length 129)))
(let (($x113 (= length 126)))
(let (($x115 (= length 123)))
(let (($x110 (= length 120)))
(let (($x108 (= length 117)))
(let (($x106 (= length 114)))
(let (($x104 (= length 111)))
(let (($x102 (= length 108)))
(let (($x100 (= length 105)))
(let (($x98 (= length 102)))
(let (($x96 (= length 99)))
(let (($x94 (= length 96)))
(let (($x92 (= length 93)))
(let (($x90 (= length 90)))
(let (($x88 (= length 87)))
(let (($x86 (= length 84)))
(let (($x84 (= length 81)))
(let (($x82 (= length 78)))
(let (($x80 (= length 75)))
(let (($x78 (= length 72)))
(let (($x76 (= length 69)))
(let (($x74 (= length 66)))
(let (($x72 (= length 63)))
(let (($x70 (= length 60)))
(let (($x41 (= length 57)))
(let (($x38 (= length 54)))
(let (($x20 (= length 51)))
(let (($x22 (= length 48)))
(let (($x12 (= length 45)))
(let (($x24 (= length 42)))
(let (($x35 (= length 39)))
(let (($x69 (= length 36)))
(let (($x17 (= length 33)))
(let (($x15 (= length 30)))
(let (($x67 (= length 27)))
(let (($x62 (= length 24)))
(let (($x5 (= length 21)))
(let (($x8 (= length 18)))
(let (($x65 (= length 15)))
(let (($x11 (= length 12)))
(let (($x28 (= length 9)))
(let (($x37 (= length 6)))
(let (($x61 (= length 3)))
(let (($x60 (= length 0)))
(or $x60 $x61 $x37 $x28 $x11 $x65 $x8 $x5 $x62 $x67 $x15 $x17 $x69 $x35 $x24 $x12 $x22 $x20 $x38 $x41 $x70 $x72 $x74 $x76 $x78 $x80 $x82 $x84 $x86 $x88 $x90 $x92 $x94 $x96 $x98 $x100 $x102 $x104 $x106 $x108 $x110 $x115 $x113 $x43 $x50 $x44 $x57 $x55 $x53 $x49 $x47 $x45 $x125 $x136 $x120 $x134 $x122 $x124 $x126 $x116 $x118 $x131 $x129 $x139 $x141 $x143 $x145 $x147 $x149 $x151 $x153 $x155 $x157 $x159 $x161 $x163 $x165 $x167 $x169 $x171 $x173 $x175 $x177 $x179 $x181 $x183 $x185 $x187 $x189 $x191 $x193 $x195 $x197 $x199 $x201 $x203 $x205 $x207 $x209 $x211 $x213 $x215 $x217 $x219 $x221 $x223 $x225 $x227 $x229 $x231 $x233 $x235 $x237 $x239 $x241 $x243 $x245 $x247 $x249 $x251 $x253 $x255 $x257 $x259 $x261 $x263 $x265 $x267 $x269 $x271 $x273 $x275 $x277 $x279 $x281 $x283 $x285 $x287 $x289 $x291 $x293 $x295 $x297 $x299 $x301 $x303 $x305 $x307 $x309 $x311 $x313 $x315 $x317 $x319 $x321 $x323 $x325 $x327 $x329 $x331 $x333 $x335 $x337 $x339 $x341 $x343 $x345 $x347 $x349 $x351 $x353 $x355 $x357 $x359 $x361 $x363 $x365 $x367 $x369 $x371 $x373 $x375 $x377 $x379 $x381 $x383 $x385 $x387 $x389 $x391 $x393 $x395 $x397 $x399 $x401 $x403 $x405 $x407 $x409 $x411 $x413 $x415 $x417 $x419 $x421 $x423 $x425 $x427 $x429 $x431 $x433 $x435 $x437 $x439 $x441 $x443 $x445 $x447 $x449 $x451 $x453 $x455 $x457 $x459 $x461 $x463 $x465 $x467 $x469 $x471 $x473 $x475 $x477 $x479 $x481 $x483 $x485 $x487 $x489 $x491 $x493 $x495 $x497 $x499 $x501 $x503 $x505 $x507 $x509 $x511 $x513 $x515 $x517 $x519 $x521 $x523 $x525)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert
(let ((?x544 (mod length 3)))
(and (distinct ?x544 0) true)))
(check-sat)
libpng rejects PLTE as out-of-place when PNG_HAVE_IDAT is already set; palette must be defined before image data chunks. From png_handle_PLTE() in pngrutil.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun mode_have_idat () Int)
(assert
(<= mode_have_idat 0))
(assert
(>= mode_have_idat 0))
(assert
(or (< mode_have_idat 0) (> mode_have_idat 0)))
(check-sat)
PNG tRNS chunk length must follow color type rules: grayscale=2 bytes, RGB=6 bytes, palette=1..256 entries (with additional runtime bound by num_palette). From png_handle_tRNS() in pngrutil.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun length () Int)
(declare-fun color_type () Int)
(assert
(let (($x544 (= length 6)))
(let (($x39 (= color_type 2)))
(let (($x6 (and $x39 $x544)))
(let (($x10 (= length 2)))
(let (($x17 (= color_type 0)))
(let (($x69 (and $x17 $x10)))
(or $x69 $x6 (and (= color_type 3) (= length 1)) (and (= color_type 3) $x10) (and (= color_type 3) (= length 3)) (and (= color_type 3) (= length 4)) (and (= color_type 3) (= length 5)) (and (= color_type 3) $x544) (and (= color_type 3) (= length 7)) (and (= color_type 3) (= length 8)) (and (= color_type 3) (= length 9)) (and (= color_type 3) (= length 10)) (and (= color_type 3) (= length 11)) (and (= color_type 3) (= length 12)) (and (= color_type 3) (= length 13)) (and (= color_type 3) (= length 14)) (and (= color_type 3) (= length 15)) (and (= color_type 3) (= length 16)) (and (= color_type 3) (= length 17)) (and (= color_type 3) (= length 18)) (and (= color_type 3) (= length 19)) (and (= color_type 3) (= length 20)) (and (= color_type 3) (= length 21)) (and (= color_type 3) (= length 22)) (and (= color_type 3) (= length 23)) (and (= color_type 3) (= length 24)) (and (= color_type 3) (= length 25)) (and (= color_type 3) (= length 26)) (and (= color_type 3) (= length 27)) (and (= color_type 3) (= length 28)) (and (= color_type 3) (= length 29)) (and (= color_type 3) (= length 30)) (and (= color_type 3) (= length 31)) (and (= color_type 3) (= length 32)) (and (= color_type 3) (= length 33)) (and (= color_type 3) (= length 34)) (and (= color_type 3) (= length 35)) (and (= color_type 3) (= length 36)) (and (= color_type 3) (= length 37)) (and (= color_type 3) (= length 38)) (and (= color_type 3) (= length 39)) (and (= color_type 3) (= length 40)) (and (= color_type 3) (= length 41)) (and (= color_type 3) (= length 42)) (and (= color_type 3) (= length 43)) (and (= color_type 3) (= length 44)) (and (= color_type 3) (= length 45)) (and (= color_type 3) (= length 46)) (and (= color_type 3) (= length 47)) (and (= color_type 3) (= length 48)) (and (= color_type 3) (= length 49)) (and (= color_type 3) (= length 50)) (and (= color_type 3) (= length 51)) (and (= color_type 3) (= length 52)) (and (= color_type 3) (= length 53)) (and (= color_type 3) (= length 54)) (and (= color_type 3) (= length 55)) (and (= color_type 3) (= length 56)) (and (= color_type 3) (= length 57)) (and (= color_type 3) (= length 58)) (and (= color_type 3) (= length 59)) (and (= color_type 3) (= length 60)) (and (= color_type 3) (= length 61)) (and (= color_type 3) (= length 62)) (and (= color_type 3) (= length 63)) (and (= color_type 3) (= length 64)) (and (= color_type 3) (= length 65)) (and (= color_type 3) (= length 66)) (and (= color_type 3) (= length 67)) (and (= color_type 3) (= length 68)) (and (= color_type 3) (= length 69)) (and (= color_type 3) (= length 70)) (and (= color_type 3) (= length 71)) (and (= color_type 3) (= length 72)) (and (= color_type 3) (= length 73)) (and (= color_type 3) (= length 74)) (and (= color_type 3) (= length 75)) (and (= color_type 3) (= length 76)) (and (= color_type 3) (= length 77)) (and (= color_type 3) (= length 78)) (and (= color_type 3) (= length 79)) (and (= color_type 3) (= length 80)) (and (= color_type 3) (= length 81)) (and (= color_type 3) (= length 82)) (and (= color_type 3) (= length 83)) (and (= color_type 3) (= length 84)) (and (= color_type 3) (= length 85)) (and (= color_type 3) (= length 86)) (and (= color_type 3) (= length 87)) (and (= color_type 3) (= length 88)) (and (= color_type 3) (= length 89)) (and (= color_type 3) (= length 90)) (and (= color_type 3) (= length 91)) (and (= color_type 3) (= length 92)) (and (= color_type 3) (= length 93)) (and (= color_type 3) (= length 94)) (and (= color_type 3) (= length 95)) (and (= color_type 3) (= length 96)) (and (= color_type 3) (= length 97)) (and (= color_type 3) (= length 98)) (and (= color_type 3) (= length 99)) (and (= color_type 3) (= length 100)) (and (= color_type 3) (= length 101)) (and (= color_type 3) (= length 102)) (and (= color_type 3) (= length 103)) (and (= color_type 3) (= length 104)) (and (= color_type 3) (= length 105)) (and (= color_type 3) (= length 106)) (and (= color_type 3) (= length 107)) (and (= color_type 3) (= length 108)) (and (= color_type 3) (= length 109)) (and (= color_type 3) (= length 110)) (and (= color_type 3) (= length 111)) (and (= color_type 3) (= length 112)) (and (= color_type 3) (= length 113)) (and (= color_type 3) (= length 114)) (and (= color_type 3) (= length 115)) (and (= color_type 3) (= length 116)) (and (= color_type 3) (= length 117)) (and (= color_type 3) (= length 118)) (and (= color_type 3) (= length 119)) (and (= color_type 3) (= length 120)) (and (= color_type 3) (= length 121)) (and (= color_type 3) (= length 122)) (and (= color_type 3) (= length 123)) (and (= color_type 3) (= length 124)) (and (= color_type 3) (= length 125)) (and (= color_type 3) (= length 126)) (and (= color_type 3) (= length 127)) (and (= color_type 3) (= length 128)) (and (= color_type 3) (= length 129)) (and (= color_type 3) (= length 130)) (and (= color_type 3) (= length 131)) (and (= color_type 3) (= length 132)) (and (= color_type 3) (= length 133)) (and (= color_type 3) (= length 134)) (and (= color_type 3) (= length 135)) (and (= color_type 3) (= length 136)) (and (= color_type 3) (= length 137)) (and (= color_type 3) (= length 138)) (and (= color_type 3) (= length 139)) (and (= color_type 3) (= length 140)) (and (= color_type 3) (= length 141)) (and (= color_type 3) (= length 142)) (and (= color_type 3) (= length 143)) (and (= color_type 3) (= length 144)) (and (= color_type 3) (= length 145)) (and (= color_type 3) (= length 146)) (and (= color_type 3) (= length 147)) (and (= color_type 3) (= length 148)) (and (= color_type 3) (= length 149)) (and (= color_type 3) (= length 150)) (and (= color_type 3) (= length 151)) (and (= color_type 3) (= length 152)) (and (= color_type 3) (= length 153)) (and (= color_type 3) (= length 154)) (and (= color_type 3) (= length 155)) (and (= color_type 3) (= length 156)) (and (= color_type 3) (= length 157)) (and (= color_type 3) (= length 158)) (and (= color_type 3) (= length 159)) (and (= color_type 3) (= length 160)) (and (= color_type 3) (= length 161)) (and (= color_type 3) (= length 162)) (and (= color_type 3) (= length 163)) (and (= color_type 3) (= length 164)) (and (= color_type 3) (= length 165)) (and (= color_type 3) (= length 166)) (and (= color_type 3) (= length 167)) (and (= color_type 3) (= length 168)) (and (= color_type 3) (= length 169)) (and (= color_type 3) (= length 170)) (and (= color_type 3) (= length 171)) (and (= color_type 3) (= length 172)) (and (= color_type 3) (= length 173)) (and (= color_type 3) (= length 174)) (and (= color_type 3) (= length 175)) (and (= color_type 3) (= length 176)) (and (= color_type 3) (= length 177)) (and (= color_type 3) (= length 178)) (and (= color_type 3) (= length 179)) (and (= color_type 3) (= length 180)) (and (= color_type 3) (= length 181)) (and (= color_type 3) (= length 182)) (and (= color_type 3) (= length 183)) (and (= color_type 3) (= length 184)) (and (= color_type 3) (= length 185)) (and (= color_type 3) (= length 186)) (and (= color_type 3) (= length 187)) (and (= color_type 3) (= length 188)) (and (= color_type 3) (= length 189)) (and (= color_type 3) (= length 190)) (and (= color_type 3) (= length 191)) (and (= color_type 3) (= length 192)) (and (= color_type 3) (= length 193)) (and (= color_type 3) (= length 194)) (and (= color_type 3) (= length 195)) (and (= color_type 3) (= length 196)) (and (= color_type 3) (= length 197)) (and (= color_type 3) (= length 198)) (and (= color_type 3) (= length 199)) (and (= color_type 3) (= length 200)) (and (= color_type 3) (= length 201)) (and (= color_type 3) (= length 202)) (and (= color_type 3) (= length 203)) (and (= color_type 3) (= length 204)) (and (= color_type 3) (= length 205)) (and (= color_type 3) (= length 206)) (and (= color_type 3) (= length 207)) (and (= color_type 3) (= length 208)) (and (= color_type 3) (= length 209)) (and (= color_type 3) (= length 210)) (and (= color_type 3) (= length 211)) (and (= color_type 3) (= length 212)) (and (= color_type 3) (= length 213)) (and (= color_type 3) (= length 214)) (and (= color_type 3) (= length 215)) (and (= color_type 3) (= length 216)) (and (= color_type 3) (= length 217)) (and (= color_type 3) (= length 218)) (and (= color_type 3) (= length 219)) (and (= color_type 3) (= length 220)) (and (= color_type 3) (= length 221)) (and (= color_type 3) (= length 222)) (and (= color_type 3) (= length 223)) (and (= color_type 3) (= length 224)) (and (= color_type 3) (= length 225)) (and (= color_type 3) (= length 226)) (and (= color_type 3) (= length 227)) (and (= color_type 3) (= length 228)) (and (= color_type 3) (= length 229)) (and (= color_type 3) (= length 230)) (and (= color_type 3) (= length 231)) (and (= color_type 3) (= length 232)) (and (= color_type 3) (= length 233)) (and (= color_type 3) (= length 234)) (and (= color_type 3) (= length 235)) (and (= color_type 3) (= length 236)) (and (= color_type 3) (= length 237)) (and (= color_type 3) (= length 238)) (and (= color_type 3) (= length 239)) (and (= color_type 3) (= length 240)) (and (= color_type 3) (= length 241)) (and (= color_type 3) (= length 242)) (and (= color_type 3) (= length 243)) (and (= color_type 3) (= length 244)) (and (= color_type 3) (= length 245)) (and (= color_type 3) (= length 246)) (and (= color_type 3) (= length 247)) (and (= color_type 3) (= length 248)) (and (= color_type 3) (= length 249)) (and (= color_type 3) (= length 250)) (and (= color_type 3) (= length 251)) (and (= color_type 3) (= length 252)) (and (= color_type 3) (= length 253)) (and (= color_type 3) (= length 254)) (and (= color_type 3) (= length 255)) (and (= color_type 3) (= length 256))))))))))
(assert
(let (($x544 (= length 6)))
(let (($x39 (= color_type 2)))
(let (($x6 (and $x39 $x544)))
(let (($x10 (= length 2)))
(let (($x17 (= color_type 0)))
(let (($x69 (and $x17 $x10)))
(let (($x882 (or $x69 $x6 (and (= color_type 3) (>= length 1) (<= length 256)))))
(not $x882)))))))))
(check-sat)