Martin Blicha 
							
						 
					 
					
						
						
						
						
							
						
						
							cdfc19b503 
							
						 
					 
					
						
						
							
							SMTChecker: Bring back counterexample checks in regression tests  
						
						... 
						
						
						
						Since the default is now to ignore the counterexamples when checking
test output, we bring back counterexample checks in tests where the
counterexample is (mostly) deterministic. 
						
					 
					
						2023-07-25 12:26:21 +02:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							21c0f78650 
							
						 
					 
					
						
						
							
							Report safe properties in BMC and CHC  
						
						
						
					 
					
						2023-03-09 14:59:32 +01:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							8d91ccf028 
							
						 
					 
					
						
						
							
							[SMTChecker] Add a new trusted mode which assumes that code that is  
						
						... 
						
						
						
						available at compile time is trusted. 
						
					 
					
						2023-02-06 17:02:33 +01:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							098a3cb537 
							
						 
					 
					
						
						
							
							adjust tests for nondeterminism  
						
						
						
					 
					
						2022-01-12 18:43:18 +01:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							316be7206f 
							
						 
					 
					
						
						
							
							Fix soundness of storage/memory pointers that were not erasing enough knowledge  
						
						
						
					 
					
						2021-12-14 12:02:18 +01:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							4c2b661eaa 
							
						 
					 
					
						
						
							
							[SMTChecker] Report values for block, msg and tx variables in counterexamples  
						
						
						
					 
					
						2021-10-05 15:19:10 +02:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							a1bea368cb 
							
						 
					 
					
						
						
							
							[SMTChecker] Support constants via modules  
						
						
						
					 
					
						2021-09-16 14:35:05 +02:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							60b866f9d8 
							
						 
					 
					
						
						
							
							Fix ICE on multi-source use of abi.*  
						
						
						
					 
					
						2021-08-27 18:55:36 +02:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							0cc9162fb5 
							
						 
					 
					
						
						
							
							Update SMTChecker tests  
						
						
						
					 
					
						2021-08-27 16:25:09 +02:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							a9af63187e 
							
						 
					 
					
						
						
							
							Adjust tests for nondeterminism  
						
						
						
					 
					
						2021-08-25 21:10:43 +02:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							85378b1770 
							
						 
					 
					
						
						
							
							Update existing tests  
						
						
						
					 
					
						2021-08-25 21:10:08 +02:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							9ea4576664 
							
						 
					 
					
						
						
							
							Update tests  
						
						
						
					 
					
						2021-08-19 16:34:01 +02:00 
						 
				 
			
				
					
						
							
							
								chriseth 
							
						 
					 
					
						
						
						
						
							
						
						
							c87c0f02bd 
							
						 
					 
					
						
						
							
							Test updates.  
						
						
						
					 
					
						2021-08-12 16:56:12 +02:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							10397e440c 
							
						 
					 
					
						
						
							
							Fix ICE in constants  
						
						
						
					 
					
						2021-08-12 10:53:01 +02:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							3c1f555f71 
							
						 
					 
					
						
						
							
							Tests  
						
						
						
					 
					
						2021-08-04 13:54:50 +02:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							e46abd0ca1 
							
						 
					 
					
						
						
							
							Update tests due to nondeterminism  
						
						
						
					 
					
						2021-07-19 15:20:11 +02:00 
						 
				 
			
				
					
						
							
							
								Leo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							20e23171da 
							
						 
					 
					
						
						
							
							Update tests to z3 4.8.12  
						
						
						
					 
					
						2021-07-16 14:43:52 +02:00 
						 
				 
			
				
					
						
							
							
								Alex Beregszaszi 
							
						 
					 
					
						
						
						
						
							
						
						
							1be07c2b36 
							
						 
					 
					
						
						
							
							Trivial isoltest updates: missing // ---- at the end  
						
						
						
					 
					
						2021-04-20 17:38:29 +02:00 
						 
				 
			
				
					
						
							
							
								Leonardo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							a39a6e26da 
							
						 
					 
					
						
						
							
							update tests  
						
						
						
					 
					
						2021-04-19 19:23:18 +02:00 
						 
				 
			
				
					
						
							
							
								Leonardo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							80892c8a21 
							
						 
					 
					
						
						
							
							Fix nondeterminism  
						
						
						
					 
					
						2021-04-19 19:23:18 +02:00 
						 
				 
			
				
					
						
							
							
								Leonardo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							36def3ef6e 
							
						 
					 
					
						
						
							
							tests for free constants  
						
						
						
					 
					
						2021-04-19 19:23:18 +02:00 
						 
				 
			
				
					
						
							
							
								Leonardo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							fd8b4afb76 
							
						 
					 
					
						
						
							
							new free function tests  
						
						
						
					 
					
						2021-04-19 19:23:18 +02:00 
						 
				 
			
				
					
						
							
							
								Leonardo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							095d337140 
							
						 
					 
					
						
						
							
							Basic support to free constants  
						
						
						
					 
					
						2021-04-19 19:23:18 +02:00 
						 
				 
			
				
					
						
							
							
								Leonardo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							4e34359063 
							
						 
					 
					
						
						
							
							Basic support to free functions  
						
						
						
					 
					
						2021-04-19 19:23:18 +02:00 
						 
				 
			
				
					
						
							
							
								Leonardo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							0a4afa71bd 
							
						 
					 
					
						
						
							
							Update old tests  
						
						
						
					 
					
						2021-04-08 21:03:39 +02:00 
						 
				 
			
				
					
						
							
							
								Leonardo Alt 
							
						 
					 
					
						
						
						
						
							
						
						
							a961a76263 
							
						 
					 
					
						
						
							
							Do not run SMTChecker when file level functions/constants are present.  
						
						
						
					 
					
						2020-12-09 12:18:55 +01:00