From a6db37ac9c0f84253d88b8a41fcf6b12860ef325 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Tue, 30 Apr 2019 18:22:54 +0200
Subject: [PATCH] [SMTChecker] Fix bad cast in base constructor modifier.

---
 Changelog.md                                           |  1 +
 libsolidity/formal/SMTChecker.cpp                      |  9 +++++++--
 .../functions/constructor_hierarchy.sol                |  6 ++++++
 .../functions/constructor_hierarchy_2.sol              | 10 ++++++++++
 4 files changed, 24 insertions(+), 2 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol
 create mode 100644 test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol

diff --git a/Changelog.md b/Changelog.md
index 801a4f2a0..32a3a3c95 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -7,6 +7,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix bad cast in base constructor modifier.
 
 
 
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index e54c64c3f..5c062edb2 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -101,13 +101,18 @@ bool SMTChecker::visit(ModifierDefinition const&)
 
 bool SMTChecker::visit(FunctionDefinition const& _function)
 {
+	m_functionPath.push_back(&_function);
+	m_modifierDepthStack.push_back(-1);
+
 	if (_function.isConstructor())
+	{
 		m_errorReporter.warning(
 			_function.location(),
 			"Assertion checker does not yet support constructors."
 		);
-	m_functionPath.push_back(&_function);
-	m_modifierDepthStack.push_back(-1);
+		return false;
+	}
+
 	// Not visited by a function call
 	if (isRootFunction())
 	{
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol
new file mode 100644
index 000000000..ebc674edf
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol
@@ -0,0 +1,6 @@
+pragma experimental SMTChecker;
+contract C { constructor(uint) public {} }
+contract A is C { constructor() C(2) public {} }
+// ----
+// Warning: (45-72): Assertion checker does not yet support constructors.
+// Warning: (93-121): Assertion checker does not yet support constructors.
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol
new file mode 100644
index 000000000..0b96c566c
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+contract C { constructor(uint) public {} }
+contract A is C { constructor() C(2) public {} }
+contract B is C { constructor() C(3) public {} }
+contract J is C { constructor() C(3) public {} }
+// ----
+// Warning: (45-72): Assertion checker does not yet support constructors.
+// Warning: (93-121): Assertion checker does not yet support constructors.
+// Warning: (142-170): Assertion checker does not yet support constructors.
+// Warning: (191-219): Assertion checker does not yet support constructors.