diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp
index 525c90f55..220fde77e 100644
--- a/libsolidity/formal/EncodingContext.cpp
+++ b/libsolidity/formal/EncodingContext.cpp
@@ -38,8 +38,8 @@ void EncodingContext::reset()
 	resetAllVariables();
 	m_expressions.clear();
 	m_globalContext.clear();
-	m_thisAddress->increaseIndex();
-	m_balances->increaseIndex();
+	m_thisAddress->resetIndex();
+	m_balances->resetIndex();
 	m_assertions.clear();
 }
 
diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index d7625ed9d..907e62f64 100644
--- a/libsolidity/formal/SymbolicVariables.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -78,6 +78,12 @@ string SymbolicVariable::uniqueSymbol(unsigned _index) const
 	return m_uniqueName + "_" + to_string(_index);
 }
 
+Expression SymbolicVariable::resetIndex()
+{
+	m_ssa->resetIndex();
+	return currentValue();
+}
+
 Expression SymbolicVariable::increaseIndex()
 {
 	++(*m_ssa);
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index 7d65a1aa3..e6ebb8127 100644
--- a/libsolidity/formal/SymbolicVariables.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -55,6 +55,7 @@ public:
 	std::string currentName() const;
 	virtual Expression valueAtIndex(int _index) const;
 	virtual std::string nameAtIndex(int _index) const;
+	virtual Expression resetIndex();
 	virtual Expression increaseIndex();
 	virtual Expression operator()(std::vector<Expression> /*_arguments*/) const
 	{
diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json
index 06a8f0be4..b848f6338 100644
--- a/test/libsolidity/smtCheckerTestsJSON/multi.json
+++ b/test/libsolidity/smtCheckerTestsJSON/multi.json
@@ -3,9 +3,9 @@
 	{
 		"smtlib2responses":
 		{
-			"0x0e5da3eca3d435940329103801b225604b2117438acea19504f980c5c1aaa571": "sat\n((|EVALEXPR_0| 0))\n",
-			"0xb83649564ec7bcc0c986c9c9c9d3fc28d90ad276ed2a6605fd48d10d30bef5e6": "sat\n((|EVALEXPR_0| 1))\n",
-			"0xeb8a2252226643551271abef0bc6c5c68b3a12fa509ad78a687c2cf76ddb4148": "unsat\n"
+			"0x047d0c67d7e03c5ac96ca227d1e19ba63257f4ab19cef30029413219ec8963af": "sat\n((|EVALEXPR_0| 0))\n",
+			"0x21d5b49d1416d788fe34b1d2a10a99ea92b007e17a977604afd7b2ff01a055cd": "unsat\n",
+			"0xada7569fb01a9b3e2823517ed40dcc99b11fb1e433e6e3ec8a8713f6f95753d3": "sat\n((|EVALEXPR_0| 1))\n"
 		}
 	}
 }
diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json
index 9a362fd55..2f7ebdffb 100644
--- a/test/libsolidity/smtCheckerTestsJSON/simple.json
+++ b/test/libsolidity/smtCheckerTestsJSON/simple.json
@@ -3,7 +3,7 @@
 	{
 		"smtlib2responses":
 		{
-			"0x9804531ddd39e0d6df2dcb24d8dfd9e7b8c7ed3ece5d33f1680063d3e02f18f0": "sat\n((|EVALEXPR_0| 0))\n"
+			"0x2e32517a1410b1a16decd448bb9bac7789d7cf1c6f98703ed6bacfcad6abebfb": "sat\n((|EVALEXPR_0| 0))\n"
 		}
 	}
 }