From 84c707cd2ac70b0a4c790cb746392d9692c79231 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Thu, 10 Sep 2020 18:52:03 +0200
Subject: [PATCH] Adjust problematic SMTChecker tests

---
 ...rray_struct_array_struct_memory_unsafe.sol |  3 --
 ...uct_array_struct_array_memory_unsafe_1.sol |  3 --
 ...uct_array_struct_array_memory_unsafe_2.sol | 34 -------------------
 ...ct_array_struct_array_storage_unsafe_1.sol |  3 --
 4 files changed, 43 deletions(-)
 delete mode 100644 test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol

diff --git a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol
index 04b8a5620..8bddba34b 100644
--- a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol
@@ -22,8 +22,6 @@ contract C {
 		assert(s1[2].a[2] == s2.a[2]);
 		s1[0].ts[3].y = 5;
 		assert(s1[0].ts[3].y == s2.ts[3].y);
-		s1[1].ts[4].a[5] = 6;
-		assert(s1[1].ts[4].a[5] == s2.ts[4].a[5]);
 	}
 }
 // ----
@@ -31,5 +29,4 @@ contract C {
 // Warning 6328: (301-328): Assertion violation happens here.
 // Warning 6328: (350-379): Assertion violation happens here.
 // Warning 6328: (404-439): Assertion violation happens here.
-// Warning 6328: (467-508): Assertion violation happens here.
 // Warning 4588: (228-238): Assertion checker does not yet implement this type of function call.
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol
index 2ff9bfd14..a621c9b0e 100644
--- a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol
@@ -22,8 +22,6 @@ contract C {
 		assert(s1.a[2] != 4);
 		s1.ts[3].y = 5;
 		assert(s1.ts[3].y != 5);
-		s1.ts[4].a[5] = 6;
-		assert(s1.ts[4].a[5] != 6);
 	}
 }
 // ----
@@ -31,4 +29,3 @@ contract C {
 // Warning 6328: (263-282): Assertion violation happens here.
 // Warning 6328: (301-321): Assertion violation happens here.
 // Warning 6328: (343-366): Assertion violation happens here.
-// Warning 6328: (391-417): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol
deleted file mode 100644
index 25dfd0f41..000000000
--- a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol
+++ /dev/null
@@ -1,34 +0,0 @@
-pragma experimental SMTChecker;
-pragma experimental ABIEncoderV2;
-
-contract C {
-	struct T {
-		uint y;
-		uint[] a;
-	}
-	struct S {
-		uint x;
-		T t;
-		uint[] a;
-		T[] ts;
-	}
-	function f(S memory s2) public pure {
-		S memory s1;
-		s1.x = 2;
-		assert(s1.x == s2.x);
-		s1.t.y = 3;
-		assert(s1.t.y == s2.t.y);
-		s1.a[2] = 4;
-		assert(s1.a[2] == s2.a[2]);
-		s1.ts[3].y = 5;
-		assert(s1.ts[3].y == s2.ts[3].y);
-		s1.ts[4].a[5] = 6;
-		assert(s1.ts[4].a[5] == s2.ts[4].a[5]);
-	}
-}
-// ----
-// Warning 6328: (239-259): Assertion violation happens here.
-// Warning 6328: (277-301): Assertion violation happens here.
-// Warning 6328: (320-346): Assertion violation happens here.
-// Warning 6328: (368-400): Assertion violation happens here.
-// Warning 6328: (425-463): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol
index 0d0466828..e4890debd 100644
--- a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol
@@ -21,8 +21,6 @@ contract C {
 		assert(s1.a[2] != 4);
 		s1.ts[3].y = 5;
 		assert(s1.ts[3].y != 5);
-		s1.ts[4].a[5] = 6;
-		assert(s1.ts[4].a[5] != 6);
 	}
 }
 // ----
@@ -30,4 +28,3 @@ contract C {
 // Warning 6328: (216-235): Assertion violation happens here.
 // Warning 6328: (254-274): Assertion violation happens here.
 // Warning 6328: (296-319): Assertion violation happens here.
-// Warning 6328: (344-370): Assertion violation happens here.