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;
+}