mirror of
				https://github.com/ethereum/solidity
				synced 2023-10-03 13:03:40 +00:00 
			
		
		
		
	
		
			
				
	
	
		
			26 lines
		
	
	
		
			420 B
		
	
	
	
		
			Plaintext
		
	
	
	
	
	
			
		
		
	
	
			26 lines
		
	
	
		
			420 B
		
	
	
	
		
			Plaintext
		
	
	
	
	
	
| Warning: CHC: Assertion violation happens here.
 | |
| Counterexample:
 | |
| 
 | |
| x = 0
 | |
| 
 | |
| Transaction trace:
 | |
| B.constructor()
 | |
| B.f(0)
 | |
|  --> model_checker_contracts_all/input.sol:5:3:
 | |
|   |
 | |
| 5 | 		assert(x > 0);
 | |
|   | 		^^^^^^^^^^^^^
 | |
| 
 | |
| Warning: CHC: Assertion violation happens here.
 | |
| Counterexample:
 | |
| 
 | |
| y = 0
 | |
| 
 | |
| Transaction trace:
 | |
| A.constructor()
 | |
| A.g(0)
 | |
|   --> model_checker_contracts_all/input.sol:10:3:
 | |
|    |
 | |
| 10 | 		assert(y > 0);
 | |
|    | 		^^^^^^^^^^^^^
 |