Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							d31a2a8d21
							
						
					 | 
					
						
						
							
							CHC clears indices so that initial is 0 and current is 1
						
						
						
						
						
					 | 
					
						2020-02-12 11:47:58 -03:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Christian Parpart
							
						 
					 | 
					
						
						
						
						
							
						
						
							6b23412fae
							
						
					 | 
					
						
						
							
							C++ namespace cleanup (except tests).
						
						
						
						
						
					 | 
					
						2020-01-07 15:51:50 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							f4f83690f3
							
						
					 | 
					
						
						
							
							Replace some shared_ptr by unique_ptr or raw pointers
						
						
						
						
						
					 | 
					
						2020-01-06 14:16:49 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
						
						
							
						
						
							f6916a637e
							
						
					 | 
					
						
						
							
							Merge remote-tracking branch 'origin/develop' into develop_060
						
						
						
						
						
					 | 
					
						2019-12-09 17:16:58 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							225041738e
							
						
					 | 
					
						
						
							
							Add SMTCheckerTest for isoltest
						
						
						
						
						
					 | 
					
						2019-12-09 15:32:08 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
						
						
							
						
						
							e061f1e743
							
						
					 | 
					
						
						
							
							Merge remote-tracking branch 'origin/develop' into HEAD
						
						
						
						
						
					 | 
					
						2019-12-05 16:44:26 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							48c3a5c225
							
						
					 | 
					
						
						
							
							[SMTChecker] Create options to choose SMT solver in runtime
						
						
						
						
						
					 | 
					
						2019-12-04 17:31:44 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
						
						
							
						
						
							96d777d7f1
							
						
					 | 
					
						
						
							
							Merge commit 'a7d481fb9' into develop_060
						
						
						
						
						
					 | 
					
						2019-12-03 20:47:30 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							c09da092d2
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix constructors with local vars
						
						
						
						
						
					 | 
					
						2019-11-29 16:59:15 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							a352abe00d
							
						
					 | 
					
						
						
							
							[SMTChecker] Add support to constructors
						
						
						
						
						
					 | 
					
						2019-11-28 14:43:23 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							ddc478e3e4
							
						
					 | 
					
						
						
							
							Add CallbackKind and use it for the SMT solver
						
						
						
						
						
					 | 
					
						2019-11-21 22:10:21 +00:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
						
						
							
						
						
							216e1749f4
							
						
					 | 
					
						
						
							
							Merge remote-tracking branch 'origin/develop' into develop_060
						
						
						
						
						
					 | 
					
						2019-11-14 13:42:46 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							e3652627fd
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix ICE in CHC when function used as argument
						
						
						
						
						
					 | 
					
						2019-11-13 15:11:30 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							2e5a42836c
							
						
					 | 
					
						
						
							
							Merge pull request #7681 from ethereum/develop
						
						
						
						
						
						
						
						Merge develop into develop_060 
						
					 | 
					
						2019-11-11 16:42:03 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							6b10efff8c
							
						
					 | 
					
						
						
							
							Add CHCSmtLib2Interface
						
						
						
						
						
					 | 
					
						2019-11-07 11:12:11 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							21e65076b3
							
						
					 | 
					
						
						
							
							Merge pull request #7650 from ethereum/develop
						
						
						
						
						
						
						
						Merge develop into develop_060 
						
					 | 
					
						2019-11-06 21:56:55 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							10e70b8603
							
						
					 | 
					
						
						
							
							[SMTChecker] Support inheritance and resolve overrides
						
						
						
						
						
					 | 
					
						2019-11-06 11:00:06 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								chriseth
							
						 
					 | 
					
						
						
							
							
						
						
						
							
						
						
							4d99bf68f4
							
						
					 | 
					
						
						
							
							Merge pull request #7638 from ethereum/develop
						
						
						
						
						
						
						
						Merge develop into develop_060 
						
					 | 
					
						2019-11-05 17:33:54 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							c5e081dc8c
							
						
					 | 
					
						
						
							
							[SMTChecker] Refactor CHC loops and add if blocks
						
						
						
						
						
					 | 
					
						2019-11-05 09:28:59 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Daniel Kirchner
							
						 
					 | 
					
						
						
						
						
							
						
						
							3321fc56ea
							
						
					 | 
					
						
						
							
							Split fallback function and introduce "fallback()" and "receive()" syntax.
						
						
						
						
						
					 | 
					
						2019-11-04 17:17:58 +01:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							e1c238e25f
							
						
					 | 
					
						
						
							
							[SMTChecker] Add loop support
						
						
						
						
						
					 | 
					
						2019-09-13 12:40:53 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							1a70a46f9b
							
						
					 | 
					
						
						
							
							[CHC] Add function blocks and check asserts
						
						
						
						
						
					 | 
					
						2019-08-15 12:25:15 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							bef6228810
							
						
					 | 
					
						
						
							
							[SMTChecker] Create CHC constructor/interface/error blocks
						
						
						
						
						
					 | 
					
						2019-08-12 12:34:57 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							4214cd1354
							
						
					 | 
					
						
						
							
							[SMTChecker] Fix ICE when reporting cex concerning state vars from different source files
						
						
						
						
						
					 | 
					
						2019-08-10 20:56:52 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							369f8cd97f
							
						
					 | 
					
						
						
							
							[SMTChecker] CHC create function return variables
						
						
						
						
						
					 | 
					
						2019-08-05 12:36:51 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							b204f27047
							
						
					 | 
					
						
						
							
							[SMTChecker] EncodingContext config flag to accumulate assertions
						
						
						
						
						
					 | 
					
						2019-07-19 19:31:25 +02:00 | 
					
					
						
						
							
							
							
						
					 | 
				
			
				
					
						
							
							
								 
								Leonardo Alt
							
						 
					 | 
					
						
						
						
						
							
						
						
							03cc124f32
							
						
					 | 
					
						
						
							
							Add CHC skeleton
						
						
						
						
						
					 | 
					
						2019-07-19 11:52:05 +02:00 | 
					
					
						
						
							
							
							
						
					 |