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