test/libsolidity/smtCheckerTests/storage_value_vars_3.sol


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

pragma experimental SMTChecker;
contract C
{
    function f(uint x) public {
        if (x == 0)
        {
            a = 0x0000000000000000000000000000000000000100;
            b = true;
        }
        else
        {
            a = 0x0000000000000000000000000000000000000200;
            b = false;
        }
        assert(b == (a < 0x0000000000000000000000000000000000000200));
    }

    function g() public view {
        require(a < 0x0000000000000000000000000000000000000100);
        assert(c >= 0);
    }
    address a;
    bool b;
    uint c;
}