From 103fa3b7eb90c521eb91bd01e1c8f45c6be2bb33 Mon Sep 17 00:00:00 2001
From: Martin Blicha <blichm@usi.ch>
Date: Mon, 14 Dec 2020 18:23:07 +0100
Subject: [PATCH] [SMTChecker] Fix internal error on abstract modifier

---
 libsolidity/formal/SMTEncoder.cpp                          | 7 +++++--
 .../smtCheckerTests/modifiers/modifier_abstract.sol        | 6 ++++++
 2 files changed, 11 insertions(+), 2 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/modifiers/modifier_abstract.sol

diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index e39827723..b44230674 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -2604,8 +2604,11 @@ vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefini
 			continue;
 
 		visited.insert(modifier);
-		vars += applyMap(modifier->parameters(), [](auto _var) { return _var.get(); });
-		vars += BlockVars(modifier->body()).vars;
+		if (modifier->isImplemented())
+		{
+			vars += applyMap(modifier->parameters(), [](auto _var) { return _var.get(); });
+			vars += BlockVars(modifier->body()).vars;
+		}
 	}
 	return vars;
 }
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_abstract.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_abstract.sol
new file mode 100644
index 000000000..c02aa5c66
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_abstract.sol
@@ -0,0 +1,6 @@
+pragma experimental SMTChecker;
+
+abstract contract A {
+	function f() public mod {}
+	modifier mod virtual;
+}