| 
							
							
								 Leo Alt | 21c0f78650 | Report safe properties in BMC and CHC | 2023-03-09 14:59:32 +01:00 |  | 
			
				
					| 
							
							
								 Rodrigo Q. Saramago | feba4de509 | Add paris constraints to SMTChecker Co-authored-by: Daniel <daniel@ekpyron.org>
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
Co-authored-by: Leo <leo@ethereum.org> | 2023-01-31 11:03:04 +01:00 |  | 
			
				
					| 
							
							
								 Leo Alt | 77698f8108 | Fix internal error when deleting struct member of function type | 2022-11-30 12:47:32 +01:00 |  | 
			
				
					| 
							
							
								 Leo Alt | d660f0cab0 | adjust nondeterministic tests | 2022-11-24 13:08:06 +01:00 |  | 
			
				
					| 
							
							
								 Leo Alt | 504b70b6af | update smt tests | 2022-11-24 13:08:06 +01:00 |  | 
			
				
					| 
							
							
								 Leo Alt | 16c0838f75 | Update docker images and tests | 2022-08-30 11:51:59 +02:00 |  | 
			
				
					| 
							
							
								 Leo Alt | cba3d18f66 | adjust for osx nondeterminism | 2022-05-04 19:04:54 +02:00 |  | 
			
				
					| 
							
							
								 Leo Alt | f9fa76c9d3 | smt encode call | 2022-04-11 12:19:41 +02:00 |  | 
			
				
					| 
							
							
								 Marenz | 7a96953e78 | Implement typechecked abi.encodeCall() | 2021-12-16 17:35:58 +01:00 |  | 
			
				
					| 
							
							
								 Leo Alt | ff5c842d67 | update smtchecker tests | 2021-11-24 20:41:22 +01:00 |  | 
			
				
					| 
							
							
								 Leo Alt | 6e2fe1e340 | [SMTChecker] Cleanup spurious messages about TypeTypes | 2021-09-07 16:55:25 +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 | 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 |  | 
			
				
					| 
							
							
								 Alex Beregszaszi | 84c05d35f3 | Trivial isoltest updates: normalized whitespace | 2021-04-20 17:38:29 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 0a4afa71bd | Update old tests | 2021-04-08 21:03:39 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | ba97d6ac4e | Add local vars to cex | 2021-03-30 17:55:21 +02:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | dbd067d6db | Report out of bounds index access | 2021-03-30 10:28:48 +02:00 |  | 
			
				
					| 
							
							
								 Martin Blicha | 5293f05ee3 | [SMTChecker] Fix ICE on ABI functions with no arguments | 2021-03-25 13:28:29 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 6fd76e830d | Fix CHC cex order | 2021-03-11 10:36:40 +01:00 |  | 
			
				
					| 
							
							
								 Martin Blicha | 5af01f6896 | [SMTChecker] Use same sort name for array slice as for the underlying array. | 2021-03-09 11:06:22 +01:00 |  | 
			
				
					| 
							
							
								 Martin Blicha | a49950cdf3 | [SMTChecker] Added transaction constraints also for contract deployment | 2021-02-01 16:46:34 +01:00 |  | 
			
				
					| 
							
							
								 Martin Blicha | deb90d84a6 | [SMTChecker] added missing type constraints for Address | 2021-01-27 20:39:24 +01:00 |  | 
			
				
					| 
							
							
								 Martin Blicha | 2ee0f347b9 | [SMTChecker] additional regression tests | 2021-01-14 14:54:14 +01:00 |  | 
			
				
					| 
							
							
								 Martin Blicha | be0a0f4d90 | [SMTChecker] Added constraints for block properties | 2020-12-29 22:17:44 +01:00 |  | 
			
				
					| 
							
							
								 Martin Blicha | 77dff222e9 | disabling some tests because of nondeterminism in Spacer | 2020-12-28 16:24:44 +01:00 |  | 
			
				
					| 
							
							
								 Martin Blicha | 745466b71f | updates to the tests | 2020-12-28 14:32:53 +01:00 |  | 
			
				
					| 
							
							
								 Leonardo Alt | 50be39fc21 | Add and update tests | 2020-12-17 14:42:49 +01:00 |  |