mirror of
				https://github.com/ethereum/solidity
				synced 2023-10-03 13:03:40 +00:00 
			
		
		
		
	
		
			
				
	
	
		
			19 lines
		
	
	
		
			321 B
		
	
	
	
		
			Solidity
		
	
	
	
	
	
			
		
		
	
	
			19 lines
		
	
	
		
			321 B
		
	
	
	
		
			Solidity
		
	
	
	
	
	
pragma experimental SMTChecker;
 | 
						|
 | 
						|
contract C {
 | 
						|
	uint[] a;
 | 
						|
	function h() internal returns (uint[] storage) {
 | 
						|
		if (a[2] == 0)
 | 
						|
			a[2] = 3;
 | 
						|
		return a;
 | 
						|
	}
 | 
						|
	function g() public {
 | 
						|
		h()[2] = 4;
 | 
						|
		assert(h()[2] == 3);
 | 
						|
	}
 | 
						|
}
 | 
						|
// ====
 | 
						|
// SMTIgnoreCex: yes
 | 
						|
// ----
 | 
						|
// Warning 6328: (191-210): CHC: Assertion violation happens here.
 |