Symbolically executed tests fails on simple signed types

[hellwolf]

$ cat src/TestInt96BoundaryError.sol 
// SPDX-License-Identifier: GPL-3.0-or-later
pragma solidity ^0.8.6;

contract TestInt96BoundaryError {


    function id_int96(int96 x) pure external returns (int96) {
        return x;
    }

    function id_int128(int128 x) pure external returns (int128) {
        return x;
    }

    function id_uint128(uint128 x) pure external returns (uint128) {
        return x;
    }

}

$ cat src/TestInt96BoundaryError.t.sol 
// SPDX-License-Identifier: GPL-3.0-or-later
pragma solidity ^0.8.6;

import "ds-test/test.sol";

import "./TestInt96BoundaryError.sol";

contract TestInt96BoundaryErrorTest is DSTest {
    TestInt96BoundaryError t;

    function setUp() public {
        t = new TestInt96BoundaryError();
    }

    function test_basic_sanity_int96(int96 x) public {
        assertTrue(t.id_int96(x) == x);
    }

    function prove_basic_sanity_int96(int96 x) public {
        assertTrue(t.id_int96(x) == x);
    }
    function prove_basic_sanity_int128(int128 x) public {
        assertTrue(t.id_int128(x) == x);
    }
    function prove_basic_sanity_uint128(uint128 x) public {
        assertTrue(t.id_uint128(x) == x);
    }
}

$ dapp test
Running 4 tests for src/TestInt96BoundaryError.t.sol:TestInt96BoundaryErrorTest
[FAIL] prove_basic_sanity_int96(int96)
[PASS] test_basic_sanity_int96(int96) (runs: 100)
[PASS] prove_basic_sanity_uint128(uint128)
[FAIL] prove_basic_sanity_int128(int128)

Failure: prove_basic_sanity_int128(int128)

  Counterexample:
  
    result:   Revert
    calldata: prove_basic_sanity_int128(170141183460469231731687303715884105728)
  

Failure: prove_basic_sanity_int96(int96)

  Counterexample:
  
    result:   Revert
    calldata: prove_basic_sanity_int96(39614081257132168796771975168)

Both 39614081257132168796771975168 and 170141183460469231731687303715884105728 are not valid signed int values for those types.

[hellwolf]

It looks like duplicated with #899

[d-xo]

Thanks for the report! Closing as a duplicate.