diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp
index 601891c5a..90fceab3c 100644
--- a/libsolidity/formal/PredicateInstance.cpp
+++ b/libsolidity/formal/PredicateInstance.cpp
@@ -64,7 +64,7 @@ smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const
 		return _pred(currentFunctionVariables(*constructor, &_contract, _context));
 
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state()};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state(0), state.state()};
 	return _pred(stateExprs + currentStateVariables(_contract, _context));
 }
 
diff --git a/libsolidity/formal/PredicateSort.cpp b/libsolidity/formal/PredicateSort.cpp
index 5bcc5efcb..b9e1c1d40 100644
--- a/libsolidity/formal/PredicateSort.cpp
+++ b/libsolidity/formal/PredicateSort.cpp
@@ -60,7 +60,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
 		return functionSort(*constructor, &_contract, _state);
 
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()} + stateSorts(_contract),
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract),
 		SortProvider::boolSort
 	);
 }