From cebf2d2ca7f087f22500a6c4aa247b9f2dcce1af Mon Sep 17 00:00:00 2001
From: Anton Bukov <k06aaa@gmail.com>
Date: Sun, 7 May 2023 00:12:25 +0300
Subject: [PATCH] Add tests for type(S).typehash

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

diff --git a/test/libsolidity/smtCheckerTests/types/type_typehash.sol b/test/libsolidity/smtCheckerTests/types/type_typehash.sol
new file mode 100644
index 000000000..757f795bc
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/type_typehash.sol
@@ -0,0 +1,45 @@
+interface I1 {
+}
+
+contract C {
+    struct S1 {
+        uint256 x;
+    }
+
+    struct S2 {
+        uint256 x;
+        address y;
+    }
+
+    struct S3 {
+        uint256 x;
+        I1 y;
+        S2 third;
+    }
+
+    struct S4 {
+        S3 one;
+        S2 two;
+    }
+
+    struct S5 {
+        S2 two;
+        S1 one;
+        S3 three;
+        S4[5] four;
+    }
+
+	function f() public pure {
+		assert(type(S1).typehash == keccak256(bytes("S1(uint256 x)")));
+		assert(type(S2).typehash == keccak256(bytes("S2(uint256 x,address y)")));
+		assert(type(S3).typehash == keccak256(bytes("S3(uint256 x,address y,S2 third)S2(uint256 x,address y)")));
+        assert(type(S4).typehash == keccak256(bytes("S4(S3 one,S2 two)S2(uint256 x,address y)S3(uint256 x,address y,S2 third)")));
+        assert(type(S5).typehash == keccak256(bytes("S5(S2 two,S1 one,S3 three,S4[5] four)S1(uint256 x)S2(uint256 x,address y)S3(uint256 x,address y,S2 third)S4(S3 one,S2 two)")));
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (416-468): CHC: Assertion violation happens here.
+// Warning 6328: (503-555): CHC: Assertion violation happens here.
+// Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.