1contract C {
2	bytes32 bhash;
3	address coin;
4	uint dif;
5	uint glimit;
6	uint number;
7	uint tstamp;
8	bytes mdata;
9	address sender;
10	bytes4 sig;
11	uint value;
12	uint gprice;
13	address origin;
14
15	function f() public payable {
16		bhash = blockhash(12);
17		coin = block.coinbase;
18		dif = block.difficulty;
19		glimit = block.gaslimit;
20		number = block.number;
21		tstamp = block.timestamp;
22		mdata = msg.data;
23		sender = msg.sender;
24		sig = msg.sig;
25		value = msg.value;
26		gprice = tx.gasprice;
27		origin = tx.origin;
28
29		fi();
30
31		assert(bhash == blockhash(122));
32		assert(coin != block.coinbase);
33		assert(dif != block.difficulty);
34		assert(glimit != block.gaslimit);
35		assert(number != block.number);
36		assert(tstamp != block.timestamp);
37		assert(mdata.length != msg.data.length);
38		assert(sender != msg.sender);
39		assert(sig != msg.sig);
40		assert(value != msg.value);
41		assert(gprice != tx.gasprice);
42		assert(origin != tx.origin);
43	}
44
45	function fi() internal view {
46		assert(bhash == blockhash(122));
47		assert(coin != block.coinbase);
48		assert(dif != block.difficulty);
49		assert(glimit != block.gaslimit);
50		assert(number != block.number);
51		assert(tstamp != block.timestamp);
52		assert(mdata.length != msg.data.length);
53		assert(sender != msg.sender);
54		assert(sig != msg.sig);
55		assert(value != msg.value);
56		assert(gprice != tx.gasprice);
57		assert(origin != tx.origin);
58	}
59}
60// ====
61// SMTEngine: all
62// SMTIgnoreCex: yes
63// ----
64// Warning 6328: (512-543): CHC: Assertion violation happens here.
65// Warning 6328: (547-577): CHC: Assertion violation happens here.
66// Warning 6328: (581-612): CHC: Assertion violation happens here.
67// Warning 6328: (616-648): CHC: Assertion violation happens here.
68// Warning 6328: (652-682): CHC: Assertion violation happens here.
69// Warning 6328: (686-719): CHC: Assertion violation happens here.
70// Warning 6328: (723-762): CHC: Assertion violation happens here.
71// Warning 6328: (766-794): CHC: Assertion violation happens here.
72// Warning 6328: (798-820): CHC: Assertion violation happens here.
73// Warning 6328: (824-850): CHC: Assertion violation happens here.
74// Warning 6328: (854-883): CHC: Assertion violation happens here.
75// Warning 6328: (887-914): CHC: Assertion violation happens here.
76// Warning 6328: (953-984): CHC: Assertion violation happens here.
77// Warning 6328: (988-1018): CHC: Assertion violation happens here.
78// Warning 6328: (1022-1053): CHC: Assertion violation happens here.
79// Warning 6328: (1057-1089): CHC: Assertion violation happens here.
80// Warning 6328: (1093-1123): CHC: Assertion violation happens here.
81// Warning 6328: (1127-1160): CHC: Assertion violation happens here.
82// Warning 6328: (1164-1203): CHC: Assertion violation happens here.
83// Warning 6328: (1207-1235): CHC: Assertion violation happens here.
84// Warning 6328: (1239-1261): CHC: Assertion violation happens here.
85// Warning 6328: (1265-1291): CHC: Assertion violation happens here.
86// Warning 6328: (1295-1324): CHC: Assertion violation happens here.
87// Warning 6328: (1328-1355): CHC: Assertion violation happens here.
88