From 059d0bdebbe45edffb676b19ff49a112325e5b99 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Fri, 24 Apr 2020 11:55:58 +0200
Subject: [PATCH] Revert "Use Spacer option to improve performance of constant
 arrays"

This reverts commit 92059fa84848ce7f78d93a8af720bef034b74fde.
---
 libsolidity/formal/Z3CHCInterface.cpp           |  2 --
 .../functions/functions_recursive_indirect.sol  |  1 +
 ...for_loop_array_assignment_storage_memory.sol |  4 +++-
 ...or_loop_array_assignment_storage_storage.sol |  1 +
 ...le_loop_array_assignment_storage_storage.sol |  6 ++++--
 .../operators/delete_array_index_2d.sol         |  1 -
 .../smtCheckerTests/types/unused_mapping.sol    | 17 -----------------
 7 files changed, 9 insertions(+), 23 deletions(-)
 delete mode 100644 test/libsolidity/smtCheckerTests/types/unused_mapping.sol

diff --git a/libsolidity/formal/Z3CHCInterface.cpp b/libsolidity/formal/Z3CHCInterface.cpp
index dcfd19c86..c64da2edc 100644
--- a/libsolidity/formal/Z3CHCInterface.cpp
+++ b/libsolidity/formal/Z3CHCInterface.cpp
@@ -43,8 +43,6 @@ Z3CHCInterface::Z3CHCInterface():
 	p.set("fp.spacer.mbqi", false);
 	// Ground pobs by using values from a model.
 	p.set("fp.spacer.ground_pobs", false);
-	// Limits array reasoning, good for constant arrays.
-	p.set("fp.spacer.weak_abs", false);
 	m_solver.set(p);
 }
 
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol
index 7cb7b22b1..5d3292992 100644
--- a/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol
+++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol
@@ -22,3 +22,4 @@ contract C
 	}
 }
 // ----
+// Warning: (130-144): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol
index d7d88424a..0b301505b 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol
@@ -12,10 +12,12 @@ contract LoopFor2 {
 			b[i] = i + 1;
 			c[i] = b[i];
 		}
+		// This is safe but too hard to solve currently.
 		assert(b[0] == c[0]);
 		assert(a[0] == 900);
 		assert(b[0] == 900);
 	}
 }
 // ----
-// Warning: (312-331): Assertion violation happens here
+// Warning: (316-336): Assertion violation happens here
+// Warning: (363-382): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol
index a90053024..333273781 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol
@@ -19,5 +19,6 @@ contract LoopFor2 {
 	}
 }
 // ----
+// Warning: (317-337): Assertion violation happens here
 // Warning: (341-360): Assertion violation happens here
 // Warning: (364-383): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
index 7670ddb6d..92d1ded3e 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
@@ -14,11 +14,13 @@ contract LoopFor2 {
 			c[i] = b[i];
 			++i;
 		}
+		// Fails as false positive.
 		assert(b[0] == c[0]);
 		assert(a[0] == 900);
 		assert(b[0] == 900);
 	}
 }
 // ----
-// Warning: (290-309): Assertion violation happens here
-// Warning: (313-332): Assertion violation happens here
+// Warning: (296-316): Assertion violation happens here
+// Warning: (320-339): Assertion violation happens here
+// Warning: (343-362): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol
index cb5a0799f..8a1ba5e6e 100644
--- a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol
+++ b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol
@@ -16,5 +16,4 @@ contract C
 // ====
 // SMTSolvers: z3
 // ----
-// Warning: (174-194): Error trying to invoke SMT solver.
 // Warning: (174-194): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/unused_mapping.sol b/test/libsolidity/smtCheckerTests/types/unused_mapping.sol
deleted file mode 100644
index f12cd41de..000000000
--- a/test/libsolidity/smtCheckerTests/types/unused_mapping.sol
+++ /dev/null
@@ -1,17 +0,0 @@
-pragma experimental SMTChecker;
-
-contract C {
-	uint x;
-	uint y;
-	mapping (address => bool) public never_used;
-
-	function inc() public {
-		require(x < 10);
-		require(y < 10);
-
-		if(x == 0) x = 0; // noop state var read
-		x++;
-		y++;
-		assert(y == x);
-	}
-}