Leo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							8d91ccf028
							
						
					 | 
					
						
						
							
							[SMTChecker] Add a new trusted mode which assumes that code that is
						
						
						
						
						
						
						
						available at compile time is trusted. 
						
					 | 
					
						2023-02-06 17:02:33 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Rodrigo Q. Saramago
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							feba4de509
							
						
					 | 
					
						
						
							
							Add paris constraints to SMTChecker
						
						
						
						
						
						
						
						Co-authored-by: Daniel <daniel@ekpyron.org>
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
Co-authored-by: Leo <leo@ethereum.org> 
						
					 | 
					
						2023-01-31 11:03:04 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							61160aa0e7
							
						
					 | 
					
						
						
							
							Add constraints correlating address(this).balance and msg.value
						
						
						
						
						
					 | 
					
						2021-08-25 21:10:08 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
						
						
							
						
						
							90c4623460
							
						
					 | 
					
						
						
							
							Some more base fees.
						
						
						
						
						
					 | 
					
						2021-08-12 16:37:21 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Mathias Baumann
							
						 
					 | 
					
						
						
						
						
							
						
						
							e197ebbdd1
							
						
					 | 
					
						
						
							
							Replace TypePointer with Type const*
						
						
						
						
						
					 | 
					
						2021-03-23 11:47:19 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Martin Blicha
							
						 
					 | 
					
						
						
						
						
							
						
						
							a49950cdf3
							
						
					 | 
					
						
						
							
							[SMTChecker] Added transaction constraints also for contract deployment
						
						
						
						
						
					 | 
					
						2021-02-01 16:46:34 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							a612daa783
							
						
					 | 
					
						
						
							
							Add msgvalue to cex
						
						
						
						
						
					 | 
					
						2021-01-21 19:05:44 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Martin Blicha
							
						 
					 | 
					
						
						
						
						
							
						
						
							be0a0f4d90
							
						
					 | 
					
						
						
							
							[SMTChecker] Added constraints for block properties
						
						
						
						
						
					 | 
					
						2020-12-29 22:17:44 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Martin Blicha
							
						 
					 | 
					
						
						
						
						
							
						
						
							bb0003f5ea
							
						
					 | 
					
						
						
							
							removed extra parameter from PredicateInstance::nondetInterface
						
						
						
						
						
					 | 
					
						2020-12-28 19:48:48 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							2cbf33ca1c
							
						
					 | 
					
						
						
							
							SMTChecker support ABI functions as UFs
						
						
						
						
						
					 | 
					
						2020-12-17 14:03:17 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							54f76e081a
							
						
					 | 
					
						
						
							
							[SMTChecker] Support crypto functions in CHC
						
						
						
						
						
					 | 
					
						2020-10-16 14:57:13 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							a2cdde1191
							
						
					 | 
					
						
						
							
							Add tx data to symbolic state
						
						
						
						
						
					 | 
					
						2020-10-13 17:49:04 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							18cf01c187
							
						
					 | 
					
						
						
							
							Add this and state to CHC
						
						
						
						
						
					 | 
					
						2020-10-12 11:11:52 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							a86f656704
							
						
					 | 
					
						
						
							
							Refactor state as tuple
						
						
						
						
						
					 | 
					
						2020-10-12 11:11:52 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							ac93ee1d08
							
						
					 | 
					
						
						
							
							Move error flag from CHC to SymbolicState
						
						
						
						
						
					 | 
					
						2020-09-28 12:37:57 +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 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							9e9f0c52e1
							
						
					 | 
					
						
						
							
							[SMTChecker] Support to bitwise
						
						
						
						
						
					 | 
					
						2020-05-27 20:59:00 +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
							
						 
					 | 
					
						
						
						
						
							
						
						
							05a85461fe
							
						
					 | 
					
						
						
							
							Symbolic state
						
						
						
						
						
					 | 
					
						2020-04-06 12:27:53 +02:00 | 
					
					
						
						
							
							
							
						
					 |