diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index 279ed8e74..5e3f6c7ff 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -49,6 +49,8 @@ void BMC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner
 
 	m_scanner = _scanner;
 
+	m_context.clear();
+
 	_source.accept(*this);
 
 	solAssert(m_interface->solvers() > 0, "");
diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp
index 5170773a6..da04a7463 100644
--- a/libsolidity/formal/EncodingContext.cpp
+++ b/libsolidity/formal/EncodingContext.cpp
@@ -44,6 +44,12 @@ void EncodingContext::reset()
 	m_assertions.clear();
 }
 
+void EncodingContext::clear()
+{
+	m_variables.clear();
+	reset();
+}
+
 /// Variables.
 
 shared_ptr<SymbolicVariable> EncodingContext::variable(solidity::VariableDeclaration const& _varDecl)
diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h
index 3bce9b6e4..2a4fa9442 100644
--- a/libsolidity/formal/EncodingContext.h
+++ b/libsolidity/formal/EncodingContext.h
@@ -38,8 +38,13 @@ class EncodingContext
 public:
 	EncodingContext(std::shared_ptr<SolverInterface> _solver);
 
-	/// Resets the entire context.
+	/// Resets the entire context except for symbolic variables which stay
+	/// alive because of state variables and inlined function calls.
+	/// To be used in the beginning of a root function visit.
 	void reset();
+	/// Clears the entire context, erasing everything.
+	/// To be used before a model checking engine starts.
+	void clear();
 
 	/// Forwards variable creation to the solver.
 	Expression newVariable(std::string _name, SortPointer _sort)
diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json
index 6d85039e5..780a15a2d 100644
--- a/test/libsolidity/smtCheckerTestsJSON/multi.json
+++ b/test/libsolidity/smtCheckerTestsJSON/multi.json
@@ -3,9 +3,9 @@
 	{
 		"smtlib2responses":
 		{
-			"0x68fa399769cf119cbe46d5ae578164d39ea67e06eee08eeb37042d08a13a0cd8": "unsat\n",
-			"0xd78cd71ff120c5b5ecc5020146952f62de0506c4baef7ba499239a2ce2b14343": "sat\n((|EVALEXPR_0| 0))\n",
-			"0xf74672131cc6b7b3d6b82ed2fa0da2b75d01c9bc32f15d2f77e8e39e174f5a37": "sat\n((|EVALEXPR_0| 1))\n"
+			"0x6e5cf865938b82f1627009d26ecb4c59e9b8c05cc1024ccf548b9b94c1c73e56": "unsat\n",
+			"0x890d45bd5b96d51c4d11683bcf3b7547cea993b3e15961c216a0a782d5d3ccb2": "sat\n((|EVALEXPR_0| 0))\n",
+			"0xa649be28767cedec4a7b7f5591e3fb237447405a823dbd861869eb35d91bebce": "sat\n((|EVALEXPR_0| 1))\n"
 		}
 	}
 }
diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json
index f390e4840..4f0cafbac 100644
--- a/test/libsolidity/smtCheckerTestsJSON/simple.json
+++ b/test/libsolidity/smtCheckerTestsJSON/simple.json
@@ -3,7 +3,7 @@
 	{
 		"smtlib2responses":
 		{
-			"0x9e377366ae857502a72974bd4e563258a29fa84dd4358cc053057544409da0ea": "sat\n((|EVALEXPR_0| 0))\n"
+			"0xcae00c08b91a968103a89431c473645366101a2b037d72aa10fbe3099ccd6931": "sat\n((|EVALEXPR_0| 0))\n"
 		}
 	}
 }