Merge pull request #8754 from ethereum/smt_improve_array_performance

Use Spacer option to improve performance of constant arrays

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);
 }
 

test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol

@@ -22,4 +22,3 @@ contract C
 	}
 }
 // ----
-// Warning: (130-144): Error trying to invoke SMT solver.

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

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

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

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

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);
+	}
+}