Bogus range calculations for bitwise operations in Guile 2.2

[Mark H Weaver]

Hi Andy,

While investigating <https://bugs.gnu.org/31474>, I've found several
mistakes in the range calculations for bitwise operations in (language
cps types).  As a result, 'logand', 'logsub', 'logior' and 'logxor'
would sometimes generate bad code.

Andy Wingo <address@hidden> writes:

> wingo pushed a commit to branch stable-2.2
> in repository guile.
>
> commit 5f59e2812db7108ef9302f7bd862325572751b17
> Author: Andy Wingo <address@hidden>
> Date:   Thu Nov 23 18:13:56 2017 +0100
>
>     Fix logand type inference
>     
>     * module/language/cps/types.scm (logand): We were computing the wrong
>       ranges when either argument was negative; a terrible bug!
>       (logsub): Also fix range when A is negative and B is non-negative.
>       (ulogand): Tighten up range.
> ---
>  module/language/cps/types.scm | 17 +++++++++++------
>  1 file changed, 11 insertions(+), 6 deletions(-)
>
> diff --git a/module/language/cps/types.scm b/module/language/cps/types.scm
> index 8464a65..c24f9b9 100644
> --- a/module/language/cps/types.scm
> +++ b/module/language/cps/types.scm
> @@ -1283,12 +1283,17 @@ minimum, and maximum."
>  (define-type-inferrer (logand a b result)
>    (define (logand-min a b)
>      (if (and (negative? a) (negative? b))
> -        (min a b)
> +        (let ((min (min a b)))
> +          (if (inf? min)
> +              -inf.0
> +              (- 1 (next-power-of-two (- min)))))
>          0))
>    (define (logand-max a b)
> -    (if (and (positive? a) (positive? b))
> -        (min a b)
> -        0))
> +    (cond
> +     ((or (and (positive? a) (positive? b))
> +          (and (negative? a) (negative? b)))
> +      (min a b))
> +     (else (max a b))))
>    (restrict! a &exact-integer -inf.0 +inf.0)
>    (restrict! b &exact-integer -inf.0 +inf.0)
>    (define! result &exact-integer

Even with this fix, the code is still broken.  For example, suppose we
know that (-1 <= a <= 3) and (0 <= b <= 7).  In this case, 'logand-max'
will see that the upper bounds of both arguments are positive, and thus
return the minimum of those upper bounds, which in this case is 3.  This
is bogus because 'a' could be -1, in which case the result could be as
large as 7, since (logand -1 7) = 7.

Further investigation revealed that *all* of the generic binary bitwise
operator type inferrers in Guile 2.2 (logand, logior, logsub, logxor)
sometimes compute ranges that omit the true result.

I've sent a proposed patch for stable-2.2 to fix these problems to
<https://bugs.gnu.org/31474>.  Could you take a look, and maybe
integrate these fixes into 'master'?

I hacked up some code to perform random testing on my new code, and to
find examples where the old code fails.  See below for the test code and
transcript.

What do you think?

      Mark


--8<---------------cut here---------------start------------->8---
GNU Guile 2.2.3
Copyright (C) 1995-2017 Free Software Foundation, Inc.

Guile comes with ABSOLUTELY NO WARRANTY; for details type `,show w'.
This program is free software, and you are welcome to redistribute it
under certain conditions; type `,show c' for details.

Enter `,help' for help.
scheme@(guile-user)> (load "bounds-tests.scm")
;;; note: source file /home/mhw/src/bounds-tests.scm
;;;       newer than compiled 
/home/mhw/.cache/guile/ccache/2.2-LE-8-3.A/home/mhw/src/bounds-tests.scm.go
;;; note: auto-compilation is enabled, set GUILE_AUTO_COMPILE=0
;;;       or pass the --no-auto-compile argument to disable.
;;; compiling /home/mhw/src/bounds-tests.scm
;;; compiled 
/home/mhw/.cache/guile/ccache/2.2-LE-8-3.A/home/mhw/src/bounds-tests.scm.go
scheme@(guile-user)> (repeated-test-bounds 1000000 logand logand-bounds)
scheme@(guile-user)> (repeated-test-bounds 1000000 logsub logsub-bounds)
scheme@(guile-user)> (repeated-test-bounds 1000000 logior logior-bounds)
scheme@(guile-user)> (repeated-test-bounds 1000000 logxor logxor-bounds)
scheme@(guile-user)> (repeated-test-bounds 1000 logand old-logand-bounds)
failed: (-inf.0 <= -418 <= 88) and (-inf.0 <= 730 <= 1001), but not: (-inf.0 <= 
602 <= 88)
failed: (-261 <= -153 <= 39) and (241 <= 483 <= 996), but not: (0 <= 355 <= 39)
failed: (-647 <= -34 <= 54) and (501 <= 691 <= 696), but not: (0 <= 658 <= 54)
failed: (-490 <= 521 <= 899) and (-291 <= -64 <= 365), but not: (-511 <= 512 <= 
365)
failed: (-806 <= -404 <= 158) and (261 <= 806 <= 895), but not: (0 <= 548 <= 
158)
failed: (-745 <= -409 <= 24) and (-569 <= 497 <= 552), but not: (-1023 <= 97 <= 
24)
failed: (-681 <= -187 <= 420) and (393 <= 556 <= 998), but not: (0 <= 516 <= 
420)
failed: (449 <= 499 <= 555) and (-589 <= -565 <= 42), but not: (0 <= 451 <= 42)
failed: (-inf.0 <= 784 <= 897) and (-736 <= -193 <= 140), but not: (-inf.0 <= 
784 <= 140)
failed: (-885 <= -566 <= 358) and (372 <= 397 <= 563), but not: (0 <= 392 <= 
358)
failed: (-326 <= 677 <= 863) and (-558 <= -354 <= 577), but not: (-1023 <= 644 
<= 577)
failed: (-887 <= -297 <= 567) and (833 <= 875 <= 905), but not: (0 <= 579 <= 
567)
failed: (-865 <= -708 <= 175) and (-56 <= 435 <= 974), but not: (-1023 <= 304 
<= 175)
failed: (-494 <= 410 <= 633) and (-484 <= -104 <= 407), but not: (-511 <= 408 
<= 407)
failed: (-56 <= 155 <= 903) and (-823 <= -592 <= 120), but not: (-1023 <= 144 
<= 120)
failed: (-13 <= 653 <= 909) and (-835 <= -194 <= 491), but not: (-1023 <= 524 
<= 491)
failed: (823 <= 963 <= +inf.0) and (-350 <= -307 <= 279), but not: (0 <= 705 <= 
279.0)
failed: (-991 <= -742 <= -633) and (-861 <= -859 <= -835), but not: (-1023 <= 
-1024 <= -835)
failed: (31 <= 569 <= 1006) and (-679 <= -501 <= 405), but not: (0 <= 521 <= 
405)
failed: (-598 <= -284 <= 254) and (-6 <= 842 <= 919), but not: (-1023 <= 576 <= 
254)
failed: (-574 <= -568 <= -107) and (-968 <= -493 <= 934), but not: (-1023 <= 
-1024 <= 934)
failed: (-605 <= -524 <= 290) and (449 <= 891 <= 945), but not: (0 <= 368 <= 
290)
failed: (-1020 <= -496 <= 346) and (-999 <= -860 <= -91), but not: (-1023 <= 
-1024 <= 346)
failed: (-677 <= -200 <= 148) and (181 <= 724 <= 1004), but not: (0 <= 528 <= 
148)
failed: (-inf.0 <= -299 <= 425) and (296 <= 697 <= 976), but not: (0 <= 657 <= 
425)
failed: (282 <= 290 <= 593) and (-618 <= -598 <= 42), but not: (0 <= 290 <= 42)
failed: (-inf.0 <= -97 <= 251) and (466 <= 482 <= 677), but not: (0 <= 386 <= 
251)
failed: (-928 <= -432 <= 877) and (-767 <= -756 <= -659), but not: (-1023 <= 
-1024 <= 877)
failed: (-540 <= -3 <= 75) and (-370 <= 134 <= 645), but not: (-1023 <= 132 <= 
75)
failed: (-314 <= -255 <= 357) and (-252 <= 754 <= 871), but not: (-511 <= 512 
<= 357)
failed: (-884 <= -440 <= 35) and (242 <= 242 <= 277), but not: (0 <= 64 <= 35)
failed: (-489 <= 400 <= 519) and (-inf.0 <= -11 <= 25), but not: (-inf.0 <= 400 
<= 25)
failed: (-672 <= -89 <= 97) and (311 <= 788 <= 805), but not: (0 <= 772 <= 97)
failed: (-618 <= -391 <= 47) and (-247 <= 182 <= 815), but not: (-1023 <= 48 <= 
47)
failed: (-943 <= 469 <= +inf.0) and (-759 <= -638 <= 272), but not: (-1023 <= 
384 <= 272.0)
failed: (-536 <= -246 <= 6) and (235 <= 363 <= 529), but not: (0 <= 266 <= 6)
failed: (-710 <= -81 <= 252) and (502 <= 606 <= 733), but not: (0 <= 526 <= 252)
failed: (-935 <= -524 <= 434) and (296 <= 508 <= 727), but not: (0 <= 500 <= 
434)
failed: (-620 <= -32 <= 335) and (-59 <= 428 <= 987), but not: (-1023 <= 416 <= 
335)
failed: (960 <= 994 <= 1005) and (-47 <= -10 <= 668), but not: (0 <= 994 <= 668)
failed: (-654 <= -95 <= 405) and (-3 <= 747 <= 953), but not: (-1023 <= 673 <= 
405)
failed: (-417 <= -239 <= -100) and (-844 <= -794 <= -669), but not: (-1023 <= 
-1024 <= -669)
failed: (-696 <= -266 <= 369) and (275 <= 641 <= 685), but not: (0 <= 640 <= 
369)
failed: (659 <= 772 <= 793) and (-92 <= -21 <= 250), but not: (0 <= 768 <= 250)
failed: (-414 <= 387 <= 917) and (-974 <= -206 <= 68), but not: (-1023 <= 258 
<= 68)
failed: (-658 <= -544 <= 238) and (-32 <= 346 <= 842), but not: (-1023 <= 320 
<= 238)
failed: (-494 <= -493 <= -449) and (-838 <= -724 <= -713), but not: (-1023 <= 
-1024 <= -713)
failed: (-449 <= -371 <= 930) and (-986 <= -912 <= -616), but not: (-1023 <= 
-1024 <= 930)
failed: (-262 <= -14 <= 365) and (300 <= 503 <= 660), but not: (0 <= 498 <= 365)
failed: (773 <= 910 <= 918) and (-482 <= -453 <= 409), but not: (0 <= 522 <= 
409)
failed: (-inf.0 <= 524 <= 623) and (-152 <= -62 <= 321), but not: (-inf.0 <= 
512 <= 321)
failed: (-381 <= -312 <= 203) and (341 <= 543 <= 660), but not: (0 <= 520 <= 
203)
failed: (-962 <= -383 <= 587) and (-916 <= -710 <= -163), but not: (-1023 <= 
-1024 <= 587)
failed: (-447 <= 518 <= 920) and (-inf.0 <= -178 <= 275), but not: (-inf.0 <= 
518 <= 275)
failed: (-10 <= 662 <= 835) and (-547 <= -311 <= 199), but not: (-1023 <= 640 
<= 199)
failed: (-667 <= -324 <= 350) and (365 <= 727 <= 846), but not: (0 <= 660 <= 
350)
failed: (-815 <= 870 <= 887) and (-799 <= -470 <= 145), but not: (-1023 <= 546 
<= 145)
failed: (-595 <= 502 <= 784) and (-177 <= -99 <= 232), but not: (-1023 <= 404 
<= 232)
failed: (-725 <= -43 <= 88) and (155 <= 319 <= 368), but not: (0 <= 277 <= 88)
failed: (-543 <= -72 <= 223) and (-inf.0 <= 822 <= 843), but not: (-inf.0 <= 
816 <= 223)
failed: (-38 <= 159 <= 209) and (-885 <= -315 <= 103), but not: (-1023 <= 133 
<= 103)
failed: (-740 <= 472 <= 788) and (-322 <= -242 <= 182), but not: (-1023 <= 264 
<= 182)
failed: (-150 <= 470 <= 847) and (-32 <= -31 <= 87), but not: (-255 <= 448 <= 
87)
failed: (-inf.0 <= 241 <= 310) and (-157 <= -4 <= 19), but not: (-inf.0 <= 240 
<= 19)
failed: (-239 <= -63 <= 256) and (578 <= 665 <= 675), but not: (0 <= 641 <= 256)
failed: (204 <= 381 <= 711) and (-335 <= -98 <= 4), but not: (0 <= 284 <= 4)
failed: (-inf.0 <= 860 <= 947) and (-343 <= -185 <= 775), but not: (-inf.0 <= 
836 <= 775)
failed: (-48 <= 221 <= 421) and (-inf.0 <= -629 <= 56), but not: (-inf.0 <= 137 
<= 56)
failed: (453 <= 587 <= 754) and (-975 <= -93 <= 403), but not: (0 <= 515 <= 403)
failed: (607 <= 686 <= 688) and (-931 <= -476 <= 490), but not: (0 <= 548 <= 
490)
failed: (-708 <= -147 <= 268) and (815 <= 844 <= 899), but not: (0 <= 844 <= 
268)
failed: (-935 <= 88 <= 323) and (-598 <= -568 <= 4), but not: (-1023 <= 72 <= 4)
failed: (-63 <= 455 <= 732) and (-363 <= -62 <= 64), but not: (-511 <= 450 <= 
64)
failed: (-552 <= -420 <= 263) and (589 <= 715 <= 814), but not: (0 <= 584 <= 
263)
failed: (606 <= 638 <= 798) and (-428 <= -114 <= 45), but not: (0 <= 526 <= 45)
failed: (-456 <= 384 <= 758) and (-249 <= -156 <= 221), but not: (-511 <= 256 
<= 221)
failed: (-217 <= -204 <= 172) and (486 <= 881 <= 980), but not: (0 <= 816 <= 
172)
failed: (-608 <= -584 <= 148) and (134 <= 472 <= +inf.0), but not: (0 <= 408 <= 
148.0)
failed: (-935 <= -297 <= 44) and (230 <= 333 <= 895), but not: (0 <= 69 <= 44)
failed: (-163 <= -38 <= 108) and (328 <= 399 <= 507), but not: (0 <= 394 <= 108)
failed: (-316 <= -266 <= 125) and (-435 <= 570 <= 935), but not: (-511 <= 562 
<= 125)
failed: (107 <= 117 <= 152) and (-895 <= -562 <= 49), but not: (0 <= 68 <= 49)
failed: (-331 <= -318 <= 588) and (-150 <= 665 <= 846), but not: (-511 <= 640 
<= 588)
failed: (-362 <= -134 <= 572) and (106 <= 783 <= 1014), but not: (0 <= 778 <= 
572)
failed: (-908 <= 565 <= 588) and (-765 <= -183 <= 505), but not: (-1023 <= 513 
<= 505)
failed: (-495 <= -259 <= 59) and (16 <= 70 <= 572), but not: (0 <= 68 <= 59)
failed: (-556 <= -376 <= 105) and (-967 <= -713 <= -602), but not: (-1023 <= 
-1024 <= 105)
failed: (-118 <= 728 <= 786) and (-inf.0 <= -246 <= 103), but not: (-inf.0 <= 
520 <= 103)
failed: (-618 <= -62 <= 35) and (292 <= 812 <= 833), but not: (0 <= 768 <= 35)
failed: (-46 <= 75 <= 505) and (-555 <= -412 <= 5), but not: (-1023 <= 64 <= 5)
failed: (-873 <= -280 <= 100) and (-742 <= 361 <= 905), but not: (-1023 <= 104 
<= 100)
failed: (593 <= 597 <= 603) and (-742 <= -370 <= 291), but not: (0 <= 516 <= 
291)
failed: (-483 <= -449 <= 519) and (-146 <= 929 <= 996), but not: (-511 <= 545 
<= 519)
failed: (-835 <= -658 <= 60) and (275 <= 357 <= 402), but not: (0 <= 356 <= 60)
failed: (-514 <= -434 <= 204) and (579 <= 608 <= 686), but not: (0 <= 576 <= 
204)
failed: (897 <= 994 <= 1003) and (-979 <= -258 <= 289), but not: (0 <= 738 <= 
289)
failed: (422 <= 451 <= 511) and (-329 <= -195 <= 5), but not: (0 <= 257 <= 5)
failed: (80 <= 789 <= 827) and (-716 <= -343 <= 97), but not: (0 <= 513 <= 97)
failed: (-894 <= -474 <= 18) and (-1007 <= -743 <= 125), but not: (-1023 <= 
-1024 <= 18)
failed: (-35 <= 649 <= 697) and (-565 <= -321 <= 17), but not: (-1023 <= 649 <= 
17)
failed: (372 <= 423 <= 835) and (-196 <= -113 <= 211), but not: (0 <= 391 <= 
211)
failed: (-903 <= -704 <= 27) and (-644 <= -342 <= 183), but not: (-1023 <= 
-1024 <= 27)
failed: (-611 <= -333 <= 215) and (234 <= 644 <= 717), but not: (0 <= 640 <= 
215)
scheme@(guile-user)> (repeated-test-bounds 1000 logsub old-logsub-bounds)
failed: (-372 <= -186 <= 55) and (-210 <= 883 <= 938), but not: (-372 <= -1020 
<= +inf.0)
failed: (275 <= 485 <= 593) and (-908 <= -674 <= 480), but not: (275 <= 161 <= 
593)
failed: (837 <= 838 <= 851) and (-10 <= 239 <= 649), but not: (837 <= 768 <= 
851)
failed: (367 <= 376 <= 642) and (-319 <= 292 <= 762), but not: (367 <= 88 <= 
642)
failed: (451 <= 655 <= 794) and (-71 <= -3 <= 615), but not: (451 <= 2 <= 794)
failed: (-893 <= -696 <= -170) and (-13 <= 356 <= 977), but not: (-893 <= -1016 
<= +inf.0)
failed: (349 <= 465 <= 776) and (-46 <= -26 <= 248), but not: (349 <= 17 <= 776)
failed: (372 <= 374 <= 416) and (-137 <= -51 <= 1006), but not: (372 <= 50 <= 
416)
failed: (-506 <= -382 <= -260) and (-153 <= 187 <= 364), but not: (-506 <= -512 
<= +inf.0)
failed: (247 <= 762 <= 975) and (-754 <= -228 <= 991), but not: (247 <= 226 <= 
975)
failed: (-67 <= -43 <= 259) and (-838 <= 203 <= 633), but not: (-67 <= -236 <= 
+inf.0)
failed: (636 <= 891 <= +inf.0) and (-inf.0 <= -513 <= 663), but not: (636 <= 
512 <= +inf.0)
failed: (-588 <= -334 <= +inf.0) and (-913 <= 520 <= 559), but not: (-588 <= 
-846 <= +inf.0)
failed: (610 <= 611 <= 613) and (-900 <= -420 <= 499), but not: (610 <= 35 <= 
613)
failed: (-766 <= -551 <= -344) and (-986 <= 458 <= 994), but not: (-766 <= 
-1007 <= +inf.0)
failed: (-121 <= -77 <= -6) and (-159 <= 265 <= 978), but not: (-121 <= -334 <= 
+inf.0)
failed: (144 <= 182 <= 416) and (-145 <= 417 <= 579), but not: (144 <= 22 <= 
416)
failed: (183 <= 199 <= 224) and (-809 <= -371 <= 36), but not: (183 <= 66 <= 
224)
failed: (-410 <= -343 <= -142) and (-348 <= 155 <= 759), but not: (-410 <= -480 
<= +inf.0)
failed: (284 <= 418 <= 422) and (-792 <= -53 <= 879), but not: (284 <= 32 <= 
422)
failed: (917 <= 924 <= 957) and (-194 <= -183 <= 160), but not: (917 <= 148 <= 
957)
failed: (-439 <= -258 <= 388) and (-40 <= 774 <= 927), but not: (-439 <= -776 
<= +inf.0)
failed: (-619 <= -543 <= 357) and (-189 <= 161 <= +inf.0), but not: (-619 <= 
-704 <= +inf.0)
failed: (75 <= 140 <= 213) and (-872 <= 129 <= 466), but not: (75 <= 12 <= 213)
failed: (-611 <= -570 <= -501) and (-186 <= 610 <= 652), but not: (-611 <= -636 
<= +inf.0)
failed: (720 <= 731 <= 767) and (-303 <= 67 <= 528), but not: (720 <= 664 <= 
767)
failed: (-979 <= -868 <= -139) and (-39 <= 697 <= 804), but not: (-979 <= -1020 
<= +inf.0)
failed: (-695 <= -652 <= -647) and (-630 <= 503 <= 538), but not: (-695 <= 
-1024 <= +inf.0)
failed: (763 <= 781 <= 781) and (-inf.0 <= 426 <= 483), but not: (763 <= 517 <= 
781)
failed: (269 <= 426 <= 545) and (-271 <= -84 <= 496), but not: (269 <= 2 <= 545)
failed: (-625 <= -546 <= -543) and (-259 <= 783 <= 939), but not: (-625 <= -816 
<= +inf.0)
failed: (53 <= 272 <= 303) and (-396 <= -144 <= 794), but not: (53 <= 0 <= 303)
failed: (-73 <= -41 <= 722) and (-972 <= 197 <= 636), but not: (-73 <= -238 <= 
+inf.0)
failed: (559 <= 674 <= 866) and (-691 <= -186 <= 295), but not: (559 <= 160 <= 
866)
failed: (691 <= 740 <= 947) and (-662 <= 182 <= 421), but not: (691 <= 576 <= 
947)
failed: (201 <= 298 <= 880) and (-600 <= 482 <= 599), but not: (201 <= 8 <= 880)
failed: (344 <= 443 <= 860) and (-43 <= -5 <= 12), but not: (344 <= 0 <= 860)
failed: (303 <= 382 <= +inf.0) and (-inf.0 <= -35 <= 442), but not: (303 <= 34 
<= +inf.0)
failed: (-156 <= -111 <= 87) and (-601 <= 195 <= 197), but not: (-156 <= -240 
<= +inf.0)
failed: (139 <= 174 <= 649) and (-763 <= -357 <= 810), but not: (139 <= 36 <= 
649)
failed: (692 <= 769 <= 877) and (-557 <= -158 <= 962), but not: (692 <= 1 <= 
877)
failed: (-439 <= -214 <= -2) and (-251 <= 406 <= 474), but not: (-439 <= -472 
<= +inf.0)
failed: (239 <= 521 <= +inf.0) and (-516 <= -239 <= +inf.0), but not: (239 <= 8 
<= +inf.0)
failed: (311 <= 330 <= 754) and (-986 <= -392 <= 187), but not: (311 <= 258 <= 
754)
failed: (929 <= 937 <= 946) and (-247 <= -96 <= 108), but not: (929 <= 9 <= 946)
failed: (680 <= 708 <= 852) and (-947 <= 493 <= 693), but not: (680 <= 512 <= 
852)
failed: (686 <= 688 <= 688) and (-93 <= 112 <= 890), but not: (686 <= 640 <= 
688)
failed: (99 <= 847 <= 878) and (-751 <= -184 <= 82), but not: (99 <= 7 <= 878)
failed: (-449 <= -359 <= -346) and (-444 <= 854 <= 944), but not: (-449 <= -887 
<= +inf.0)
failed: (-519 <= -517 <= -515) and (-573 <= 309 <= 437), but not: (-519 <= -822 
<= +inf.0)
failed: (969 <= 972 <= 974) and (-590 <= 42 <= 613), but not: (969 <= 964 <= 
974)
failed: (545 <= 570 <= 619) and (-857 <= -376 <= 741), but not: (545 <= 50 <= 
619)
failed: (588 <= 939 <= 996) and (-205 <= 558 <= 727), but not: (588 <= 385 <= 
996)
failed: (-644 <= -622 <= -22) and (-218 <= 175 <= 221), but not: (-644 <= -752 
<= +inf.0)
failed: (-926 <= -911 <= 597) and (-264 <= 350 <= +inf.0), but not: (-926 <= 
-991 <= +inf.0)
failed: (-861 <= -856 <= -850) and (-596 <= 435 <= 606), but not: (-861 <= 
-1016 <= +inf.0)
failed: (-605 <= -513 <= -457) and (-786 <= 510 <= 510), but not: (-605 <= 
-1023 <= +inf.0)
failed: (-724 <= -688 <= -669) and (-25 <= 259 <= 373), but not: (-724 <= -944 
<= +inf.0)
failed: (-656 <= -510 <= -368) and (-inf.0 <= 656 <= 799), but not: (-656 <= 
-1022 <= +inf.0)
failed: (327 <= 438 <= 482) and (-inf.0 <= 732 <= 785), but not: (327 <= 290 <= 
482)
failed: (152 <= 216 <= 230) and (-24 <= 344 <= 573), but not: (152 <= 128 <= 
230)
failed: (-475 <= -465 <= -317) and (-368 <= 162 <= 648), but not: (-475 <= -499 
<= +inf.0)
failed: (-631 <= -549 <= 498) and (-inf.0 <= 511 <= 604), but not: (-631 <= 
-1024 <= +inf.0)
failed: (-939 <= -916 <= -255) and (-180 <= 437 <= 486), but not: (-939 <= -952 
<= +inf.0)
failed: (146 <= 250 <= 581) and (-16 <= 136 <= 971), but not: (146 <= 114 <= 
581)
failed: (-855 <= -720 <= -664) and (-150 <= 455 <= 1012), but not: (-855 <= 
-976 <= +inf.0)
failed: (238 <= 626 <= 748) and (-909 <= -386 <= 38), but not: (238 <= 0 <= 748)
failed: (-348 <= -211 <= 104) and (-inf.0 <= 430 <= 588), but not: (-348 <= 
-511 <= +inf.0)
failed: (742 <= 755 <= 868) and (-594 <= -43 <= 846), but not: (742 <= 34 <= 
868)
failed: (-92 <= -19 <= 350) and (-inf.0 <= 780 <= +inf.0), but not: (-92 <= 
-799 <= +inf.0)
failed: (223 <= 228 <= 239) and (-247 <= -95 <= 447), but not: (223 <= 68 <= 
239)
failed: (-502 <= -337 <= -143) and (-209 <= 506 <= 729), but not: (-502 <= -507 
<= +inf.0)
failed: (-62 <= -6 <= 124) and (-inf.0 <= 124 <= 457), but not: (-62 <= -126 <= 
+inf.0)
failed: (-242 <= -99 <= -69) and (-10 <= 247 <= 343), but not: (-242 <= -248 <= 
+inf.0)
failed: (867 <= 871 <= 954) and (-919 <= -457 <= 513), but not: (867 <= 320 <= 
954)
failed: (294 <= 513 <= 936) and (-27 <= 541 <= 824), but not: (294 <= 0 <= 936)
failed: (-251 <= -95 <= +inf.0) and (-487 <= 547 <= 906), but not: (-251 <= 
-640 <= +inf.0)
failed: (57 <= 459 <= 693) and (-557 <= -39 <= +inf.0), but not: (57 <= 2 <= 
693)
failed: (898 <= 941 <= 984) and (-inf.0 <= 869 <= 910), but not: (898 <= 136 <= 
984)
failed: (269 <= 279 <= 326) and (-837 <= -215 <= 998), but not: (269 <= 22 <= 
326)
failed: (260 <= 288 <= 407) and (-920 <= 183 <= 198), but not: (260 <= 256 <= 
407)
failed: (-675 <= -664 <= -403) and (-168 <= 717 <= 908), but not: (-675 <= -736 
<= +inf.0)
failed: (577 <= 587 <= 714) and (-712 <= 519 <= 543), but not: (577 <= 72 <= 
714)
failed: (-324 <= -315 <= 300) and (-281 <= 364 <= 412), but not: (-324 <= -383 
<= +inf.0)
failed: (352 <= 405 <= 411) and (-985 <= -41 <= 681), but not: (352 <= 0 <= 411)
failed: (648 <= 714 <= 937) and (-711 <= 138 <= 886), but not: (648 <= 576 <= 
937)
failed: (-457 <= -405 <= -31) and (-359 <= 366 <= 850), but not: (-457 <= -511 
<= +inf.0)
failed: (-34 <= -10 <= 713) and (-258 <= 517 <= 825), but not: (-34 <= -526 <= 
+inf.0)
failed: (276 <= 956 <= 997) and (-397 <= -215 <= 194), but not: (276 <= 148 <= 
997)
failed: (-984 <= -937 <= -709) and (-439 <= 237 <= 574), but not: (-984 <= 
-1006 <= +inf.0)
failed: (-838 <= -609 <= -253) and (-399 <= 268 <= 562), but not: (-838 <= -877 
<= +inf.0)
failed: (-158 <= -148 <= -144) and (-1017 <= 827 <= 873), but not: (-158 <= 
-956 <= +inf.0)
failed: (-303 <= -129 <= 928) and (-194 <= 673 <= 894), but not: (-303 <= -674 
<= +inf.0)
failed: (219 <= 292 <= 417) and (-424 <= -121 <= 734), but not: (219 <= 32 <= 
417)
failed: (-280 <= -274 <= -265) and (-454 <= 801 <= 840), but not: (-280 <= -818 
<= +inf.0)
failed: (-640 <= -600 <= -409) and (-253 <= 953 <= 975), but not: (-640 <= 
-1024 <= +inf.0)
failed: (448 <= 727 <= 988) and (-438 <= -23 <= 1004), but not: (448 <= 22 <= 
988)
failed: (472 <= 525 <= 542) and (-57 <= 652 <= 774), but not: (472 <= 1 <= 542)
failed: (454 <= 476 <= 489) and (-104 <= -34 <= 732), but not: (454 <= 0 <= 489)
scheme@(guile-user)> (repeated-test-bounds 1000 logior old-logior-bounds)
failed: (-54 <= 284 <= 811) and (-256 <= -122 <= 80), but not: (-54 <= -98 <= 
1023)
failed: (-573 <= 203 <= 845) and (-1020 <= -789 <= -309), but not: (-573 <= 
-789 <= -1)
failed: (-785 <= -730 <= 161) and (-155 <= 816 <= 1002), but not: (-155 <= -202 
<= 1023)
failed: (-664 <= -601 <= -227) and (-138 <= 263 <= 486), but not: (-138 <= -601 
<= -1)
failed: (-63 <= 90 <= 385) and (-589 <= -463 <= -283), but not: (-63 <= -389 <= 
-1)
failed: (-30 <= 203 <= 907) and (-262 <= -253 <= 168), but not: (-30 <= -53 <= 
1023)
failed: (-204 <= 68 <= 226) and (-942 <= -536 <= -453), but not: (-204 <= -532 
<= -1)
failed: (-155 <= 264 <= 477) and (-652 <= -622 <= -606), but not: (-155 <= -614 
<= -1)
failed: (-791 <= -729 <= -329) and (-347 <= 110 <= 727), but not: (-347 <= -657 
<= -1)
failed: (-275 <= 467 <= 526) and (-690 <= -546 <= -130), but not: (-275 <= -545 
<= -1)
failed: (-617 <= -519 <= -189) and (-58 <= 73 <= 104), but not: (-58 <= -519 <= 
-1)
failed: (-205 <= 37 <= 334) and (-307 <= -216 <= -151), but not: (-205 <= -211 
<= -1)
failed: (-347 <= 101 <= 120) and (-inf.0 <= -817 <= +inf.0), but not: (-347.0 
<= -785 <= +inf.0)
failed: (-551 <= -492 <= -487) and (-30 <= 440 <= 543), but not: (-30 <= -68 <= 
-1)
failed: (-40 <= 103 <= 341) and (-inf.0 <= -719 <= -262), but not: (-40.0 <= 
-649 <= -1)
failed: (-12 <= 165 <= 600) and (-687 <= -529 <= -258), but not: (-12 <= -529 
<= -1)
failed: (-202 <= 113 <= 123) and (-935 <= -823 <= -485), but not: (-202 <= -775 
<= -1)
failed: (-506 <= -404 <= -222) and (-248 <= 140 <= +inf.0), but not: (-248 <= 
-276 <= -1)
failed: (-474 <= -303 <= -213) and (-45 <= 224 <= 750), but not: (-45 <= -271 
<= -1)
failed: (-906 <= -855 <= -850) and (-490 <= 96 <= 772), but not: (-490 <= -791 
<= -1)
failed: (-416 <= 475 <= 710) and (-999 <= -646 <= 905), but not: (-416 <= -517 
<= 1023)
failed: (-649 <= 228 <= 437) and (-806 <= -781 <= -531), but not: (-649 <= -777 
<= -1)
failed: (-5 <= 129 <= 200) and (-inf.0 <= -300 <= 625), but not: (-5.0 <= -299 
<= 1023)
failed: (-inf.0 <= -607 <= 154) and (-81 <= 413 <= 642), but not: (-81.0 <= 
-579 <= 1023)
failed: (-182 <= 529 <= 566) and (-948 <= -316 <= 622), but not: (-182 <= -299 
<= 1023)
failed: (-597 <= -94 <= 346) and (-19 <= 98 <= 106), but not: (-19 <= -30 <= 
511)
failed: (-53 <= 28 <= 123) and (-545 <= -276 <= -72), but not: (-53 <= -260 <= 
-1)
failed: (-261 <= 309 <= 821) and (-906 <= -899 <= -877), but not: (-261 <= -643 
<= -1)
failed: (-932 <= -673 <= -478) and (-534 <= 120 <= 594), but not: (-534 <= -641 
<= -1)
failed: (-489 <= 191 <= 937) and (-964 <= -924 <= 772), but not: (-489 <= -769 
<= 1023)
failed: (-393 <= -310 <= -52) and (-203 <= 53 <= 355), but not: (-203 <= -257 
<= -1)
failed: (-740 <= -514 <= 721) and (-440 <= 375 <= 758), but not: (-440 <= -513 
<= 1023)
failed: (-995 <= -597 <= 988) and (-262 <= 142 <= 208), but not: (-262 <= -593 
<= 1023)
failed: (-752 <= -567 <= 66) and (-146 <= 344 <= 877), but not: (-146 <= -551 
<= 1023)
failed: (-966 <= -574 <= -380) and (-452 <= 65 <= 290), but not: (-452 <= -573 
<= -1)
failed: (-671 <= -609 <= 21) and (-71 <= 32 <= +inf.0), but not: (-71 <= -577 
<= +inf.0)
failed: (-122 <= 206 <= 270) and (-790 <= -461 <= 598), but not: (-122 <= -257 
<= 1023)
failed: (-625 <= 53 <= 459) and (-1006 <= -990 <= -968), but not: (-625 <= -969 
<= -1)
failed: (-733 <= -732 <= -703) and (-251 <= 187 <= 270), but not: (-251 <= -577 
<= -1)
failed: (-892 <= -838 <= -419) and (-382 <= 416 <= 941), but not: (-382 <= -582 
<= -1)
failed: (-204 <= 147 <= 580) and (-706 <= -609 <= 22), but not: (-204 <= -609 
<= 1023)
failed: (-29 <= 257 <= 635) and (-272 <= -249 <= 471), but not: (-29 <= -249 <= 
1023)
failed: (-951 <= -166 <= 961) and (-39 <= 115 <= 164), but not: (-39 <= -133 <= 
1023)
failed: (-346 <= -312 <= -150) and (-43 <= 177 <= 316), but not: (-43 <= -263 
<= -1)
failed: (-174 <= 427 <= 481) and (-838 <= -630 <= 755), but not: (-174 <= -597 
<= 1023)
failed: (-357 <= -230 <= +inf.0) and (-105 <= 362 <= 363), but not: (-105 <= 
-134 <= +inf.0)
failed: (-104 <= 102 <= 163) and (-573 <= -316 <= -240), but not: (-104 <= -282 
<= -1)
failed: (-503 <= 246 <= 779) and (-601 <= -533 <= 288), but not: (-503 <= -513 
<= 1023)
failed: (-782 <= -178 <= 210) and (-33 <= 93 <= 601), but not: (-33 <= -161 <= 
1023)
failed: (-130 <= 40 <= 277) and (-432 <= -395 <= -377), but not: (-130 <= -387 
<= -1)
failed: (-540 <= -501 <= -459) and (-424 <= 4 <= 287), but not: (-424 <= -497 
<= -1)
failed: (-1019 <= -995 <= -445) and (-542 <= 214 <= 720), but not: (-542 <= 
-801 <= -1)
failed: (-616 <= -531 <= +inf.0) and (-381 <= 493 <= 922), but not: (-381 <= 
-531 <= +inf.0)
failed: (-55 <= 762 <= 796) and (-961 <= -822 <= -312), but not: (-55 <= -262 
<= -1)
failed: (-443 <= 70 <= 198) and (-797 <= -774 <= -175), but not: (-443 <= -770 
<= -1)
failed: (-549 <= 105 <= 115) and (-953 <= -915 <= -657), but not: (-549 <= -915 
<= -1)
failed: (-247 <= 579 <= 649) and (-983 <= -903 <= -887), but not: (-247 <= -389 
<= -1)
failed: (-774 <= -719 <= -225) and (-196 <= 514 <= 815), but not: (-196 <= -205 
<= -1)
failed: (-896 <= -644 <= 340) and (-292 <= 74 <= 171), but not: (-292 <= -642 
<= 511)
failed: (-595 <= 366 <= 477) and (-812 <= -728 <= -453), but not: (-595 <= -658 
<= -1)
failed: (-787 <= -637 <= -187) and (-163 <= 160 <= 287), but not: (-163 <= -605 
<= -1)
failed: (-962 <= -881 <= 424) and (-176 <= 612 <= 713), but not: (-176 <= -273 
<= 1023)
failed: (-43 <= 122 <= 392) and (-423 <= -269 <= -80), but not: (-43 <= -261 <= 
-1)
failed: (-751 <= -682 <= -112) and (-84 <= 301 <= 998), but not: (-84 <= -641 
<= -1)
failed: (-79 <= 143 <= 278) and (-799 <= -510 <= -369), but not: (-79 <= -369 
<= -1)
failed: (-60 <= 263 <= 454) and (-106 <= -92 <= -90), but not: (-60 <= -89 <= 
-1)
failed: (-971 <= -826 <= -35) and (-398 <= 124 <= 434), but not: (-398 <= -770 
<= -1)
failed: (-828 <= -702 <= -598) and (-92 <= 30 <= 141), but not: (-92 <= -674 <= 
-1)
failed: (-974 <= -680 <= -638) and (-363 <= 81 <= 852), but not: (-363 <= -679 
<= -1)
failed: (-478 <= -456 <= -446) and (-173 <= 38 <= 323), but not: (-173 <= -450 
<= -1)
failed: (-841 <= -540 <= -82) and (-124 <= 106 <= 599), but not: (-124 <= -530 
<= -1)
failed: (-853 <= -847 <= -776) and (-325 <= 120 <= 637), but not: (-325 <= -775 
<= -1)
failed: (-630 <= -301 <= +inf.0) and (-31 <= 37 <= 383), but not: (-31 <= -265 
<= +inf.0)
failed: (-1021 <= -979 <= -871) and (-105 <= 687 <= 865), but not: (-105 <= 
-337 <= -1)
failed: (-inf.0 <= -406 <= 86) and (-75 <= 44 <= 69), but not: (-75.0 <= -402 
<= 127)
failed: (-45 <= 706 <= 949) and (-inf.0 <= -349 <= -146), but not: (-45.0 <= 
-285 <= -1)
failed: (-57 <= 321 <= 675) and (-462 <= -460 <= -365), but not: (-57 <= -139 
<= -1)
failed: (-14 <= 70 <= 88) and (-953 <= -294 <= 390), but not: (-14 <= -290 <= 
511)
failed: (-1011 <= -563 <= 378) and (-215 <= 346 <= 767), but not: (-215 <= -545 
<= 1023)
failed: (-41 <= 15 <= 246) and (-739 <= -496 <= 719), but not: (-41 <= -481 <= 
1023)
failed: (-391 <= 213 <= 278) and (-809 <= -587 <= 96), but not: (-391 <= -523 
<= 511)
failed: (-649 <= -445 <= -416) and (-269 <= 594 <= 1006), but not: (-269 <= 
-429 <= -1)
failed: (-985 <= -978 <= -519) and (-716 <= 71 <= 834), but not: (-716 <= -913 
<= -1)
failed: (-85 <= 19 <= 30) and (-849 <= -842 <= -333), but not: (-85 <= -841 <= 
-1)
failed: (-617 <= 49 <= 563) and (-1000 <= -760 <= 601), but not: (-617 <= -711 
<= 1023)
failed: (-948 <= -729 <= 188) and (-68 <= 37 <= 56), but not: (-68 <= -729 <= 
255)
failed: (-181 <= 167 <= +inf.0) and (-894 <= -560 <= -207), but not: (-181 <= 
-521 <= -1)
failed: (-847 <= -838 <= -698) and (-35 <= 39 <= 901), but not: (-35 <= -833 <= 
-1)
failed: (-100 <= 37 <= 541) and (-208 <= -159 <= -54), but not: (-100 <= -155 
<= -1)
scheme@(guile-user)> (repeated-test-bounds 1000 logxor old-logxor-bounds)
failed: (-723 <= -712 <= -702) and (158 <= 477 <= 1010), but not: (-723 <= -795 
<= -1)
failed: (-763 <= -465 <= -7) and (-inf.0 <= -589 <= -72), but not: (-763.0 <= 
924 <= -1)
failed: (-125 <= 361 <= 508) and (-563 <= -538 <= -235), but not: (-125 <= -881 
<= -1)
failed: (-969 <= -835 <= 552) and (-447 <= -422 <= -379), but not: (-447 <= 743 
<= -1)
failed: (-inf.0 <= -246 <= -94) and (-858 <= -797 <= 648), but not: (-858.0 <= 
1001 <= -1)
failed: (-932 <= -408 <= 175) and (-633 <= -567 <= -291), but not: (-633 <= 929 
<= -1)
failed: (-639 <= -268 <= +inf.0) and (-736 <= -601 <= -528), but not: (-639 <= 
851 <= -1)
failed: (577 <= 601 <= 952) and (-315 <= -302 <= -145), but not: (-315 <= -885 
<= -1)
failed: (-273 <= -117 <= 245) and (-inf.0 <= 643 <= 991), but not: (-273.0 <= 
-760 <= 1023)
failed: (-655 <= -328 <= -29) and (-804 <= -314 <= 191), but not: (-655 <= 126 
<= -1)
failed: (-934 <= -881 <= 609) and (-177 <= 267 <= 348), but not: (-177 <= -636 
<= 1023)
failed: (-396 <= -382 <= 634) and (663 <= 693 <= 781), but not: (-396 <= -969 
<= 1023)
failed: (-427 <= -191 <= 493) and (-715 <= -691 <= -652), but not: (-427 <= 524 
<= -1)
failed: (-694 <= -394 <= 509) and (-294 <= -242 <= -233), but not: (-294 <= 376 
<= -1)
failed: (-inf.0 <= -208 <= 86) and (-568 <= -279 <= 190), but not: (-568.0 <= 
473 <= 255)
failed: (-453 <= 690 <= 892) and (-483 <= -480 <= +inf.0), but not: (-453 <= 
-878 <= +inf.0)
failed: (-786 <= -764 <= -614) and (-445 <= 260 <= 330), but not: (-445 <= 
-1024 <= -1)
failed: (-397 <= -334 <= -163) and (-839 <= 217 <= 964), but not: (-397 <= -405 
<= -1)
failed: (210 <= 231 <= 239) and (-79 <= -53 <= 30), but not: (-79 <= -212 <= 
255)
failed: (-869 <= -402 <= 541) and (253 <= 622 <= 638), but not: (-869 <= -1024 
<= 1023)
failed: (-386 <= -70 <= 691) and (-inf.0 <= 482 <= 865), but not: (-386.0 <= 
-424 <= 1023)
failed: (-297 <= 229 <= 1005) and (-156 <= -29 <= 65), but not: (-156 <= -250 
<= 1023)
failed: (-290 <= -257 <= 740) and (-721 <= -402 <= -170), but not: (-290 <= 145 
<= -1)
failed: (-886 <= -621 <= -504) and (-618 <= -576 <= -418), but not: (-618 <= 83 
<= -1)
failed: (-927 <= -665 <= -244) and (-477 <= 186 <= 569), but not: (-477 <= -547 
<= -1)
failed: (634 <= 652 <= 697) and (-597 <= -487 <= 567), but not: (-597 <= -875 
<= 1023)
failed: (187 <= 546 <= 993) and (-690 <= -415 <= -243), but not: (-690 <= -957 
<= -1)
failed: (-813 <= 212 <= 620) and (-676 <= -516 <= 518), but not: (-676 <= -728 
<= 1023)
failed: (-929 <= -810 <= +inf.0) and (-989 <= -981 <= -955), but not: (-929 <= 
253 <= -1)
failed: (-43 <= -41 <= -27) and (-780 <= -674 <= -361), but not: (-43 <= 649 <= 
-1)
failed: (-696 <= -386 <= -347) and (-589 <= -509 <= 285), but not: (-589 <= 125 
<= -1)
failed: (-877 <= 622 <= 715) and (-754 <= -381 <= -339), but not: (-754 <= -787 
<= -1)
failed: (192 <= 385 <= 535) and (-577 <= -561 <= -498), but not: (-577 <= -946 
<= -1)
failed: (-402 <= -182 <= -101) and (-693 <= -693 <= -692), but not: (-402 <= 
513 <= -1)
failed: (825 <= 979 <= 1024) and (-511 <= -321 <= 245), but not: (-511 <= -660 
<= 2047)
failed: (490 <= 491 <= 593) and (257 <= 264 <= 361), but not: (490 <= 227 <= 
1023)
failed: (293 <= 402 <= 652) and (352 <= 477 <= 945), but not: (352 <= 79 <= 
1023)
failed: (-903 <= -524 <= -460) and (-650 <= -267 <= 612), but not: (-650 <= 769 
<= -1)
failed: (-inf.0 <= -234 <= 224) and (-1008 <= -674 <= 296), but not: (-1008.0 
<= 584 <= 511)
failed: (-348 <= -348 <= -282) and (-145 <= -112 <= 428), but not: (-145 <= 308 
<= -1)
failed: (-214 <= -158 <= 95) and (-976 <= -557 <= -494), but not: (-214 <= 689 
<= -1)
failed: (-735 <= -681 <= -480) and (-395 <= 30 <= 903), but not: (-395 <= -695 
<= -1)
failed: (-291 <= -55 <= 54) and (-inf.0 <= 709 <= 743), but not: (-291.0 <= 
-756 <= 1023)
failed: (-475 <= -295 <= 1009) and (-inf.0 <= 737 <= 973), but not: (-475.0 <= 
-968 <= 1023)
failed: (-844 <= -829 <= -693) and (-835 <= -175 <= +inf.0), but not: (-835 <= 
914 <= -1)
failed: (-936 <= -846 <= -772) and (-197 <= 190 <= 467), but not: (-197 <= 
-1012 <= -1)
failed: (-636 <= 6 <= 484) and (-775 <= -771 <= -725), but not: (-636 <= -773 
<= -1)
failed: (-78 <= -54 <= 901) and (-649 <= 226 <= 565), but not: (-78 <= -216 <= 
1023)
failed: (-742 <= -565 <= +inf.0) and (395 <= 441 <= 792), but not: (-742 <= 
-910 <= +inf.0)
failed: (-182 <= -49 <= 574) and (-58 <= 383 <= 657), but not: (-58 <= -336 <= 
1023)
failed: (-924 <= 356 <= 735) and (-872 <= -728 <= 285), but not: (-872 <= -948 
<= 1023)
failed: (696 <= 776 <= 929) and (218 <= 299 <= 367), but not: (696 <= 547 <= 
1023)
failed: (-387 <= -223 <= -170) and (-inf.0 <= 338 <= 1011), but not: (-387.0 <= 
-397 <= -1)
failed: (-5 <= 118 <= 614) and (-556 <= -467 <= -384), but not: (-5 <= -421 <= 
-1)
failed: (-790 <= -774 <= -763) and (-559 <= -494 <= 372), but not: (-559 <= 744 
<= -1)
failed: (-236 <= -158 <= 520) and (636 <= 712 <= 714), but not: (-236 <= -598 
<= 1023)
failed: (-893 <= -550 <= -304) and (-195 <= 850 <= 916), but not: (-195 <= -376 
<= -1)
failed: (-25 <= 199 <= 439) and (-964 <= -421 <= 178), but not: (-25 <= -356 <= 
511)
failed: (-836 <= -430 <= 709) and (119 <= 612 <= 628), but not: (-836 <= -970 
<= 1023)
failed: (-764 <= -604 <= -466) and (-544 <= -88 <= 423), but not: (-544 <= 524 
<= -1)
failed: (-180 <= 19 <= 233) and (-992 <= -880 <= -592), but not: (-180 <= -893 
<= -1)
failed: (145 <= 216 <= 855) and (-620 <= -518 <= -487), but not: (-620 <= -734 
<= -1)
failed: (598 <= 927 <= 954) and (-887 <= -17 <= 204), but not: (-887 <= -912 <= 
1023)
failed: (496 <= 555 <= 929) and (-383 <= -77 <= 225), but not: (-383 <= -616 <= 
1023)
failed: (-657 <= -340 <= -330) and (-93 <= 70 <= 84), but not: (-93 <= -278 <= 
-1)
failed: (-311 <= -269 <= 761) and (-645 <= -167 <= -12), but not: (-311 <= 426 
<= -1)
failed: (-654 <= -308 <= -60) and (-596 <= -54 <= 779), but not: (-596 <= 262 
<= -1)
failed: (-834 <= -787 <= -690) and (-726 <= -631 <= -629), but not: (-726 <= 
356 <= -1)
failed: (-182 <= -114 <= 26) and (-817 <= -432 <= -108), but not: (-182 <= 478 
<= -1)
failed: (-610 <= -343 <= -120) and (-693 <= -674 <= -407), but not: (-610 <= 
1015 <= -1)
failed: (184 <= 303 <= +inf.0) and (247 <= 302 <= 463), but not: (247 <= 1 <= 
+inf.0)
failed: (-71 <= 212 <= 362) and (-995 <= -741 <= -719), but not: (-71 <= -561 
<= -1)
failed: (-736 <= -322 <= 51) and (-253 <= 49 <= 296), but not: (-253 <= -369 <= 
511)
failed: (-850 <= -111 <= 430) and (-740 <= -524 <= -361), but not: (-740 <= 613 
<= -1)
failed: (-903 <= -695 <= -408) and (281 <= 281 <= 281), but not: (-903 <= -944 
<= -1)
failed: (-136 <= -96 <= -28) and (-640 <= -350 <= 557), but not: (-136 <= 258 
<= -1)
failed: (-750 <= -569 <= -448) and (-1009 <= -889 <= -639), but not: (-750 <= 
320 <= -1)
failed: (-604 <= 205 <= +inf.0) and (-930 <= -583 <= -460), but not: (-604 <= 
-652 <= -1)
failed: (-450 <= -90 <= 36) and (-729 <= -536 <= -317), but not: (-450 <= 590 
<= -1)
failed: (-792 <= -673 <= +inf.0) and (-244 <= -204 <= -138), but not: (-244 <= 
619 <= -1)
failed: (-545 <= 53 <= 895) and (-880 <= -867 <= +inf.0), but not: (-545 <= 
-856 <= +inf.0)
failed: (-872 <= -860 <= -557) and (-82 <= -60 <= -39), but not: (-82 <= 864 <= 
-1)
failed: (-85 <= 2 <= 847) and (-637 <= -482 <= 138), but not: (-85 <= -484 <= 
1023)
failed: (-423 <= -341 <= -100) and (-969 <= -950 <= -923), but not: (-423 <= 
737 <= -1)
failed: (-277 <= -266 <= -134) and (-inf.0 <= 680 <= 1011), but not: (-277.0 <= 
-930 <= -1)
failed: (488 <= 679 <= 764) and (-670 <= -32 <= 260), but not: (-670 <= -697 <= 
1023)
failed: (353 <= 550 <= 641) and (537 <= 826 <= 938), but not: (537 <= 284 <= 
1023)
failed: (-782 <= -731 <= -433) and (-311 <= 24 <= 270), but not: (-311 <= -707 
<= -1)
failed: (-996 <= -951 <= -845) and (-721 <= -568 <= -60), but not: (-721 <= 385 
<= -1)
failed: (-608 <= 456 <= 627) and (-255 <= -213 <= -97), but not: (-255 <= -285 
<= -1)
failed: (-834 <= -780 <= -390) and (-126 <= 469 <= 541), but not: (-126 <= -735 
<= -1)
failed: (471 <= 559 <= +inf.0) and (500 <= 536 <= 713), but not: (500 <= 55 <= 
+inf.0)
failed: (404 <= 666 <= 745) and (-375 <= -329 <= 103), but not: (-375 <= -979 
<= 1023)
failed: (-411 <= -80 <= +inf.0) and (-263 <= -142 <= -107), but not: (-263 <= 
194 <= -1)
failed: (500 <= 682 <= 739) and (-61 <= -17 <= 676), but not: (-61 <= -699 <= 
1023)
failed: (-879 <= -879 <= -809) and (-892 <= -678 <= -69), but not: (-879 <= 459 
<= -1)
failed: (-468 <= -449 <= -255) and (-433 <= -304 <= -300), but not: (-433 <= 
239 <= -1)
failed: (-999 <= -692 <= 210) and (-818 <= -186 <= -117), but not: (-818 <= 522 
<= -1)
failed: (517 <= 835 <= 886) and (-534 <= -41 <= 367), but not: (-534 <= -876 <= 
1023)
failed: (435 <= 480 <= 555) and (31 <= 282 <= 304), but not: (435 <= 250 <= 
1023)
failed: (-1000 <= -978 <= -849) and (-438 <= -422 <= -398), but not: (-438 <= 
628 <= -1)
failed: (810 <= 944 <= 980) and (-303 <= -161 <= 350), but not: (-303 <= -785 
<= 1023)
failed: (231 <= 309 <= 458) and (-160 <= -160 <= +inf.0), but not: (-160 <= 
-427 <= +inf.0)
failed: (772 <= 914 <= 944) and (-543 <= -484 <= -439), but not: (-543 <= -626 
<= -1)
failed: (-317 <= -147 <= 78) and (-49 <= 596 <= 608), but not: (-49 <= -711 <= 
1023)
failed: (-763 <= -521 <= -499) and (-608 <= -490 <= 40), but not: (-608 <= 993 
<= -1)
failed: (-758 <= 293 <= 542) and (-56 <= -52 <= -40), but not: (-56 <= -279 <= 
-1)
failed: (266 <= 270 <= 352) and (853 <= 878 <= 882), but not: (853 <= 608 <= 
1023)
failed: (-307 <= -109 <= -7) and (-745 <= -710 <= -303), but not: (-307 <= 681 
<= -1)
failed: (-786 <= -638 <= -69) and (304 <= 332 <= 429), but not: (-786 <= -818 
<= -1)
failed: (-375 <= -129 <= 641) and (-750 <= -695 <= -617), but not: (-375 <= 566 
<= -1)
failed: (560 <= 908 <= 1020) and (519 <= 557 <= 669), but not: (560 <= 417 <= 
1023)
failed: (366 <= 474 <= 683) and (-703 <= -700 <= -608), but not: (-703 <= -866 
<= -1)
failed: (-547 <= -254 <= -111) and (677 <= 728 <= 968), but not: (-547 <= -550 
<= -1)
failed: (-282 <= -168 <= +inf.0) and (-518 <= 493 <= 843), but not: (-282 <= 
-331 <= +inf.0)
failed: (-615 <= -534 <= -364) and (-1010 <= -966 <= -938), but not: (-615 <= 
464 <= -1)
failed: (-897 <= -598 <= -259) and (-778 <= -386 <= -367), but not: (-778 <= 
980 <= -1)
failed: (-inf.0 <= 761 <= 962) and (-452 <= -297 <= 183), but not: (-452.0 <= 
-978 <= 1023)
failed: (239 <= 487 <= 785) and (-693 <= -543 <= -483), but not: (-693 <= -1018 
<= -1)
failed: (-inf.0 <= -407 <= 282) and (-572 <= -172 <= -74), but not: (-572.0 <= 
317 <= -1)
failed: (-287 <= -47 <= 235) and (307 <= 351 <= 356), but not: (-287 <= -370 <= 
511)
failed: (255 <= 784 <= 916) and (-703 <= -187 <= 22), but not: (-703 <= -939 <= 
1023)
failed: (-516 <= -509 <= -509) and (-inf.0 <= -259 <= -246), but not: (-516.0 
<= 254 <= -1)
failed: (-287 <= -183 <= 722) and (-323 <= -145 <= -18), but not: (-287 <= 38 
<= -1)
failed: (-828 <= -740 <= -552) and (153 <= 393 <= 595), but not: (-828 <= -875 
<= -1)
failed: (-960 <= -947 <= -257) and (-inf.0 <= 69 <= 120), but not: (-960.0 <= 
-1016 <= -1)
failed: (-1005 <= -532 <= -512) and (-811 <= -315 <= -275), but not: (-811 <= 
809 <= -1)
failed: (-449 <= -422 <= -86) and (-643 <= -478 <= 235), but not: (-449 <= 120 
<= -1)
failed: (-508 <= -329 <= -213) and (241 <= 545 <= 810), but not: (-508 <= -874 
<= -1)
failed: (-116 <= -22 <= 58) and (-inf.0 <= -245 <= -70), but not: (-116.0 <= 
225 <= -1)
failed: (-445 <= 24 <= 385) and (-860 <= -784 <= -696), but not: (-445 <= -792 
<= -1)
failed: (-438 <= -425 <= -418) and (-479 <= -252 <= -135), but not: (-438 <= 
339 <= -1)
failed: (435 <= 797 <= 862) and (-825 <= -162 <= 46), but not: (-825 <= -957 <= 
1023)
failed: (-473 <= -4 <= 50) and (-983 <= -808 <= -437), but not: (-473 <= 804 <= 
-1)
failed: (-494 <= -412 <= -320) and (-641 <= -418 <= -103), but not: (-494 <= 58 
<= -1)
failed: (-591 <= -498 <= -379) and (-684 <= -683 <= -682), but not: (-591 <= 
859 <= -1)
failed: (-597 <= -592 <= -503) and (-999 <= 25 <= 37), but not: (-597 <= -599 
<= -1)
failed: (-264 <= -225 <= -180) and (-655 <= -116 <= 307), but not: (-264 <= 147 
<= -1)
failed: (-891 <= -656 <= -493) and (-198 <= 103 <= +inf.0), but not: (-198 <= 
-745 <= -1)
failed: (-295 <= 228 <= 698) and (-975 <= -912 <= -828), but not: (-295 <= -876 
<= -1)
failed: (-851 <= -822 <= 104) and (-207 <= -94 <= 430), but not: (-207 <= 872 
<= 511)
failed: (-426 <= -402 <= 548) and (-911 <= 46 <= 52), but not: (-426 <= -448 <= 
1023)
failed: (-451 <= -429 <= -414) and (-822 <= -181 <= -142), but not: (-451 <= 
280 <= -1)
failed: (-595 <= -511 <= -127) and (-919 <= -905 <= -863), but not: (-595 <= 
630 <= -1)
failed: (-1 <= 88 <= 909) and (-856 <= -629 <= -503), but not: (-1 <= -557 <= 
-1)
failed: (-460 <= -169 <= -133) and (-874 <= -4 <= 821), but not: (-460 <= 171 
<= -1)
failed: (-96 <= 198 <= 622) and (-370 <= -3 <= 464), but not: (-96 <= -197 <= 
1023)
failed: (-621 <= -387 <= 143) and (859 <= 862 <= 942), but not: (-621 <= -733 
<= 1023)
failed: (-629 <= -323 <= -262) and (-828 <= -827 <= -822), but not: (-629 <= 
632 <= -1)
failed: (-804 <= -34 <= 933) and (-127 <= -66 <= -2), but not: (-127 <= 96 <= 
-1)
failed: (-515 <= -39 <= 191) and (211 <= 828 <= 1009), but not: (-515 <= -795 
<= 1023)
failed: (-919 <= -791 <= -761) and (-325 <= 718 <= 862), but not: (-325 <= -473 
<= -1)
failed: (-977 <= -638 <= 875) and (-381 <= 48 <= 818), but not: (-381 <= -590 
<= 1023)
failed: (-inf.0 <= -567 <= 449) and (-308 <= -204 <= 74), but not: (-308.0 <= 
765 <= 511)
failed: (255 <= 351 <= 468) and (-872 <= -660 <= +inf.0), but not: (-872 <= 
-973 <= +inf.0)
failed: (-1005 <= 687 <= 734) and (-277 <= -152 <= +inf.0), but not: (-277 <= 
-569 <= +inf.0)
failed: (-310 <= -120 <= 362) and (438 <= 470 <= 479), but not: (-310 <= -418 
<= 511)
failed: (-642 <= -519 <= 194) and (292 <= 299 <= 414), but not: (-642 <= -814 
<= 511)
failed: (-758 <= -517 <= -469) and (-908 <= -378 <= +inf.0), but not: (-758 <= 
893 <= -1)
failed: (-inf.0 <= -924 <= -728) and (-174 <= -154 <= 418), but not: (-174.0 <= 
770 <= -1)
failed: (-775 <= -453 <= -420) and (-813 <= -100 <= 996), but not: (-775 <= 423 
<= -1)
failed: (-229 <= -70 <= 275) and (-603 <= -570 <= -548), but not: (-229 <= 636 
<= -1)
failed: (551 <= 660 <= 697) and (-222 <= -211 <= +inf.0), but not: (-222 <= 
-583 <= +inf.0)
failed: (-760 <= -747 <= -567) and (-380 <= -312 <= 483), but not: (-380 <= 989 
<= -1)
failed: (-716 <= -658 <= -412) and (95 <= 124 <= 560), but not: (-716 <= -750 
<= -1)
failed: (-243 <= -21 <= 47) and (-315 <= -196 <= -43), but not: (-243 <= 215 <= 
-1)
failed: (-183 <= 397 <= 680) and (-793 <= -714 <= -627), but not: (-183 <= -837 
<= -1)
failed: (-500 <= -73 <= 701) and (-738 <= 941 <= 950), but not: (-500 <= -998 
<= 1023)
failed: (505 <= 713 <= 731) and (-425 <= -410 <= -277), but not: (-425 <= -849 
<= -1)
failed: (-474 <= -217 <= -211) and (490 <= 666 <= 752), but not: (-474 <= -579 
<= -1)
failed: (-390 <= -322 <= -320) and (-941 <= -569 <= +inf.0), but not: (-390 <= 
889 <= -1)
failed: (258 <= 438 <= 614) and (-155 <= -135 <= +inf.0), but not: (-155 <= 
-305 <= +inf.0)
failed: (-996 <= -495 <= -357) and (-784 <= -626 <= -476), but not: (-784 <= 
927 <= -1)
failed: (-989 <= -31 <= 312) and (-165 <= 447 <= 747), but not: (-165 <= -418 
<= 1023)
failed: (-651 <= -637 <= -620) and (-649 <= 417 <= 622), but not: (-649 <= -990 
<= -1)
failed: (114 <= 141 <= 155) and (927 <= 981 <= 1021), but not: (927 <= 856 <= 
1023)
failed: (-241 <= 22 <= 610) and (-920 <= -535 <= 402), but not: (-241 <= -513 
<= 1023)
failed: (501 <= 507 <= 581) and (-795 <= -575 <= 395), but not: (-795 <= -966 
<= 1023)
failed: (-986 <= 230 <= 707) and (-876 <= -810 <= 58), but not: (-876 <= -976 
<= 1023)
failed: (-755 <= -580 <= 222) and (-1002 <= -763 <= -618), but not: (-755 <= 
185 <= -1)
failed: (243 <= 244 <= +inf.0) and (647 <= 728 <= 732), but not: (647 <= 556 <= 
+inf.0)
failed: (-476 <= -304 <= -188) and (-751 <= 629 <= 815), but not: (-476 <= -859 
<= -1)
failed: (592 <= 610 <= 671) and (-259 <= -259 <= -218), but not: (-259 <= -865 
<= -1)
failed: (-91 <= 165 <= 1005) and (-414 <= -387 <= -364), but not: (-91 <= -296 
<= -1)
failed: (-988 <= -672 <= -407) and (-456 <= 425 <= 899), but not: (-456 <= -823 
<= -1)
failed: (-294 <= -87 <= 60) and (-759 <= -706 <= -402), but not: (-294 <= 663 
<= -1)
failed: (-424 <= -81 <= -64) and (736 <= 740 <= 744), but not: (-424 <= -693 <= 
-1)
failed: (-668 <= 341 <= 558) and (-859 <= -674 <= -660), but not: (-668 <= 
-1013 <= -1)
failed: (486 <= 618 <= 619) and (-225 <= -35 <= 424), but not: (-225 <= -585 <= 
1023)
failed: (-993 <= -901 <= -850) and (-669 <= -453 <= 329), but not: (-669 <= 576 
<= -1)
failed: (-368 <= -197 <= 85) and (38 <= 261 <= 627), but not: (-368 <= -450 <= 
1023)
failed: (-368 <= -301 <= -269) and (-769 <= -237 <= -116), but not: (-368 <= 
448 <= -1)
failed: (-529 <= 349 <= 430) and (-59 <= -50 <= 53), but not: (-59 <= -365 <= 
511)
failed: (-479 <= -409 <= 843) and (-966 <= -152 <= -14), but not: (-479 <= 271 
<= -1)
failed: (-699 <= -575 <= 550) and (-476 <= -415 <= -215), but not: (-476 <= 928 
<= -1)
failed: (-447 <= -390 <= +inf.0) and (-82 <= 32 <= 70), but not: (-82 <= -422 
<= +inf.0)
failed: (-433 <= -295 <= 401) and (-922 <= -735 <= -584), but not: (-433 <= 
1016 <= -1)
failed: (-781 <= -617 <= 12) and (-389 <= 103 <= 686), but not: (-389 <= -528 
<= 1023)
failed: (-401 <= -300 <= 248) and (-inf.0 <= 613 <= 689), but not: (-401.0 <= 
-847 <= 1023)
failed: (-73 <= -61 <= 21) and (-999 <= -537 <= -502), but not: (-73 <= 548 <= 
-1)
failed: (-767 <= -607 <= -554) and (-224 <= 835 <= 899), but not: (-224 <= -286 
<= -1)
failed: (-654 <= -330 <= -255) and (-451 <= -356 <= -72), but not: (-451 <= 42 
<= -1)
failed: (520 <= 683 <= 823) and (986 <= 989 <= 1016), but not: (986 <= 374 <= 
1023)
failed: (-921 <= -466 <= -385) and (-996 <= -667 <= -249), but not: (-921 <= 
843 <= -1)
failed: (-913 <= 453 <= +inf.0) and (-956 <= -623 <= -214), but not: (-913 <= 
-940 <= -1)
failed: (754 <= 813 <= 907) and (543 <= 591 <= 790), but not: (754 <= 354 <= 
1023)
failed: (-347 <= 111 <= 844) and (-767 <= -390 <= 753), but not: (-347 <= -491 
<= 1023)
failed: (-301 <= -296 <= -283) and (-828 <= -504 <= 511), but not: (-301 <= 208 
<= -1)
failed: (-inf.0 <= -552 <= -20) and (-534 <= -344 <= 171), but not: (-534.0 <= 
880 <= -1)
failed: (309 <= 469 <= 569) and (-333 <= -7 <= 683), but not: (-333 <= -468 <= 
1023)
failed: (-774 <= -413 <= -299) and (-362 <= -331 <= -275), but not: (-362 <= 
214 <= -1)
failed: (-327 <= -314 <= -264) and (-864 <= -391 <= 139), but not: (-327 <= 191 
<= -1)
failed: (233 <= 289 <= 295) and (-271 <= -168 <= 309), but not: (-271 <= -391 
<= 511)
failed: (53 <= 216 <= 828) and (191 <= 200 <= 200), but not: (191 <= 16 <= 1023)
failed: (-835 <= -742 <= -433) and (-215 <= -101 <= -28), but not: (-215 <= 641 
<= -1)
failed: (329 <= 365 <= 830) and (-857 <= -522 <= +inf.0), but not: (-857 <= 
-869 <= +inf.0)
failed: (-445 <= -363 <= -5) and (299 <= 956 <= 977), but not: (-445 <= -727 <= 
-1)
failed: (-727 <= -377 <= 210) and (581 <= 934 <= 1019), but not: (-727 <= -735 
<= 1023)
failed: (-109 <= 360 <= 748) and (-414 <= -393 <= -382), but not: (-109 <= -225 
<= -1)
failed: (-36 <= 325 <= 583) and (-467 <= -190 <= -37), but not: (-36 <= -505 <= 
-1)
failed: (-693 <= -693 <= -563) and (-485 <= -371 <= -112), but not: (-485 <= 
966 <= -1)
failed: (-264 <= 775 <= 980) and (-671 <= -263 <= 802), but not: (-264 <= -514 
<= 1023)
failed: (-782 <= -683 <= 723) and (-inf.0 <= -113 <= -83), but not: (-782.0 <= 
730 <= -1)
failed: (-954 <= -230 <= 3) and (-826 <= -616 <= -311), but not: (-826 <= 642 
<= -1)
failed: (-459 <= -62 <= 465) and (-569 <= -280 <= -253), but not: (-459 <= 298 
<= -1)
failed: (-724 <= -377 <= -327) and (-951 <= -947 <= -174), but not: (-724 <= 
714 <= -1)
failed: (-113 <= 839 <= 904) and (-353 <= -146 <= 871), but not: (-113 <= -983 
<= 1023)
failed: (-353 <= -253 <= 87) and (-1005 <= -486 <= -287), but not: (-353 <= 281 
<= -1)
failed: (143 <= 806 <= 810) and (-767 <= -244 <= 770), but not: (-767 <= -982 
<= 1023)
failed: (602 <= 631 <= 775) and (-451 <= -115 <= 266), but not: (-451 <= -518 
<= 1023)
failed: (-874 <= -566 <= -360) and (-806 <= -610 <= -156), but not: (-806 <= 84 
<= -1)
failed: (42 <= 437 <= 697) and (-654 <= -580 <= -13), but not: (-654 <= -1015 
<= -1)
failed: (815 <= 859 <= 881) and (-401 <= -266 <= -223), but not: (-401 <= -595 
<= -1)
failed: (-217 <= -41 <= 104) and (-293 <= 260 <= 1016), but not: (-217 <= -301 
<= 1023)
failed: (-266 <= -52 <= -46) and (-741 <= -130 <= 276), but not: (-266 <= 178 
<= -1)
failed: (495 <= 501 <= 578) and (-173 <= -87 <= 86), but not: (-173 <= -420 <= 
1023)
failed: (-800 <= -349 <= -191) and (-953 <= -273 <= 105), but not: (-800 <= 76 
<= -1)
failed: (-501 <= -412 <= 100) and (-inf.0 <= -643 <= -190), but not: (-501.0 <= 
793 <= -1)
failed: (514 <= 697 <= 944) and (-651 <= -332 <= 626), but not: (-651 <= -1011 
<= 1023)
failed: (-665 <= 259 <= 509) and (-778 <= -593 <= +inf.0), but not: (-665 <= 
-852 <= +inf.0)
failed: (760 <= 816 <= 878) and (-146 <= -72 <= 1020), but not: (-146 <= -888 
<= 1023)
failed: (-926 <= -797 <= -150) and (-803 <= -233 <= 745), but not: (-803 <= 
1012 <= -1)
failed: (-489 <= -465 <= -400) and (-433 <= 805 <= 855), but not: (-433 <= -758 
<= -1)
failed: (-517 <= 476 <= 624) and (-657 <= -653 <= -651), but not: (-517 <= -849 
<= -1)
failed: (510 <= 703 <= 814) and (501 <= 672 <= 1014), but not: (510 <= 31 <= 
1023)
failed: (-166 <= -166 <= -146) and (-884 <= -880 <= -779), but not: (-166 <= 
970 <= -1)
failed: (-316 <= -193 <= -174) and (-634 <= 431 <= 740), but not: (-316 <= -368 
<= -1)
failed: (-610 <= -577 <= -561) and (-937 <= -936 <= 118), but not: (-610 <= 487 
<= -1)
failed: (-935 <= -760 <= -394) and (-1021 <= -645 <= 546), but not: (-935 <= 
115 <= -1)
failed: (231 <= 238 <= 290) and (160 <= 195 <= 220), but not: (231 <= 45 <= 511)
failed: (26 <= 287 <= 479) and (388 <= 506 <= 812), but not: (388 <= 229 <= 
1023)
failed: (-1017 <= -787 <= -386) and (-684 <= -533 <= -152), but not: (-684 <= 
262 <= -1)
failed: (-71 <= 146 <= 190) and (-906 <= -631 <= -599), but not: (-71 <= -741 
<= -1)
failed: (-702 <= -685 <= -223) and (-677 <= -182 <= 789), but not: (-677 <= 537 
<= -1)
failed: (-488 <= -286 <= -183) and (793 <= 858 <= 965), but not: (-488 <= -584 
<= -1)
failed: (-844 <= -268 <= -141) and (-140 <= 145 <= 217), but not: (-140 <= -411 
<= -1)
failed: (-490 <= -130 <= 596) and (-669 <= -633 <= -488), but not: (-490 <= 761 
<= -1)
failed: (119 <= 285 <= 869) and (-729 <= -717 <= -633), but not: (-729 <= -978 
<= -1)
failed: (255 <= 381 <= 954) and (268 <= 284 <= 348), but not: (268 <= 97 <= 
1023)
failed: (-342 <= -279 <= -237) and (-324 <= -230 <= -135), but not: (-324 <= 
499 <= -1)
failed: (-438 <= 314 <= 857) and (-874 <= -785 <= -276), but not: (-438 <= -555 
<= -1)
failed: (-640 <= -536 <= -439) and (-787 <= -735 <= -214), but not: (-640 <= 
201 <= -1)
failed: (22 <= 68 <= 72) and (707 <= 720 <= 754), but not: (707 <= 660 <= 1023)
failed: (-351 <= -313 <= 71) and (-112 <= 124 <= 594), but not: (-112 <= -325 
<= 1023)
failed: (-545 <= -160 <= -150) and (-589 <= -549 <= -495), but not: (-545 <= 
699 <= -1)
failed: (-482 <= -145 <= 586) and (-190 <= 483 <= 657), but not: (-190 <= -372 
<= 1023)
failed: (-950 <= -726 <= -680) and (-780 <= -590 <= -448), but not: (-780 <= 
152 <= -1)
failed: (-326 <= -287 <= -282) and (-671 <= -643 <= -602), but not: (-326 <= 
924 <= -1)
failed: (-831 <= -706 <= -292) and (-557 <= -337 <= 54), but not: (-557 <= 913 
<= -1)
failed: (-100 <= 170 <= 424) and (-564 <= -99 <= 78), but not: (-100 <= -201 <= 
511)
failed: (-726 <= -539 <= 812) and (-inf.0 <= -135 <= -132), but not: (-726.0 <= 
668 <= -1)
failed: (-159 <= 190 <= 309) and (-975 <= -915 <= -334), but not: (-159 <= -813 
<= -1)
failed: (-699 <= -524 <= -421) and (-849 <= -426 <= 447), but not: (-699 <= 930 
<= -1)
failed: (-687 <= -536 <= 295) and (-637 <= -529 <= -320), but not: (-637 <= 7 
<= -1)
failed: (194 <= 656 <= +inf.0) and (571 <= 698 <= 757), but not: (571 <= 42 <= 
+inf.0)
failed: (313 <= 597 <= 848) and (-657 <= -406 <= 869), but not: (-657 <= -961 
<= 1023)
failed: (-289 <= -129 <= -15) and (-276 <= 356 <= 877), but not: (-276 <= -485 
<= -1)
failed: (-397 <= -293 <= -196) and (-257 <= -222 <= 371), but not: (-257 <= 505 
<= -1)
failed: (-789 <= -742 <= -710) and (-267 <= -104 <= 406), but not: (-267 <= 642 
<= -1)
failed: (78 <= 142 <= 406) and (81 <= 151 <= 669), but not: (81 <= 25 <= 1023)
failed: (-447 <= -315 <= -209) and (-245 <= -244 <= -244), but not: (-245 <= 
457 <= -1)
failed: (-183 <= -32 <= 353) and (-734 <= -304 <= -26), but not: (-183 <= 304 
<= -1)
failed: (-1013 <= -982 <= -518) and (-422 <= -280 <= 375), but not: (-422 <= 
706 <= -1)
failed: (184 <= 379 <= 594) and (-252 <= -247 <= -171), but not: (-252 <= -398 
<= -1)
failed: (124 <= 601 <= 651) and (714 <= 802 <= 808), but not: (714 <= 379 <= 
1023)
failed: (-834 <= 437 <= 986) and (-614 <= -527 <= -435), but not: (-614 <= -956 
<= -1)
failed: (-931 <= -442 <= -159) and (-447 <= -333 <= 195), but not: (-447 <= 245 
<= -1)
failed: (-847 <= -748 <= -361) and (-49 <= 2 <= 240), but not: (-49 <= -746 <= 
-1)
failed: (-776 <= -598 <= 27) and (-495 <= -378 <= -175), but not: (-495 <= 812 
<= -1)
failed: (-60 <= 546 <= 974) and (-607 <= -195 <= -140), but not: (-60 <= -737 
<= -1)
failed: (-711 <= -533 <= -486) and (-323 <= 449 <= 687), but not: (-323 <= -982 
<= -1)
failed: (-358 <= -351 <= 683) and (419 <= 545 <= 804), but not: (-358 <= -896 
<= 1023)
failed: (-620 <= -518 <= -393) and (-365 <= 364 <= 657), but not: (-365 <= -874 
<= -1)
failed: (-891 <= -293 <= -20) and (-20 <= 171 <= 301), but not: (-20 <= -400 <= 
-1)
failed: (-292 <= 16 <= 1013) and (-816 <= -615 <= -239), but not: (-292 <= -631 
<= -1)
failed: (-564 <= -274 <= 908) and (-922 <= -554 <= -451), but not: (-564 <= 824 
<= -1)
failed: (-747 <= -667 <= -332) and (465 <= 511 <= 605), but not: (-747 <= -870 
<= -1)
failed: (-68 <= 462 <= 492) and (-836 <= -135 <= 935), but not: (-68 <= -329 <= 
1023)
failed: (-570 <= -537 <= -13) and (-860 <= -369 <= 70), but not: (-570 <= 872 
<= -1)
failed: (698 <= 704 <= 743) and (392 <= 610 <= 938), but not: (698 <= 162 <= 
1023)
failed: (-740 <= -622 <= -492) and (-84 <= 58 <= 230), but not: (-84 <= -600 <= 
-1)
failed: (-231 <= -230 <= -230) and (-8 <= -6 <= 140), but not: (-8 <= 224 <= -1)
failed: (-122 <= -114 <= 38) and (-956 <= 230 <= 721), but not: (-122 <= -152 
<= 1023)
failed: (552 <= 784 <= 947) and (-530 <= -418 <= 196), but not: (-530 <= -690 
<= 1023)
failed: (-562 <= 507 <= 826) and (-690 <= -589 <= -91), but not: (-562 <= -952 
<= -1)
failed: (-810 <= -555 <= -516) and (-131 <= -123 <= -118), but not: (-131 <= 
592 <= -1)
failed: (413 <= 417 <= 436) and (57 <= 198 <= 457), but not: (413 <= 359 <= 511)
failed: (-231 <= -142 <= -50) and (-371 <= -90 <= 767), but not: (-231 <= 212 
<= -1)
failed: (-690 <= -593 <= 449) and (-786 <= -767 <= -729), but not: (-690 <= 174 
<= -1)
failed: (541 <= 573 <= 670) and (-528 <= -337 <= 749), but not: (-528 <= -878 
<= 1023)
failed: (-672 <= -459 <= 180) and (-256 <= 139 <= 158), but not: (-256 <= -322 
<= 255)
failed: (-419 <= -332 <= -320) and (517 <= 553 <= 650), but not: (-419 <= -867 
<= -1)
failed: (-676 <= -575 <= -307) and (-394 <= -308 <= 345), but not: (-394 <= 781 
<= -1)
failed: (-589 <= -341 <= -279) and (-41 <= 818 <= 930), but not: (-41 <= -615 
<= -1)
failed: (-621 <= -619 <= -564) and (99 <= 375 <= 760), but not: (-621 <= -798 
<= -1)
failed: (-842 <= -832 <= -828) and (-inf.0 <= -364 <= -350), but not: (-842.0 
<= 596 <= -1)
failed: (-670 <= -639 <= -600) and (-426 <= -176 <= 176), but not: (-426 <= 721 
<= -1)
failed: (-759 <= -100 <= 414) and (-1016 <= -728 <= 166), but not: (-759 <= 692 
<= 511)
failed: (-394 <= -362 <= -204) and (366 <= 874 <= 969), but not: (-394 <= -516 
<= -1)
failed: (-586 <= -251 <= -110) and (-501 <= -475 <= +inf.0), but not: (-501 <= 
288 <= -1)
failed: (-889 <= -487 <= -82) and (603 <= 638 <= 721), but not: (-889 <= -921 
<= -1)
failed: (-988 <= -607 <= 920) and (-51 <= 273 <= 617), but not: (-51 <= -848 <= 
1023)
failed: (-373 <= -213 <= 447) and (-505 <= -487 <= -366), but not: (-373 <= 306 
<= -1)
failed: (755 <= 756 <= 878) and (90 <= 147 <= 356), but not: (755 <= 615 <= 
1023)
failed: (-720 <= -372 <= 525) and (-731 <= -528 <= -74), but not: (-720 <= 892 
<= -1)
failed: (254 <= 318 <= 440) and (862 <= 968 <= 1017), but not: (862 <= 758 <= 
1023)
failed: (-300 <= -293 <= -82) and (569 <= 711 <= 897), but not: (-300 <= -996 
<= -1)
failed: (-633 <= -561 <= 644) and (-21 <= 151 <= 265), but not: (-21 <= -680 <= 
1023)
failed: (-274 <= -236 <= -172) and (-153 <= -120 <= 315), but not: (-153 <= 156 
<= -1)
failed: (-775 <= -727 <= -714) and (-578 <= -204 <= 864), but not: (-578 <= 541 
<= -1)
failed: (-937 <= 251 <= 948) and (-102 <= -92 <= 518), but not: (-102 <= -161 
<= 1023)
failed: (-211 <= -201 <= -185) and (177 <= 443 <= 698), but not: (-211 <= -372 
<= -1)
failed: (-666 <= -606 <= 511) and (351 <= 357 <= 519), but not: (-666 <= -825 
<= 1023)
failed: (-32 <= 327 <= 375) and (-824 <= -295 <= +inf.0), but not: (-32 <= -98 
<= +inf.0)
failed: (1002 <= 1012 <= 1015) and (861 <= 878 <= 961), but not: (1002 <= 154 
<= 1023)
failed: (-482 <= -68 <= 815) and (-inf.0 <= -905 <= -383), but not: (-482.0 <= 
971 <= -1)
failed: (-952 <= -747 <= -585) and (-831 <= -784 <= 220), but not: (-831 <= 485 
<= -1)
failed: (-664 <= -424 <= -349) and (-81 <= 516 <= 722), but not: (-81 <= -932 
<= -1)
failed: (-245 <= -76 <= 283) and (-1000 <= -518 <= -19), but not: (-245 <= 590 
<= -1)
failed: (-793 <= -512 <= -306) and (-778 <= -716 <= -684), but not: (-778 <= 
820 <= -1)
failed: (-799 <= -652 <= -592) and (-867 <= -556 <= 5), but not: (-799 <= 160 
<= -1)
failed: (-537 <= -444 <= -235) and (-546 <= -166 <= 353), but not: (-537 <= 286 
<= -1)
failed: (403 <= 412 <= 730) and (100 <= 440 <= 543), but not: (403 <= 36 <= 
1023)
failed: (-533 <= -450 <= -335) and (-926 <= -531 <= 965), but not: (-533 <= 979 
<= -1)
failed: (-322 <= -295 <= 251) and (213 <= 217 <= 631), but not: (-322 <= -512 
<= 1023)
failed: (-997 <= -638 <= 864) and (-75 <= 356 <= 1003), but not: (-75 <= -794 
<= 1023)
failed: (-6 <= 38 <= 47) and (-451 <= -301 <= 124), but not: (-6 <= -267 <= 127)
failed: (-922 <= -660 <= +inf.0) and (-175 <= 597 <= 777), but not: (-175 <= 
-199 <= +inf.0)
failed: (191 <= 765 <= 1001) and (679 <= 759 <= 985), but not: (679 <= 10 <= 
1023)
failed: (-290 <= -125 <= -99) and (-367 <= -367 <= -338), but not: (-290 <= 274 
<= -1)
failed: (38 <= 908 <= 922) and (-270 <= -206 <= -93), but not: (-270 <= -834 <= 
-1)
failed: (425 <= 453 <= 487) and (-741 <= -610 <= -338), but not: (-741 <= -933 
<= -1)
failed: (476 <= 559 <= 910) and (-667 <= -257 <= -233), but not: (-667 <= -816 
<= -1)
failed: (853 <= 872 <= 992) and (528 <= 710 <= 996), but not: (853 <= 430 <= 
1023)
failed: (-121 <= -34 <= 434) and (15 <= 243 <= 424), but not: (-121 <= -211 <= 
511)
failed: (-663 <= -354 <= -172) and (-inf.0 <= 565 <= 734), but not: (-663.0 <= 
-853 <= -1)
failed: (-526 <= -422 <= -374) and (-261 <= -144 <= 788), but not: (-261 <= 298 
<= -1)
failed: (-873 <= -321 <= -190) and (-inf.0 <= -510 <= -467), but not: (-873.0 
<= 189 <= -1)
failed: (-570 <= 277 <= 477) and (-656 <= -655 <= 882), but not: (-570 <= -924 
<= 1023)
failed: (-994 <= -307 <= +inf.0) and (-505 <= 576 <= 814), but not: (-505 <= 
-883 <= +inf.0)
failed: (571 <= 694 <= 730) and (-741 <= -381 <= 34), but not: (-741 <= -971 <= 
1023)
failed: (-700 <= -643 <= -642) and (-800 <= -591 <= 265), but not: (-700 <= 204 
<= -1)
failed: (-842 <= -679 <= 45) and (-846 <= -339 <= -150), but not: (-842 <= 1012 
<= -1)
failed: (-670 <= -321 <= -301) and (-957 <= -749 <= 804), but not: (-670 <= 940 
<= -1)
failed: (-186 <= -181 <= 648) and (-472 <= -330 <= -329), but not: (-186 <= 509 
<= -1)
failed: (-883 <= -309 <= -288) and (-718 <= -91 <= 66), but not: (-718 <= 366 
<= -1)
failed: (-265 <= -164 <= -32) and (-579 <= -472 <= -426), but not: (-265 <= 372 
<= -1)
failed: (-212 <= -155 <= 88) and (493 <= 535 <= 658), but not: (-212 <= -654 <= 
1023)
failed: (-129 <= 317 <= 930) and (-813 <= -797 <= -746), but not: (-129 <= -546 
<= -1)
failed: (-939 <= -564 <= -124) and (-1014 <= -776 <= -16), but not: (-939 <= 
308 <= -1)
failed: (-482 <= -89 <= 555) and (-565 <= -340 <= -246), but not: (-482 <= 267 
<= -1)
failed: (-inf.0 <= -318 <= 121) and (-684 <= -651 <= -243), but not: (-684.0 <= 
951 <= -1)
failed: (-336 <= -301 <= -119) and (-249 <= -225 <= -201), but not: (-249 <= 
460 <= -1)
failed: (-752 <= -695 <= -690) and (-516 <= -157 <= 217), but not: (-516 <= 554 
<= -1)
failed: (-902 <= -900 <= -580) and (-284 <= 51 <= 159), but not: (-284 <= -945 
<= -1)
failed: (-415 <= -214 <= -9) and (477 <= 852 <= 964), but not: (-415 <= -898 <= 
-1)
failed: (-229 <= -153 <= -2) and (-440 <= -352 <= 437), but not: (-229 <= 455 
<= -1)
failed: (590 <= 849 <= 974) and (-532 <= -313 <= 306), but not: (-532 <= -618 
<= 1023)
failed: (-inf.0 <= 224 <= 500) and (-795 <= -795 <= -793), but not: (-795.0 <= 
-1019 <= -1)
failed: (-488 <= -168 <= 675) and (-221 <= -57 <= -22), but not: (-221 <= 159 
<= -1)
failed: (-1024 <= -810 <= 280) and (-218 <= -131 <= 272), but not: (-218 <= 939 
<= 511)
failed: (-949 <= -931 <= -924) and (-309 <= -32 <= 95), but not: (-309 <= 957 
<= -1)
failed: (-inf.0 <= -25 <= 543) and (-117 <= 390 <= 434), but not: (-117.0 <= 
-415 <= 1023)
failed: (-570 <= -547 <= 601) and (-382 <= 263 <= 288), but not: (-382 <= -806 
<= 1023)
failed: (-677 <= -597 <= -583) and (-707 <= -194 <= 832), but not: (-677 <= 661 
<= -1)
failed: (-610 <= -564 <= -111) and (-824 <= -527 <= 57), but not: (-610 <= 61 
<= -1)
failed: (-184 <= 163 <= 509) and (-956 <= -101 <= 861), but not: (-184 <= -200 
<= 1023)
failed: (-545 <= -367 <= 403) and (-45 <= 240 <= 359), but not: (-45 <= -415 <= 
511)
failed: (-212 <= -38 <= +inf.0) and (274 <= 318 <= 382), but not: (-212 <= -284 
<= +inf.0)
failed: (-618 <= -536 <= 528) and (-619 <= -615 <= -498), but not: (-618 <= 113 
<= -1)
failed: (261 <= 265 <= 270) and (184 <= 401 <= 458), but not: (261 <= 152 <= 
511)
failed: (-616 <= 734 <= 988) and (-inf.0 <= -283 <= 52), but not: (-616.0 <= 
-965 <= 1023)
failed: (-515 <= -141 <= -55) and (-inf.0 <= 692 <= 692), but not: (-515.0 <= 
-569 <= -1)
failed: (509 <= 751 <= 891) and (-578 <= -40 <= 211), but not: (-578 <= -713 <= 
1023)
failed: (-91 <= 113 <= 452) and (-523 <= -500 <= 345), but not: (-91 <= -387 <= 
511)
failed: (-792 <= -777 <= -613) and (-904 <= -809 <= -277), but not: (-792 <= 32 
<= -1)
failed: (-709 <= -664 <= 598) and (-inf.0 <= -729 <= -635), but not: (-709.0 <= 
79 <= -1)
failed: (-140 <= -130 <= 35) and (-553 <= -205 <= -137), but not: (-140 <= 77 
<= -1)
failed: (-293 <= -275 <= -182) and (-769 <= 175 <= 655), but not: (-293 <= -446 
<= -1)
failed: (-502 <= -497 <= -494) and (742 <= 885 <= 938), but not: (-502 <= -646 
<= -1)
failed: (-603 <= -587 <= +inf.0) and (-903 <= -869 <= -687), but not: (-603 <= 
302 <= -1)
failed: (-630 <= -606 <= -555) and (-640 <= -49 <= 1), but not: (-630 <= 621 <= 
-1)
failed: (-80 <= 254 <= +inf.0) and (-inf.0 <= -291 <= -290), but not: (-80.0 <= 
-477 <= -1)
failed: (-421 <= 171 <= 1005) and (-936 <= -936 <= -682), but not: (-421 <= 
-781 <= -1)
failed: (238 <= 260 <= 582) and (241 <= 435 <= 493), but not: (241 <= 183 <= 
1023)
failed: (-399 <= 471 <= 1004) and (-339 <= -139 <= -31), but not: (-339 <= -350 
<= -1)
failed: (629 <= 674 <= 747) and (125 <= 648 <= 823), but not: (629 <= 42 <= 
1023)
failed: (-858 <= 766 <= 821) and (-519 <= -512 <= 441), but not: (-519 <= -770 
<= 1023)
failed: (-699 <= -574 <= -168) and (-inf.0 <= -190 <= 712), but not: (-699.0 <= 
640 <= -1)
failed: (480 <= 480 <= 501) and (-621 <= -620 <= 47), but not: (-621 <= -908 <= 
511)
failed: (-693 <= -581 <= 28) and (-inf.0 <= -321 <= 497), but not: (-693.0 <= 
772 <= 511)
failed: (-600 <= -393 <= 580) and (-178 <= 117 <= 572), but not: (-178 <= -510 
<= 1023)
failed: (-464 <= 523 <= +inf.0) and (-239 <= -173 <= 897), but not: (-239 <= 
-680 <= +inf.0)
failed: (921 <= 940 <= 946) and (136 <= 313 <= 389), but not: (921 <= 661 <= 
1023)
failed: (-inf.0 <= 596 <= 815) and (-423 <= -190 <= -43), but not: (-423.0 <= 
-746 <= -1)
failed: (-983 <= -750 <= -406) and (-inf.0 <= -300 <= -284), but not: (-983.0 
<= 966 <= -1)
failed: (-474 <= -330 <= +inf.0) and (-365 <= 203 <= 359), but not: (-365 <= 
-387 <= +inf.0)
failed: (-444 <= -319 <= -279) and (-603 <= -429 <= 28), but not: (-444 <= 146 
<= -1)
failed: (-26 <= 93 <= 371) and (-962 <= -377 <= 110), but not: (-26 <= -294 <= 
511)
failed: (-739 <= -422 <= -90) and (-21 <= -3 <= 319), but not: (-21 <= 423 <= 
-1)
failed: (-82 <= -80 <= -78) and (-730 <= -292 <= -232), but not: (-82 <= 364 <= 
-1)
failed: (-483 <= -479 <= -474) and (18 <= 732 <= 896), but not: (-483 <= -771 
<= -1)
failed: (-186 <= -89 <= 835) and (376 <= 377 <= 852), but not: (-186 <= -290 <= 
1023)
failed: (-748 <= -505 <= 223) and (-22 <= 620 <= 663), but not: (-22 <= -917 <= 
1023)
failed: (-850 <= -612 <= +inf.0) and (-63 <= 736 <= 965), but not: (-63 <= -132 
<= +inf.0)
failed: (-566 <= -157 <= -130) and (-196 <= 810 <= +inf.0), but not: (-196 <= 
-951 <= -1)
failed: (-367 <= -197 <= 306) and (-833 <= -266 <= -45), but not: (-367 <= 461 
<= -1)
failed: (693 <= 744 <= 959) and (-813 <= -258 <= 452), but not: (-813 <= -1002 
<= 1023)
failed: (-857 <= -313 <= 749) and (-519 <= -389 <= -316), but not: (-519 <= 188 
<= -1)
failed: (-546 <= -419 <= 376) and (-340 <= 115 <= 354), but not: (-340 <= -466 
<= 511)
failed: (-955 <= -508 <= 968) and (-546 <= -531 <= -523), but not: (-546 <= 
1001 <= -1)
failed: (704 <= 813 <= 860) and (74 <= 610 <= 872), but not: (704 <= 335 <= 
1023)
failed: (810 <= 911 <= 970) and (29 <= 641 <= 806), but not: (810 <= 270 <= 
1023)
failed: (-412 <= -379 <= -189) and (-591 <= -23 <= 42), but not: (-412 <= 364 
<= -1)
failed: (500 <= 510 <= 643) and (368 <= 420 <= 751), but not: (500 <= 90 <= 
1023)
failed: (802 <= 813 <= 909) and (383 <= 652 <= 655), but not: (802 <= 417 <= 
1023)
failed: (-588 <= -210 <= -27) and (-247 <= -243 <= -84), but not: (-247 <= 35 
<= -1)
failed: (-415 <= 327 <= 376) and (-663 <= -647 <= 31), but not: (-415 <= -962 
<= 511)
failed: (-610 <= -566 <= -555) and (-229 <= -226 <= -226), but not: (-229 <= 
724 <= -1)
failed: (-548 <= -277 <= 248) and (508 <= 521 <= 573), but not: (-548 <= -798 
<= 1023)
failed: (-964 <= -937 <= -796) and (-313 <= -200 <= 16), but not: (-313 <= 879 
<= -1)
failed: (-604 <= -535 <= -304) and (-632 <= -603 <= -135), but not: (-604 <= 76 
<= -1)
failed: (-992 <= -596 <= 70) and (-987 <= -987 <= -985), but not: (-987 <= 393 
<= -1)
failed: (-926 <= -896 <= -687) and (-1006 <= -949 <= -702), but not: (-926 <= 
203 <= -1)
failed: (490 <= 597 <= 847) and (-254 <= -52 <= -9), but not: (-254 <= -615 <= 
-1)
scheme@(guile-user)> 
--8<---------------cut here---------------end--------------->8---

(use-modules (srfi srfi-11))

(define (next-power-of-two n)
  (let lp ((out 1))
    (if (< n out)
        out
        (lp (ash out 1)))))

(define-inlinable (non-negative? n)
  (not (negative? n)))

(define (saturate+ n)
  (if (inf? n)
      +inf.0
      (1- (ash 1 (integer-length n)))))

(define (saturate- n)
  (if (inf? n)
      -inf.0
      (ash -1 (integer-length n))))

(define (lognot* n)
  (- -1 n))

(define (old-logand-bounds a0 a1 b0 b1)
  (define (logand-min a b)
    (if (and (negative? a) (negative? b))
        (let ((min (min a b)))
          (if (inf? min)
              -inf.0
              (- 1 (next-power-of-two (- min)))))
        0))
  (define (logand-max a b)
    (cond
     ((or (and (positive? a) (positive? b))
          (and (negative? a) (negative? b)))
      (min a b))
     (else (max a b))))

  (values (logand-min a0 b0)
          (logand-max a1 b1)))

(define (logand-bounds a0 a1 b0 b1)
  ;; (a0 <= a <= a1) and (b0 <= b <= b1)
  (cond ((and (non-negative? a0) (non-negative? b0))
         (values 0 (min a1 b1)))
        ((non-negative? a0)
         (values 0 a1))
        ((non-negative? b0)
         (values 0 b1))
        (else
         (values (saturate- (min a0 b0))
                 (cond ((and (negative? a1) (negative? b1))
                        (min a1 b1))
                       ((negative? a1)
                        b1)
                       ((negative? b1)
                        a1)
                       (else
                        (saturate+ (max a1 b1))))))))

(define (logsub a b)
  (logand a (lognot b)))

(define (old-logsub-bounds min-a max-a min-b max-b)
  (cond
   ((negative? max-b)
    ;; Sign bit always set on B, so result will never be negative.
    ;; If A might be negative (all leftmost bits 1), we don't know
    ;; how positive the result might be.
    (values 0 (if (negative? min-a) +inf.0 max-a)))
   ((negative? min-b)
    ;; Sign bit might be set on B.
    (values min-a (if (negative? min-a) +inf.0 max-a)))
   ((negative? min-a)
    ;; Sign bit never set on B -- result will have the sign of A.
    (values -inf.0 max-a))
   (else
    ;; Sign bit never set on A and never set on B -- the nice case.
    (values 0 max-a))))

(define (logsub-bounds a0 a1 b0 b1)
  (logand-bounds a0 a1 (lognot* b1) (lognot* b0)))

(define (logior-bounds a0 a1 b0 b1)
  ;; (a0 <= a <= a1) and (b0 <= b <= b1)
  (cond ((and (negative? a1) (negative? b1))
         (values (max a0 b0) -1))
        ((negative? a1)
         (values a0 -1))
        ((negative? b1)
         (values b0 -1))
        (else
         (values (cond ((and (non-negative? a0) (non-negative? b0))
                        (max a0 b0))
                       ((non-negative? a0)
                        b0)
                       ((non-negative? b0)
                        a0)
                       (else
                        (saturate- (min a0 b0))))
                 (saturate+ (max a1 b1))))))

(define (old-logior-bounds a0 a1 b0 b1)
  ;; Saturate all bits of val.
  (define (saturate val)
    (1- (next-power-of-two val)))
  (define (logior-min a b)
    (cond ((and (< a 0) (<= 0 b)) a)
          ((and (< b 0) (<= 0 a)) b)
          (else (max a b))))
  (define (logior-max a b)
    ;; If either operand is negative, just assume the max is -1.
    (cond
     ((or (< a 0) (< b 0)) -1)
     ((or (inf? a) (inf? b)) +inf.0)
     (else (saturate (logior a b)))))

  (values (logior-min a0 b0)
          (logior-max a1 b1)))

(define (logxor-bounds a0 a1 b0 b1)
  ;; (a0 <= a <= a1) and (b0 <= b <= b1)
  (cond ((and (non-negative? a0) (non-negative? b0))
         (values 0 (saturate+ (max a1 b1))))
        ((and (negative? a1) (negative? b1))
         (values 0 (saturate+ (min a0 b0))))
        ((and (non-negative? a0) (negative? b1))
         (values (saturate- (max a1 (lognot* b0))) -1))
        ((and (negative? a1) (non-negative? b0))
         (values (saturate- (max b1 (lognot* a0))) -1))
        ((and (negative? a0) (non-negative? a1)
              (negative? b0) (non-negative? b1))
         (values (saturate- (max a1 b1 (lognot* a0) (lognot* b0)))
                 (saturate+ (max a1 b1 (lognot* a0) (lognot* b0)))))
        (else
         (values (if (and (non-negative? a1) (negative? b0))
                     (saturate- (max a1 (lognot* b0)))
                     (saturate- (max b1 (lognot* a0))))
                 (if (and (non-negative? a1) (non-negative? b1))
                     (saturate+ (max a1 b1))
                     (saturate+ (min a0 b0)))))))

(define old-logxor-bounds old-logior-bounds)

(define (rand lo hi)
  (+ lo (random (- hi lo -1))))

(define (rand2 lo hi)
  (let ((a (rand lo hi))
        (b (rand lo hi)))
    (if (<= a b)
        (values a b)
        (values b a))))

(define (rand3 lo hi)
  (let-values (((lo hi) (rand2 lo hi)))
    (values (rand lo hi) lo hi)))

(define (rand3* lo hi)
  (let-values (((x lo hi) (rand3 lo hi)))
    (values x
            (if (zero? (random 20)) -inf.0 lo)
            (if (zero? (random 20)) +inf.0 hi))))

(define %lo -1024)
(define %hi 1024)

(define (test-bounds f fb)
  (let-values (((a a0 a1) (rand3* %lo %hi))
               ((b b0 b1) (rand3* %lo %hi)))
    (let-values (((r0 r1) (fb a0 a1 b0 b1))
                 ((result) (f a b)))
      (unless (<= r0 result r1)
        (format #t "failed: (~s <= ~s <= ~s) and (~s <= ~s <= ~s), but not: (~s 
<= ~s <= ~s)\n"
                a0 a a1
                b0 b b1
                r0 result r1)))))

(define (repeated-test-bounds n f fb)
  (let loop ((n n))
    (unless (zero? n)
      (test-bounds f fb)
      (loop (- n 1)))))