diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index ee11d34d5..b288bee6a 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -207,12 +207,8 @@ void SMTEncoder::visitFunctionOrModifier()
 		auto refDecl = modifierInvocation->name().annotation().referencedDeclaration;
 		if (dynamic_cast<ContractDefinition const*>(refDecl))
 			visitFunctionOrModifier();
-		else if (auto modifierDef = dynamic_cast<ModifierDefinition const*>(refDecl))
-		{
-			solAssert(*modifierInvocation->name().annotation().requiredLookup == VirtualLookup::Virtual, "");
-			ModifierDefinition const& modifier = modifierDef->resolveVirtual(*m_currentContract);
-			inlineModifierInvocation(modifierInvocation.get(), &modifier);
-		}
+		else if (auto modifier = resolveModifierInvocation(*modifierInvocation, m_currentContract))
+			inlineModifierInvocation(modifierInvocation.get(), modifier);
 		else
 			solAssert(false, "");
 	}
@@ -2681,23 +2677,34 @@ vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefini
 	{
 		if (!invok)
 			continue;
-		auto decl = invok->name().annotation().referencedDeclaration;
-		auto const* modifier = dynamic_cast<ModifierDefinition const*>(decl);
+		auto const* modifier = resolveModifierInvocation(*invok, _contract);
 		if (!modifier || visited.count(modifier))
 			continue;
 
 		visited.insert(modifier);
-		solAssert(_contract, "No contract context provided for modifier analysis!");
-		auto const& actualModifier = modifier->resolveVirtual(*_contract);
-		if (actualModifier.isImplemented())
+		if (modifier->isImplemented())
 		{
-			vars += applyMap(actualModifier.parameters(), [](auto _var) { return _var.get(); });
-			vars += BlockVars(actualModifier.body()).vars;
+			vars += applyMap(modifier->parameters(), [](auto _var) { return _var.get(); });
+			vars += BlockVars(modifier->body()).vars;
 		}
 	}
 	return vars;
 }
 
+ModifierDefinition const* SMTEncoder::resolveModifierInvocation(ModifierInvocation const& _invocation, ContractDefinition const* _contract)
+{
+	auto const* modifier = dynamic_cast<ModifierDefinition const*>(_invocation.name().annotation().referencedDeclaration);
+	if (modifier)
+	{
+		VirtualLookup lookup = *_invocation.name().annotation().requiredLookup;
+		solAssert(lookup == VirtualLookup::Virtual || lookup == VirtualLookup::Static, "");
+		solAssert(_contract || lookup == VirtualLookup::Static, "No contract context provided for modifier lookup resolution!");
+		if (lookup == VirtualLookup::Virtual)
+			modifier = &modifier->resolveVirtual(*_contract);
+	}
+	return modifier;
+}
+
 SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable)
 {
 	for (auto const* s = &_scopable; s; s = dynamic_cast<Scopable const*>(s->scope()))
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 2e7fe3360..7a1966d0c 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -77,6 +77,9 @@ public:
 	static std::vector<VariableDeclaration const*> localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract);
 	static std::vector<VariableDeclaration const*> modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract);
 
+	/// @returns the ModifierDefinition of a ModifierInvocation if possible, or nullptr.
+	static ModifierDefinition const* resolveModifierInvocation(ModifierInvocation const& _invocation, ContractDefinition const* _contract);
+
 	/// @returns the SourceUnit that contains _scopable.
 	static SourceUnit const* sourceUnitContaining(Scopable const& _scopable);
 
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_1.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_1.sol
new file mode 100644
index 000000000..07c353ee9
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_1.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+contract A {
+    modifier m virtual {
+      _;
+    }
+}
+contract C is A {
+    function f() public A.m returns (uint) {
+    }
+}
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_2.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_2.sol
new file mode 100644
index 000000000..b103d9eb9
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_2.sol
@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+contract A {
+	int x = 0;
+
+	modifier m virtual {
+		assert(x == 0); // should hold
+		assert(x == 42); // should fail
+		_;
+	}
+}
+contract C is A {
+
+	modifier m override {
+		assert(x == 1); // This assert is not reachable, should NOT be reported
+		_;
+	}
+
+	function f() public A.m returns (uint) {
+	}
+}
+// ----
+// Warning 6328: (115-130): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n = 0\n\nTransaction trace:\nconstructor()\nState: x = 0\nf()