Heuristic of the race condition detector does not give interesting result

Manticore version

https://github.com/trailofbits/manticore/tree/e4e0829b6c962a40356ce2d8d6ea3b5b9ad64965

Summary of the problem

The current heuristic of the race condition detector can be summarized as:

• Does a function write to a state variable which is read by another function?

This pattern does not give any interesting results, as it matches too many code without bug.

We could follow something closer to what oyente and securify do, like:

• Is the msg.value of an internal call independent of other transactions?

I am not sure that oyente/securify strategies give pertinent results, it may also lead to several cases where it's not a bug, so we may want to refine the heuristic.

Step to reproduce the behavior

contract ERC20{
    mapping(address => mapping(address => uint)) allowance;

    function approve(address to, uint val){
        if(allowance[msg.sender][to] + val > allowance[msg.sender][to]){
            allowance[msg.sender][to] += val;  
        }
    }

    function transfer(address from, uint val){
        if(allowance[from][msg.sender] >= val){
            allowance[from][msg.sender] -= val;
        }   
    }
}

Expected behavior

No bug

Actual behavior

$  manticore test.sol --detect-race-condition
Potential race condition (transaction order dependency):
Value has been stored in storage slot/index 107947620283194693777147330934714592376293967296602958269006860500381273712713 in transaction that called approve(address,uint256) and is now used in transaction that calls transfer(address,uint256).
An attacker seeing a transaction to transfer(address,uint256) could create a transaction to approve(address,uint256) with high gas and win a race.