1contract C { 2 address coin; 3 uint dif; 4 uint gas; 5 uint number; 6 uint timestamp; 7 function f() public { 8 coin = block.coinbase; 9 dif = block.difficulty; 10 gas = block.gaslimit; 11 number = block.number; 12 timestamp = block.timestamp; 13 14 g(); 15 } 16 function g() internal view { 17 assert(uint160(coin) >= 0); // should hold 18 assert(dif >= 0); // should hold 19 assert(gas >= 0); // should hold 20 assert(number >= 0); // should hold 21 assert(timestamp >= 0); // should hold 22 23 assert(coin == block.coinbase); // should hold with CHC 24 assert(dif == block.difficulty); // should hold with CHC 25 assert(gas == block.gaslimit); // should hold with CHC 26 assert(number == block.number); // should hold with CHC 27 assert(timestamp == block.timestamp); // should hold with CHC 28 29 assert(coin == address(this)); // should fail 30 } 31} 32// ==== 33// SMTEngine: chc 34// ---- 35// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x0, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n C.g() -- internal call 36