diff --git a/Changelog.md b/Changelog.md
index 9006ac777..992436ea3 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -25,6 +25,7 @@ Bugfixes:
  * Scanner: Fix bug when two empty NatSpec comments lead to scanning past EOL.
  * Code Generator: Trigger proper unimplemented errors on certain array copy operations.
  * SMTChecker: Fix internal error when applying arithmetic operators to fixed point variables.
+ * SMTChecker: Fix internal error when short circuiting Boolean expressions with function calls in state variable initialization.
 
 ### 0.6.8 (2020-05-14)
 
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index fd1acb66f..be9bea10f 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1791,7 +1791,6 @@ Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
 
 set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _node)
 {
-	solAssert(!m_callStack.empty(), "");
 	vector<CallableDeclaration const*> callStack;
 	for (auto const& call: m_callStack)
 		callStack.push_back(call.first);
diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp
index 1871c0908..acfd34909 100644
--- a/libsolidity/formal/VariableUsage.cpp
+++ b/libsolidity/formal/VariableUsage.cpp
@@ -33,7 +33,8 @@ set<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _
 	m_touchedVariables.clear();
 	m_callStack.clear();
 	m_callStack += _outerCallstack;
-	m_lastCall = m_callStack.back();
+	if (!m_callStack.empty())
+		m_lastCall = m_callStack.back();
 	_node.accept(*this);
 	return m_touchedVariables;
 }