diff --git a/Changelog.md b/Changelog.md
index 226e8e78de12..3af5e5301598 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -11,6 +11,7 @@ Compiler Features:
 Bugfixes:
  * AST Import: For constructors, a public visibility is ignored during importing.
  * Error Reporter: Fix handling of carriage return.
+ * SMTChecker: Fix internal error in BMC on resolving virtual functions inside branches.
  * SMTChecker: Fix internal error on ``array.pop`` nested inside 1-tuple.
  * SMTChecker: Fix internal error on ``FixedBytes`` constant initialized with string literal.
  * SMTChecker: Fix internal error on array slices.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 3398e308f762..96c937d352e2 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -782,7 +782,6 @@ void SMTEncoder::initFunction(FunctionDefinition const& _function)
 	createLocalVariables(_function);
 	m_arrayAssignmentHappened = false;
 	clearIndices(m_currentContract, &_function);
-	m_variableUsage.setCurrentFunction(_function);
 	m_checked = true;
 }
 
diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp
index b96c40b791f4..9ae4120c8086 100644
--- a/libsolidity/formal/VariableUsage.cpp
+++ b/libsolidity/formal/VariableUsage.cpp
@@ -21,6 +21,8 @@
 #include <libsolidity/formal/BMC.h>
 #include <libsolidity/formal/SMTEncoder.h>
 
+#include <range/v3/view.hpp>
+
 #include <algorithm>
 
 using namespace std;
@@ -60,7 +62,7 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess)
 
 void VariableUsage::endVisit(FunctionCall const& _funCall)
 {
-	auto scopeContract = m_currentFunction->annotation().contract;
+	auto scopeContract = currentScopeContract();
 	if (m_inlineFunctionCalls(_funCall, scopeContract, m_currentContract))
 		if (auto funDef = SMTEncoder::functionCallToDefinition(_funCall, scopeContract, m_currentContract))
 			if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end())
@@ -107,3 +109,11 @@ void VariableUsage::checkIdentifier(Identifier const& _identifier)
 			m_touchedVariables.insert(varDecl);
 	}
 }
+
+ContractDefinition const* VariableUsage::currentScopeContract()
+{
+	for (auto&& f: m_callStack | ranges::views::reverse)
+		if (auto fun = dynamic_cast<FunctionDefinition const*>(f))
+			return fun->annotation().contract;
+	return nullptr;
+}
diff --git a/libsolidity/formal/VariableUsage.h b/libsolidity/formal/VariableUsage.h
index 722f98660f6e..4dc90f8c07a7 100644
--- a/libsolidity/formal/VariableUsage.h
+++ b/libsolidity/formal/VariableUsage.h
@@ -39,7 +39,6 @@ class VariableUsage: private ASTConstVisitor
 	void setFunctionInlining(std::function<bool(FunctionCall const&, ContractDefinition const*, ContractDefinition const*)> _inlineFunctionCalls) { m_inlineFunctionCalls = _inlineFunctionCalls; }
 
 	void setCurrentContract(ContractDefinition const& _contract) { m_currentContract = &_contract; }
-	void setCurrentFunction(FunctionDefinition const& _function) { m_currentFunction = &_function; }
 
 private:
 	void endVisit(Identifier const& _node) override;
@@ -53,11 +52,12 @@ class VariableUsage: private ASTConstVisitor
 	/// Checks whether an identifier should be added to touchedVariables.
 	void checkIdentifier(Identifier const& _identifier);
 
+	ContractDefinition const* currentScopeContract();
+
 	std::set<VariableDeclaration const*> m_touchedVariables;
 	std::vector<CallableDeclaration const*> m_callStack;
 	CallableDeclaration const* m_lastCall = nullptr;
 	ContractDefinition const* m_currentContract = nullptr;
-	FunctionDefinition const* m_currentFunction = nullptr;
 
 	std::function<bool(FunctionCall const&, ContractDefinition const*, ContractDefinition const*)> m_inlineFunctionCalls = [](FunctionCall const&, ContractDefinition const*, ContractDefinition const*) { return false; };
 };
diff --git a/test/libsolidity/smtCheckerTests/control_flow/virtual_function_call_inside_branch_1.sol b/test/libsolidity/smtCheckerTests/control_flow/virtual_function_call_inside_branch_1.sol
new file mode 100644
index 000000000000..1732f1b131fb
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/control_flow/virtual_function_call_inside_branch_1.sol
@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract Context {}
+
+contract ERC20 is Context {
+    function approve() public virtual { _approve(); }
+    function _approve() internal virtual {}
+}
+
+contract __unstable__ERC20Owned is ERC20 {
+    function _approve() internal override {
+        if (true) {
+            super._approve();
+        }
+    }
+}
diff --git a/test/libsolidity/smtCheckerTests/control_flow/virtual_function_call_inside_branch_2.sol b/test/libsolidity/smtCheckerTests/control_flow/virtual_function_call_inside_branch_2.sol
new file mode 100644
index 000000000000..c11521a15480
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/control_flow/virtual_function_call_inside_branch_2.sol
@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+contract A {
+    function f() internal virtual {
+        v();
+    }
+    function v() internal virtual {
+    }
+}
+
+contract B is A {
+    function f() internal virtual override {
+        super.f();
+    }
+}
+
+contract C is B {
+    function v() internal override {
+        if (0==1)
+            f();
+    }
+}
+// ----
+// Warning 6838: (303-307): BMC: Condition is always false.