| 
							
							
								 Leonardo Alt | 3bee348525 | Change CHC encoding to functions forest instead of explicit CFG | 2020-03-03 12:12:26 +01:00 |  | 
			
				
					| 
							
							
								 Christian Parpart | 6b23412fae | C++ namespace cleanup (except tests). | 2020-01-07 15:51:50 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 67d82fc8a7 | [SMTChecker] Use rlimit instead of tlimit for SMT queries | 2019-12-04 11:52:18 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 6b10efff8c | Add CHCSmtLib2Interface | 2019-11-07 11:12:11 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 71144d0d39 | [CHCChecker] Add CHCSolverInterface and Z3CHCSolverInterface | 2019-07-15 17:31:39 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | cce377833a | Sort includes in libsolidity/formal | 2018-12-17 18:26:10 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 13a142b039 | [SMTChecker] Add FunctionSort and refactors the solver interface to create variables | 2018-11-22 10:04:04 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 01ce43e51b | [SMTChecker] Refactor smt::Sort and its usage | 2018-11-21 15:46:47 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 70bb0eaf95 | [SMTChecker] Implement uninterpreted functions and use it for blockhash() | 2018-11-15 09:12:42 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 87a38e1abe | [SMTChecker] SMTPortfolio: use all SMT solvers available | 2018-07-27 16:15:34 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | ae3350ae03 | [SMTChecker] Integration with CVC4 | 2018-04-17 12:26:58 +01:00 |  | 
			
				
					| 
							
							
								 chriseth | ab5e3a8f6d | Introduce native Z3 support. | 2017-08-23 17:37:35 +02:00 |  |