From 92059fa84848ce7f78d93a8af720bef034b74fde Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Thu, 23 Apr 2020 10:40:57 +0200
Subject: [PATCH] Use Spacer option to improve performance of constant arrays

---
 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, 23 insertions(+), 9 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/types/unused_mapping.sol

diff --git a/libsolidity/formal/Z3CHCInterface.cpp b/libsolidity/formal/Z3CHCInterface.cpp
index c64da2edc..dcfd19c86 100644
--- a/libsolidity/formal/Z3CHCInterface.cpp
+++ b/libsolidity/formal/Z3CHCInterface.cpp
@@ -43,6 +43,8 @@ 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 5d3292992..7cb7b22b1 100644
--- a/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol
+++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol
@@ -22,4 +22,3 @@ 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 0b301505b..d7d88424a 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,12 +12,10 @@ 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: (316-336): Assertion violation happens here
-// Warning: (363-382): Assertion violation happens here
+// Warning: (312-331): 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 333273781..a90053024 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,6 +19,5 @@ 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 92d1ded3e..7670ddb6d 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,13 +14,11 @@ 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: (296-316): Assertion violation happens here
-// Warning: (320-339): Assertion violation happens here
-// Warning: (343-362): Assertion violation happens here
+// Warning: (290-309): Assertion violation happens here
+// Warning: (313-332): 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 8a1ba5e6e..cb5a0799f 100644
--- a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol
+++ b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol
@@ -16,4 +16,5 @@ 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
new file mode 100644
index 000000000..f12cd41de
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/unused_mapping.sol
@@ -0,0 +1,17 @@
+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);
+	}
+}