| 
							
							
								 Leonardo Alt | 3c4e286390 | [SMTChecker] Replace wrap mod by slack vars | 2020-06-12 14:57:21 +02:00 |  | 
			
				
					| 
							
							
								 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 | f49e2424b2 | [SMTChecker] Erase knowledge when array variable is pushed | 2020-06-08 10:23:06 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo | d243f5baac | Merge pull request #9045 from ethereum/smt_fix_tuple [SMTChecker] Fix internal error in tuples of tuples. | 2020-06-05 14:21:32 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo | 731e6466a0 | Merge pull request #9067 from ethereum/smt_fix_fp_again [SMTChecker] Fix BMC targets with FP | 2020-06-05 12:39:28 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 87ceb72b82 | [SMTChecker] Fix internal error in tuples of tuples. | 2020-06-05 12:20:47 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 10162016ae | [SMTChecker] Fix internal error on try/catch | 2020-06-02 16:51:53 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 2128ff9f13 | Fix ICE on push for member access | 2020-05-29 19:13:27 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | e5d25692a5 | [SMTChecker] Fix BMC targets with FP | 2020-05-29 18:13:13 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | b90fb1cab6 | [SMTChecker] Fix ICE on index access assignment inside single branches | 2020-05-28 15:56:46 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | a73ec6a82f | [SMTChecker] Fix ICE in inlining function calls while short circuiting | 2020-05-28 13:14:19 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | cb1cbbc1f1 | [SMTChecker] Fix fixed point inc/dec | 2020-05-28 10:56:06 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 9e9f0c52e1 | [SMTChecker] Support to bitwise | 2020-05-27 20:59:00 +02:00 |  | 
			
				
					| 
							
							
								 chriseth | 9604174151 | Rename asCallableFunction. | 2020-05-26 11:35:12 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 7a91c9b971 | Remove Type from SolverInterface | 2020-05-20 12:55:19 +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 | 2435ab938c | Add verification target for empty pop | 2020-05-18 16:35:56 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | d4d26c02e4 | Assume that push will not overflow | 2020-05-18 16:35:56 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 82db35e563 | [SMTChecker] Support array push/pop | 2020-05-18 16:33:34 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | a0c605aa85 | [SMTChecker] Support array length | 2020-05-14 23:32:29 +02:00 |  | 
			
				
					| 
							
							
								 a3d4 | 8f68c04358 | Add unique IDs to error reporting calls | 2020-05-06 13:53:46 +02:00 |  | 
			
				
					| 
							
							
								 hrkrshnn | e2e32d372f | virtual modifiers (in Abstract contracts) allow empty bodies | 2020-04-23 17:26:59 +05:30 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 83c9e82099 | Fix ICE with fixed point | 2020-04-22 19:57:00 +02:00 |  | 
			
				
					| 
							
							
								 chriseth | 41ef13129b | Merge pull request #8678 from ethereum/smt_remove_redundant_constraints [SMTChecker] Remove redundant CHC constraints | 2020-04-20 15:44:59 +02:00 |  | 
			
				
					| 
							
							
								 hrkrshnn | 4760b8589d | Replaced all instances of lValueRequested to willBeWrittenTo | 2020-04-20 12:33:30 +05:30 |  | 
			
				
					| 
							
							
								 Leonardo Alt | bca43586c6 | [SMTChecker] Remove redundant CHC constraints | 2020-04-15 18:11:39 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 5d9dd654cf | [SMTChecker] Add and use tuple sort | 2020-04-08 18:26:03 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 05a85461fe | Symbolic state | 2020-04-06 12:27:53 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 07368c2e1e | Add support to internal function calls | 2020-03-11 16:29:07 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 96a230af50 | [SMTChecker] Fix ICEs with tuples | 2020-03-03 11:35:58 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 34d64761d9 | Extract symbolicArguments function | 2020-02-12 11:47:58 -03:00 |  | 
			
				
					| 
							
							
								 Christian Parpart | 6b23412fae | C++ namespace cleanup (except tests). | 2020-01-07 15:51:50 +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 Alt | 9eda95caf9 | [SMTChecker] Fix visit to IndexAccess that has type Type | 2019-11-29 17:20:50 +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 |  | 
			
				
					| 
							
							
								 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 |  | 
			
				
					| 
							
							
								 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 |  |