Issues running signed integers

Given the two test examples below

    function test_assertLt_assertLe(int256 a, int256 b) public pure {
        vm.assume(a < b);
        assertLt(a, b);
        assertive(a, b);
    }
    function test_assertLt_assertLe(uint256 a, uint256 b) public pure {
        vm.assume(a < b);
        assertLt(a, b);
        assertLe(a, b);
    }

the assumption for the test that uses uint256 values is simplified to

#And ( { true #Equals VV0_a_114b9705:Int <Int VV1_b_114b9705:Int }

whereas for the one that uses int256 it is

#And { true #Equals b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ~> .K ==K #range ( #padToWidth ( 32 , #asByteStack (
 ( (chop ( VV0_a_114b9705:Int )) s<Word (chop ( VV1_b_114b9705:Int )) ) ) ) , 0 , minInt ( 32 , lengthBytes ( #padToWidth ( 32 , #asByteStack ( ( (chop ( VV0_a_114b9705:Int )) s<Word (chop ( VV1_b_114b970
5:Int )) ) ) ) ) ) ) +Bytes #range ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00Lc\xe5b\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x
00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" , ( lengthBytes ( #padToWidth ( 32 , #asByteStack ( ( (chop ( VV0_a_114b9705:Int )) s<Word (chop ( VV1_b_114b9705:Int )) ) ) ) ) +Int 132 ) , ( 
32 -Int minInt ( 32 , lengthBytes ( #padToWidth ( 32 , #asByteStack ( ( (chop ( VV0_a_114b9705:Int )) s<Word (chop ( VV1_b_114b9705:Int )) ) ) ) ) ) ) ) ~> .K } ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )

Start with the two test_assertLt_assertLe Solidity examples in the issue and reproduce the differing simplification of their assumptions. Compare the uint256 and int256 results; done means the signed-integer assumption is handled without expanding into the malformed byte-range expression shown.