-
Notifications
You must be signed in to change notification settings - Fork 479
Open
Labels
Description
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