From 240ff30878ededff0537407353538b307675f93d Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Wed, 27 Nov 2019 22:34:33 +0100
Subject: [PATCH] [SMTChecker] Do not visit the name of a modifier invocation

---
 libsolidity/formal/SMTEncoder.cpp               | 13 ++++++++++---
 libsolidity/formal/SMTEncoder.h                 |  1 +
 .../functions/constructor_base_basic.sol        | 17 +++++++++++++++++
 3 files changed, 28 insertions(+), 3 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/functions/constructor_base_basic.sol

diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 5fd364f8bc8b..b31ff37d26f1 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -537,6 +537,15 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	}
 }
 
+bool SMTEncoder::visit(ModifierInvocation const& _node)
+{
+	if (auto const* args = _node.arguments())
+		for (auto const& arg: *args)
+			if (arg)
+				arg->accept(*this);
+	return false;
+}
+
 void SMTEncoder::initContract(ContractDefinition const& _contract)
 {
 	solAssert(m_currentContract == nullptr, "");
@@ -605,9 +614,7 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
 		defineExpr(_identifier, m_context.thisAddress());
 		m_uninterpretedTerms.insert(&_identifier);
 	}
-	else if (
-		_identifier.annotation().type->category() != Type::Category::Modifier
-	)
+	else
 		createExpr(_identifier);
 }
 
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 4f8c5ac8c837..a81092f84988 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -82,6 +82,7 @@ class SMTEncoder: public ASTConstVisitor
 	bool visit(BinaryOperation const& _node) override;
 	void endVisit(BinaryOperation const& _node) override;
 	void endVisit(FunctionCall const& _node) override;
+	bool visit(ModifierInvocation const& _node) override;
 	void endVisit(Identifier const& _node) override;
 	void endVisit(ElementaryTypeNameExpression const& _node) override;
 	void endVisit(Literal const& _node) override;
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_base_basic.sol b/test/libsolidity/smtCheckerTests/functions/constructor_base_basic.sol
new file mode 100644
index 000000000000..8e5c57cf6e15
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_base_basic.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	constructor() public {
+		x = 2;
+	}
+}
+
+contract B is A {
+	constructor() A() public {
+		x = 3;
+	}
+}
+// ----
+// Warning: (56-90): Assertion checker does not yet support constructors.
+// Warning: (113-151): Assertion checker does not yet support constructors.