| 
							
							
								 Leonardo Alt | f249f9c86f | [SMTLib2] Fix repeated declarations | 2018-07-27 17:34:44 +01:00 |  | 
			
				
					| 
							
							
								 Alex Beregszaszi | dea0567e06 | Fix unterminated parentheses typo in SMTLib2 Found by @leonardoalt | 2018-07-27 17:33:53 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 87a38e1abe | [SMTChecker] SMTPortfolio: use all SMT solvers available | 2018-07-27 16:15:34 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 06dbcb3afe | Only ask for a model if it's SAT | 2018-07-27 14:13:22 +02:00 |  | 
			
				
					| 
							
							
								 chriseth | 762d591a47 | Introduce sorts for smt expressions. | 2017-11-22 15:20:26 +01:00 |  | 
			
				
					| 
							
							
								 Alex Beregszaszi | 18ae0c3d78 | SMT enforce variable types | 2017-10-05 12:29:20 +01:00 |  | 
			
				
					| 
							
							
								 chriseth | cf5e1d6120 | Review changes. | 2017-08-23 17:37:35 +02:00 |  | 
			
				
					| 
							
							
								 chriseth | 1e05ebe50e | Refactor Z3 read callback. | 2017-08-23 17:37:35 +02:00 |  | 
			
				
					| 
							
							
								 chriseth | 9ac2ac14c1 | Rename read file callback. | 2017-08-23 17:37:35 +02:00 |  | 
			
				
					| 
							
							
								 chriseth | 4cea3d4aa4 | Insert abstraction layer. | 2017-08-23 17:37:35 +02:00 |  | 
			
				
					| 
							
							
								 chriseth | b3f8ed457a | Cleanup. | 2017-08-23 14:24:30 +02:00 |  | 
			
				
					| 
							
							
								 chriseth | 39fc798999 | Use file to communicate with z3. | 2017-08-23 14:24:05 +02:00 |  | 
			
				
					| 
							
							
								 chriseth | df848859da | Rewrite using SMTLIB2 interface. | 2017-08-23 14:24:05 +02:00 |  |