From 0fda5fe077b6a2a42b64c75ae6a5a9217da795c7 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Sat, 23 May 2020 21:51:59 +0200
Subject: [PATCH] [SMTChecker] Add test that has an unused mapping

---
 .../smtCheckerTests/types/unused_mapping.sol    | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 test/libsolidity/smtCheckerTests/types/unused_mapping.sol

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