Manticore returns wrong result on trivial function

[Simon1V]

Summary of the problem

Using Manticore's python API, a wrong result is returned on a slightly adapted "incremented" function.

Manticore version

Version: 0.3.8.dev220714

Python version

Python 3.8.10

OS / Environment

No LSB modules are available. Distributor ID: Ubuntu Description: Ubuntu 20.04.5 LTS Release: 20.04 Codename: focal

Dependencies

Solc 0.8.17+commit.8df45f5f.Linux.g++ z3-solver==4.8.17.0

Step to reproduce the behavior

Python script

def testIncremented2(): 
        m = ManticoreEVM()
        userAcc = m.create_account(balance=10000000)
        contractAcc = m.solidity_create_contract(contractSrc, owner=userAcc, balance=0)
    value = m.make_symbolic_value() 
    contractAcc.incremented2(value)
    for state in m.ready_states: 
        print("Can value be negative? {}".format(state.can_be_true(value < 0)))

and the function testIncremented2 simply

function incremented2(uint256 x) public returns(uint256)
    {
        return x + 1; 
    }

Expected behavior

Can value be negative? False

Actual behavior

Can value be negative? True

Any relevant logs

[gitsan13]

Hi @Simon1V I would like to give this issue a try.