Why does Oyente report different results on virtually identical contracts?

[gsalzer]

Consider the contracts

• VeniceCityToken.sol@main:0xaaf80137ddba52d009c45b047c0e6eb312e25ddb and
• MetadollarCrw.sol@main:0x0e32d4c9581ebffbdf5d920cc2252f379b88d562.

The runtime codes of these two contracts, on Solidity as well as on bytecode level, are identical except for two multiplicative constants in the fallback function: VeniceCityToken:

        if (now <= bonusEnds) {
            tokens = msg.value * 2800;
        } else {
            tokens = msg.value * 2100;
        }

vs. MetadollarCrw:

        if (now <= bonusEnds) {
            tokens = msg.value * 1200;
        } else {
            tokens = msg.value * 1000;
        }

Why does Oyente report a Timestamp Dependency for VeniceCityToken, but not for MetadollarCrw? Is it because z3 handles constraints with different costants differently?

I ran Oyente via its Docker image:

docker run -i -t luongnguyen/oyente
# other terminal
docker cp VeniceCityToken.sol 54092cbba517:/oyente
docker cp MetadollarCrw.sol 54092cbba517:/oyente
# In the Docker image:
root@54092cbba517:/oyente# python oyente/oyente.py -s VeniceCityToken.sol
root@54092cbba517:/oyente# python oyente/oyente.py -s MetadollarCrw.sol

The binary runtime codes differ, apart from the metadata, only with respect to these constants.

145c145
< 0x134 PUSH2  0x4b0 # dec. 1200
---
> 0x134 PUSH2  0xaf0 # dec. 2800
153c153
< 0x140 PUSH2  0x3e8 # dec. 1000
---
> 0x140 PUSH2  0x834 # dec. 2100