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