Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							60a4f03d3d
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix ice in unsupported functions with multi return values
						
						
						
						
						
					 | 
					
						2019-05-16 18:23:42 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							3ea5c112d3
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix VariableUsage for IndexAccess
						
						
						
						
						
					 | 
					
						2019-05-10 11:28:10 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							89700dbcff
							
						
					 | 
					
						
						
							
							Merge pull request #6665 from ethereum/smt_inline_external_this
						
						
						
						
						
						
						
						[SMTChecker] Inline external function calls to `this` 
						
					 | 
					
						2019-05-09 19:09:08 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							ef32bf185f
							
						
					 | 
					
						
						
							
							[SMTChecker] Inline external function calls to this.
						
						
						
						
						
					 | 
					
						2019-05-09 16:53:30 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							6027383ae5
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix call to function at state var init
						
						
						
						
						
					 | 
					
						2019-05-09 16:12:44 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							3d52a6ca68
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix ICE in branch-inline function call-modify local variable
						
						
						
						
						
					 | 
					
						2019-05-09 09:15:11 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							0b046897ae
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix unsupported type assignment
						
						
						
						
						
					 | 
					
						2019-05-08 14:28:23 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							3c7540ceb2
							
						
					 | 
					
						
						
							
							[SMTChecker] Support tuples with multiple var decls
						
						
						
						
						
					 | 
					
						2019-05-07 16:57:27 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							2139c20776
							
						
					 | 
					
						
						
							
							[SMTChecker] Support delete
						
						
						
						
						
					 | 
					
						2019-05-06 18:32:10 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							e99efec085
							
						
					 | 
					
						
						
							
							Merge pull request #6652 from ethereum/smt_tuple_function
						
						
						
						
						
						
						
						[SMTChecker] Support tuples as function calls with multiple return values 
						
					 | 
					
						2019-05-06 15:19:24 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							80712f44cb
							
						
					 | 
					
						
						
							
							Fix short circuit with assignments
						
						
						
						
						
					 | 
					
						2019-05-06 11:04:43 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							5440a53d4d
							
						
					 | 
					
						
						
							
							[SMTChecker] Support tuples as function calls with multiple return values
						
						
						
						
						
					 | 
					
						2019-05-03 06:10:22 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							204dcf1771
							
						
					 | 
					
						
						
							
							[SMTChecker] Support tuple assignments
						
						
						
						
						
					 | 
					
						2019-05-02 12:55:34 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							6c7527ac90
							
						
					 | 
					
						
						
							
							[SMTChecker] Support tuple type declaration
						
						
						
						
						
					 | 
					
						2019-05-02 12:05:21 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							dd4e938265
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix ICE in inherited state var
						
						
						
						
						
					 | 
					
						2019-05-02 10:03:12 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							a6db37ac9c
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix bad cast in base constructor modifier.
						
						
						
						
						
					 | 
					
						2019-04-30 18:48:13 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							fc482de695
							
						
					 | 
					
						
						
							
							[SMTChecker] Support address members
						
						
						
						
						
					 | 
					
						2019-04-25 16:24:36 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							dd1afeba52
							
						
					 | 
					
						
						
							
							[SMTChecker] Support this as address
						
						
						
						
						
					 | 
					
						2019-04-18 17:56:52 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							ecd89393ee
							
						
					 | 
					
						
						
							
							[SMTChecker] Support contract type
						
						
						
						
						
					 | 
					
						2019-04-17 16:30:11 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Mathias Baumann
							
						 
					 | 
					
						
						
						
						
							
						
						
							efc8d79d53
							
						
					 | 
					
						
						
							
							Fix wrong location for inline asm blocks
						
						
						
						
						
					 | 
					
						2019-04-15 16:40:07 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							bf5792f7ca
							
						
					 | 
					
						
						
							
							Merge pull request #6483 from ethereum/smt_support_mod
						
						
						
						
						
						
						
						[SMTChecker] Support mod 
						
					 | 
					
						2019-04-15 13:42:18 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							73ac8f6220
							
						
					 | 
					
						
						
							
							Merge pull request #6421 from ethereum/smt_fix_variable_usage
						
						
						
						
						
						
						
						[SMTChecker] Refactor VariableUsage 
						
					 | 
					
						2019-04-15 13:39:10 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							af9f16e014
							
						
					 | 
					
						
						
							
							[SMTChecker] Support mod
						
						
						
						
						
					 | 
					
						2019-04-12 12:39:25 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							4fe303530a
							
						
					 | 
					
						
						
							
							[SMTChecker] Show unsupported warning for asm blocks
						
						
						
						
						
					 | 
					
						2019-04-05 16:41:15 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							79d8a4e13a
							
						
					 | 
					
						
						
							
							[SMTChecker] Refactor VariableUsage
						
						
						
						
						
					 | 
					
						2019-04-05 11:38:37 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							aa9b9aa87e
							
						
					 | 
					
						
						
							
							[SMTChecker] Support unary inc/dec for array/mapping access
						
						
						
						
						
					 | 
					
						2019-04-02 16:53:19 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							84251e5a22
							
						
					 | 
					
						
						
							
							Merge pull request #6405 from ethereum/smt_compound_assignment
						
						
						
						
						
						
						
						[SMTChecker] Support arithmetic compound assignment operators. 
						
					 | 
					
						2019-03-28 18:27:25 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							dadafed022
							
						
					 | 
					
						
						
							
							Short circuit tests
						
						
						
						
						
					 | 
					
						2019-03-28 16:08:30 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							a7e826a224
							
						
					 | 
					
						
						
							
							[SMTChecker] Implement short circuit
						
						
						
						
						
					 | 
					
						2019-03-28 16:08:30 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							c7e5468505
							
						
					 | 
					
						
						
							
							Arithmetic compound assignment operators tests
						
						
						
						
						
					 | 
					
						2019-03-28 15:27:52 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							2764d2f525
							
						
					 | 
					
						
						
							
							Tests that used to give false negatives
						
						
						
						
						
					 | 
					
						2019-03-28 14:32:47 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							2ae778bf0a
							
						
					 | 
					
						
						
							
							[SMTChecker] Add buggy short circuit test
						
						
						
						
						
					 | 
					
						2019-03-21 18:47:14 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							9659f40c8d
							
						
					 | 
					
						
						
							
							[SMTChecker] Support modifiers
						
						
						
						
						
					 | 
					
						2019-03-20 11:32:20 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							365b59b1f9
							
						
					 | 
					
						
						
							
							Add MerkleProof test that used to crash
						
						
						
						
						
					 | 
					
						2019-03-11 14:29:47 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							a8209e9899
							
						
					 | 
					
						
						
							
							[SMTChecker] Shortcut RationalNumber expressions
						
						
						
						
						
					 | 
					
						2019-03-11 12:53:49 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							02d0e609b9
							
						
					 | 
					
						
						
							
							[SMTChecker] Support enums
						
						
						
						
						
					 | 
					
						2019-03-07 15:15:12 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							29b2ab6f66
							
						
					 | 
					
						
						
							
							Handle aliasing
						
						
						
						
						
					 | 
					
						2019-03-06 11:29:54 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							cb6c2b33f8
							
						
					 | 
					
						
						
							
							Add tests
						
						
						
						
						
					 | 
					
						2019-03-06 11:29:26 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							e74f58130e
							
						
					 | 
					
						
						
							
							Add SMT type support to Solidity arrays
						
						
						
						
						
					 | 
					
						2019-03-06 11:29:26 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Mathias Baumann
							
						 
					 | 
					
						
						
						
						
							
						
						
							f782125463
							
						
					 | 
					
						
						
							
							Fix SMT Checker crash due to missing type information
						
						
						
						
						
					 | 
					
						2019-02-28 11:55:45 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							123d0857c5
							
						
					 | 
					
						
						
							
							[SMTChecker] Move tests that contain division to boost tests
						
						
						
						
						
					 | 
					
						2019-02-20 12:17:03 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Mathias Baumann
							
						 
					 | 
					
						
						
						
						
							
						
						
							a63f7ca9df
							
						
					 | 
					
						
						
							
							Fix crash due to missing type info
						
						
						
						
						
					 | 
					
						2019-02-19 17:28:44 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							34470f3549
							
						
					 | 
					
						
						
							
							[SMTChecker] Only check for overflow/underflow in the end of the function
						
						
						
						
						
					 | 
					
						2019-02-18 23:55:58 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							22cdfb18d4
							
						
					 | 
					
						
						
							
							[SMTChecker] Assert type is not function when assigning
						
						
						
						
						
					 | 
					
						2019-02-14 13:32:56 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							7f8ceaadab
							
						
					 | 
					
						
						
							
							[SMTChecker] Clear state knowledge after external function calls
						
						
						
						
						
					 | 
					
						2019-01-21 12:58:40 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							a10db051de
							
						
					 | 
					
						
						
							
							[SMTChecker] Support basic typecast
						
						
						
						
						
					 | 
					
						2019-01-16 13:00:54 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							9199718ec0
							
						
					 | 
					
						
						
							
							Clear all mapping knowledge after array variable assignment
						
						
						
						
						
					 | 
					
						2018-12-14 12:21:53 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							6a2809a582
							
						
					 | 
					
						
						
							
							[SMTChecker] Support to mapping
						
						
						
						
						
					 | 
					
						2018-12-14 12:21:53 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							08737e43dc
							
						
					 | 
					
						
						
							
							[SMTChecker] Use SymbolicFunctionVariable for uninterpreted functions
						
						
						
						
						
					 | 
					
						2018-12-11 11:28:25 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Kevin Kelley
							
						 
					 | 
					
						
						
						
						
							
						
						
							fb6fd1b3c2
							
						
					 | 
					
						
						
							
							add a 'readable' format for large hex values
						
						
						
						
						
					 | 
					
						2018-12-05 22:15:02 +01:00 | 
					
					
						
						
							
							
							
						
					 |