| 
							
							
								 Alexander Arlt | aac7a1e434 | Apply modernize-pass-by-value. | 2020-04-14 10:32:13 -05:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 4fc9920112 | Use tuple sort name plus index for field name | 2020-04-09 12:59:57 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 5d9dd654cf | [SMTChecker] Add and use tuple sort | 2020-04-08 18:26:03 +02:00 |  | 
			
				
					| 
							
							
								 chriseth | 823a119117 | Merge pull request #8570 from aarlt/clang-tidy-apply-modernize-use-emplace clang-tidy: Apply modernize-use-emplace. | 2020-04-07 17:28:50 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | e3ec22124e | [SMTChecker] Fix ICE in CHC internal calls | 2020-04-07 01:09:03 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 05a85461fe | Symbolic state | 2020-04-06 12:27:53 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 2cfa44bba3 | Allow constructing symbolic arrays from smt sort | 2020-04-06 10:50:00 +02:00 |  | 
			
				
					| 
							
							
								 Alexander Arlt | 90bb1d8a7c | Apply modernize-use-emplace. | 2020-04-02 17:35:48 -05:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | d2f65ea8b1 | [SMTChecker] Add SortProvider | 2020-03-26 14:55:54 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 07368c2e1e | Add support to internal function calls | 2020-03-11 16:29:07 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo | 32ca1a5e26 | Merge pull request #8311 from ethereum/smt_split_2 [SMTChecker] Change CHC encoding from explicit CFG to function forests | 2020-03-03 13:16:14 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 3bee348525 | Change CHC encoding to functions forest instead of explicit CFG | 2020-03-03 12:12:26 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 96a230af50 | [SMTChecker] Fix ICEs with tuples | 2020-03-03 11:35:58 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | d31a2a8d21 | CHC clears indices so that initial is 0 and current is 1 | 2020-02-12 11:47:58 -03:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 34d64761d9 | Extract symbolicArguments function | 2020-02-12 11:47:58 -03:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 6451a4d2a0 | Move VerificationTarget and add BMCVerificationTarget | 2020-02-12 11:47:58 -03:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | ba576bc6c3 | Fix new namespaces | 2020-02-12 10:35:44 -03:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | a02308cfa5 | Replace void cast by maybe_unused | 2020-01-09 13:41:30 +01:00 |  | 
			
				
					| 
							
							
								 Christian Parpart | 345f9928ab | Library libdevcore renamed to libsolutil. | 2020-01-07 15:51:50 +01: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 | 7be6b54fc7 | Add comment | 2019-12-04 17:31:44 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 48c3a5c225 | [SMTChecker] Create options to choose SMT solver in runtime | 2019-12-04 17:31:44 +01:00 |  | 
			
				
					| 
							
							
								 chriseth | 42d9a8e962 | Merge remote-tracking branch 'origin/develop' into develop_060 | 2019-12-04 17:01:44 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 67d82fc8a7 | [SMTChecker] Use rlimit instead of tlimit for SMT queries | 2019-12-04 11:52:18 +01:00 |  | 
			
				
					| 
							
							
								 chriseth | 2f11ac3590 | Merge remote-tracking branch 'origin/develop' into develop_060 | 2019-12-03 21:17:15 +01:00 |  | 
			
				
					| 
							
							
								 chriseth | 96d777d7f1 | Merge commit 'a7d481fb9' into develop_060 | 2019-12-03 20:47:30 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | b1577f5e46 | [SMTChecker] Fix ICE in array of structs type | 2019-12-03 01:12:30 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo | a7d481fb94 | Merge pull request #7851 from ethereum/smt_fix_function_type [SMTChecker] Fix ICE for arrays and mappings of functions. | 2019-11-30 13:15:08 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo | 767ce4417f | Merge pull request #7850 from ethereum/smt_fix_typetype [SMTChecker] Fix visit to IndexAccess that has type Type | 2019-11-29 18:18:26 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 5adc2a40b9 | [SMTChecker] Fix ICE for arrays and mappings of functions. | 2019-11-29 18:06:44 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 9eda95caf9 | [SMTChecker] Fix visit to IndexAccess that has type Type | 2019-11-29 17:20:50 +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 |  | 
			
				
					| 
							
							
								 chriseth | f7fc42d8c3 | Merge pull request #7826 from ethereum/develop Merge develop into develop_060 | 2019-11-28 13:37:19 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 240ff30878 | [SMTChecker] Do not visit the name of a modifier invocation | 2019-11-27 22:34:33 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | ddc478e3e4 | Add CallbackKind and use it for the SMT solver | 2019-11-21 22:10:21 +00:00 |  | 
			
				
					| 
							
							
								 Erik K | 94272d44aa | Merge pull request #7745 from ethereum/develop Merge develop into develop_060 | 2019-11-19 15:30:31 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | d818746e0c | [SMTChecker] Fix ICE in abi.decode | 2019-11-18 13:15:10 +01:00 |  | 
			
				
					| 
							
							
								 chriseth | 216e1749f4 | Merge remote-tracking branch 'origin/develop' into develop_060 | 2019-11-14 13:42:46 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 8efacfb545 | [SMTChecker] Fix ICE in string literal to fixed bytes implicit conversion | 2019-11-13 22:25:18 +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 | 5dacaf57bc | Fix ICE in FixedBytes IndexAccess | 2019-11-08 17:29:40 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | fc945880d1 | [SMTChecker] Fix override tests | 2019-11-07 11:49:32 +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 |  |