diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index f3831b40f..8b50600ad 100644
--- a/libsolidity/formal/Why3Translator.cpp
+++ b/libsolidity/formal/Why3Translator.cpp
@@ -757,6 +757,11 @@ bool Why3Translator::visit(Literal const& _literal)
 	return false;
 }
 
+bool Why3Translator::visit(PragmaDirective const&)
+{
+	return false;
+}
+
 bool Why3Translator::isStateVariable(VariableDeclaration const* _var) const
 {
 	return contains(m_currentContract.stateVariables, _var);
diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h
index 22bfff895..4fdac3851 100644
--- a/libsolidity/formal/Why3Translator.h
+++ b/libsolidity/formal/Why3Translator.h
@@ -94,6 +94,7 @@ private:
 	virtual bool visit(IndexAccess const& _node) override;
 	virtual bool visit(Identifier const& _node) override;
 	virtual bool visit(Literal const& _node) override;
+	virtual bool visit(PragmaDirective const& _node) override;
 
 	virtual bool visitNode(ASTNode const& _node) override
 	{