Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							e38d0db683
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix internal error when array.push() is used as LHS of assignment
						
						
						
						
						
					 | 
					
						2020-11-02 13:32:53 +00:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							d3d77e482c
							
						
					 | 
					
						
						
							
							Fix ICE on conditions with tuples of rationals
						
						
						
						
						
					 | 
					
						2020-10-23 14:47:53 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							e61b731647
							
						
					 | 
					
						
						
							
							[SMTChecker] Support structs
						
						
						
						
						
					 | 
					
						2020-09-03 15:19:03 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Sachin Grover
							
						 
					 | 
					
						
						
						
						
							
						
						
							b7adb2aa42
							
						
					 | 
					
						
						
							
							Add SPDX license identifier if not present already in source file
						
						
						
						
						
						
						
						Fixes: #9220 
						
					 | 
					
						2020-07-17 20:24:12 +05:30 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Djordje Mijovic
							
						 
					 | 
					
						
						
						
						
							
						
						
							c6e4943089
							
						
					 | 
					
						
						
							
							Adding fixes for signedness warnings in libsolidity
						
						
						
						
						
						
						
						Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it> 
						
					 | 
					
						2020-06-10 10:41:55 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							45eba27424
							
						
					 | 
					
						
						
							
							Rename namespace
						
						
						
						
						
					 | 
					
						2020-05-20 12:55:18 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							087605ea02
							
						
					 | 
					
						
						
							
							Create libsmtutil
						
						
						
						
						
					 | 
					
						2020-05-20 12:55:18 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							a0c605aa85
							
						
					 | 
					
						
						
							
							[SMTChecker] Support array length
						
						
						
						
						
					 | 
					
						2020-05-14 23:32:29 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							5d9dd654cf
							
						
					 | 
					
						
						
							
							[SMTChecker] Add and use tuple sort
						
						
						
						
						
					 | 
					
						2020-04-08 18:26:03 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							2cfa44bba3
							
						
					 | 
					
						
						
							
							Allow constructing symbolic arrays from smt sort
						
						
						
						
						
					 | 
					
						2020-04-06 10:50:00 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Christian Parpart
							
						 
					 | 
					
						
						
						
						
							
						
						
							6b23412fae
							
						
					 | 
					
						
						
							
							C++ namespace cleanup (except tests).
						
						
						
						
						
					 | 
					
						2020-01-07 15:51:50 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							d818746e0c
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix ICE in abi.decode
						
						
						
						
						
					 | 
					
						2019-11-18 13:15:10 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							e3652627fd
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix ICE in CHC when function used as argument
						
						
						
						
						
					 | 
					
						2019-11-13 15:11:30 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							360f868836
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix literal string type mismatch
						
						
						
						
						
					 | 
					
						2019-08-10 21:51:46 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							6bcbeb1d23
							
						
					 | 
					
						
						
							
							[SMTChecker] Reset SSA index to 0 instead of increasing in context reset
						
						
						
						
						
					 | 
					
						2019-07-25 14:16:34 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							4aebdcc442
							
						
					 | 
					
						
						
							
							[SMTChecker] Allow FunctionSort to be created via sort and not type
						
						
						
						
						
					 | 
					
						2019-07-04 12:00:24 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							934e00d235
							
						
					 | 
					
						
						
							
							[SMTChecker] SymbolicVariables use EncodingContext to declare SMT vars
						
						
						
						
						
					 | 
					
						2019-07-03 16:05:56 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							fac383a233
							
						
					 | 
					
						
						
							
							Move SMT specific code into smt namespace
						
						
						
						
						
					 | 
					
						2019-05-10 20:03:11 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							c8a017ccd6
							
						
					 | 
					
						
						
							
							[SMTChecker] Use unique_ptr instead of shared_ptr where applicable.
						
						
						
						
						
					 | 
					
						2019-05-09 16:34:22 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							6c7527ac90
							
						
					 | 
					
						
						
							
							[SMTChecker] Support tuple type declaration
						
						
						
						
						
					 | 
					
						2019-05-02 12:05:21 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							07fac9e381
							
						
					 | 
					
						
						
							
							[SMTChecker] Allow SymbolicVariable from smt::Sort
						
						
						
						
						
					 | 
					
						2019-04-15 14:52:46 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							02d0e609b9
							
						
					 | 
					
						
						
							
							[SMTChecker] Support enums
						
						
						
						
						
					 | 
					
						2019-03-07 15:15:12 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							e74f58130e
							
						
					 | 
					
						
						
							
							Add SMT type support to Solidity arrays
						
						
						
						
						
					 | 
					
						2019-03-06 11:29:26 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							cce377833a
							
						
					 | 
					
						
						
							
							Sort includes in libsolidity/formal
						
						
						
						
						
					 | 
					
						2018-12-17 18:26:10 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							6a2809a582
							
						
					 | 
					
						
						
							
							[SMTChecker] Support to mapping
						
						
						
						
						
					 | 
					
						2018-12-14 12:21:53 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							de46bb2c42
							
						
					 | 
					
						
						
							
							[SMTChecker] Introduce SymbolicFunctionVariable
						
						
						
						
						
					 | 
					
						2018-12-10 11:34:29 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							b9f424e373
							
						
					 | 
					
						
						
							
							[SMTChecker] Simplify symbolic variables
						
						
						
						
						
					 | 
					
						2018-12-05 09:56:52 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							ec84a7dc9b
							
						
					 | 
					
						
						
							
							[SMTChecker] Refactor setZeroValue and setUnknownValue
						
						
						
						
						
					 | 
					
						2018-11-22 16:42:51 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							70bb0eaf95
							
						
					 | 
					
						
						
							
							[SMTChecker] Implement uninterpreted functions and use it for blockhash()
						
						
						
						
						
					 | 
					
						2018-11-15 09:12:42 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							d8cbf321da
							
						
					 | 
					
						
						
							
							Grouping of symbolic variables in the same file and support to FixedBytes
						
						
						
						
						
					 | 
					
						2018-10-25 09:30:48 +02:00 | 
					
					
						
						
							
							
							
						
					 |