Merge remote-tracking branch 'origin/develop' into breaking

libsolidity/codegen/CompilerUtils.cpp

@@ -941,8 +941,8 @@ void CompilerUtils::convertType(
 	case Type::Category::Array:
 	{
 		solAssert(targetTypeCategory == stackTypeCategory, "");
-		ArrayType const& typeOnStack = dynamic_cast<ArrayType const&>(_typeOnStack);
-		ArrayType const& targetType = dynamic_cast<ArrayType const&>(_targetType);
+		auto const& typeOnStack = dynamic_cast<ArrayType const&>(_typeOnStack);
+		auto const& targetType = dynamic_cast<ArrayType const&>(_targetType);
 		switch (targetType.location())
 		{
 		case DataLocation::Storage:
@@ -958,65 +958,77 @@ void CompilerUtils::convertType(
 			// Copy the array to a free position in memory, unless it is already in memory.
 			if (typeOnStack.location() != DataLocation::Memory)
 			{
-				// stack: <source ref> (variably sized)
-				unsigned stackSize = typeOnStack.sizeOnStack();
-				ArrayUtils(m_context).retrieveLength(typeOnStack);
+				if (
+					typeOnStack.dataStoredIn(DataLocation::CallData) &&
+					typeOnStack.baseType()->isDynamicallyEncoded()
+				)
+				{
+					solAssert(m_context.useABICoderV2(), "");
+					// stack: offset length(optional in case of dynamically sized array)
+					solAssert(typeOnStack.sizeOnStack() == (typeOnStack.isDynamicallySized() ? 2 : 1), "");
+					if (typeOnStack.isDynamicallySized())
+						m_context << Instruction::SWAP1;
 
-				// allocate memory
-				// stack: <source ref> (variably sized) <length>
-				m_context << Instruction::DUP1;
-				ArrayUtils(m_context).convertLengthToSize(targetType, true);
-				// stack: <source ref> (variably sized) <length> <size>
-				if (targetType.isDynamicallySized())
-					m_context << u256(0x20) << Instruction::ADD;
-				allocateMemory();
-				// stack: <source ref> (variably sized) <length> <mem start>
-				m_context << Instruction::DUP1;
-				moveIntoStack(2 + stackSize);
-				if (targetType.isDynamicallySized())
-				{
-					m_context << Instruction::DUP2;
-					storeInMemoryDynamic(*TypeProvider::uint256());
-				}
-				// stack: <mem start> <source ref> (variably sized) <length> <mem data pos>
-				if (targetType.baseType()->isValueType())
-				{
-					copyToStackTop(2 + stackSize, stackSize);
-					ArrayUtils(m_context).copyArrayToMemory(typeOnStack);
+					m_context.callYulFunction(
+						m_context.utilFunctions().conversionFunction(typeOnStack, targetType),
+						typeOnStack.isDynamicallySized() ? 2 : 1,
+						1
+					);
 				}
 				else
 				{
-					if (auto baseType = dynamic_cast<ArrayType const*>(typeOnStack.baseType()))
-						solUnimplementedAssert(
-							typeOnStack.location() != DataLocation::CallData ||
-							!typeOnStack.isDynamicallyEncoded() ||
-							!baseType->isDynamicallySized(),
-							"Copying nested dynamic calldata arrays to memory is not implemented in the old code generator."
-						);
+					// stack: <source ref> (variably sized)
+					unsigned stackSize = typeOnStack.sizeOnStack();
+					ArrayUtils(m_context).retrieveLength(typeOnStack);
 
-					m_context << u256(0) << Instruction::SWAP1;
-					// stack: <mem start> <source ref> (variably sized) <length> <counter> <mem data pos>
-					auto repeat = m_context.newTag();
-					m_context << repeat;
-					m_context << Instruction::DUP3 << Instruction::DUP3;
-					m_context << Instruction::LT << Instruction::ISZERO;
-					auto loopEnd = m_context.appendConditionalJump();
-					copyToStackTop(3 + stackSize, stackSize);
-					copyToStackTop(2 + stackSize, 1);
-					ArrayUtils(m_context).accessIndex(typeOnStack, false);
-					if (typeOnStack.location() == DataLocation::Storage)
-						StorageItem(m_context, *typeOnStack.baseType()).retrieveValue(SourceLocation(), true);
-					convertType(*typeOnStack.baseType(), *targetType.baseType(), _cleanupNeeded);
-					storeInMemoryDynamic(*targetType.baseType(), true);
-					m_context << Instruction::SWAP1 << u256(1) << Instruction::ADD;
-					m_context << Instruction::SWAP1;
-					m_context.appendJumpTo(repeat);
-					m_context << loopEnd;
-					m_context << Instruction::POP;
+					// allocate memory
+					// stack: <source ref> (variably sized) <length>
+					m_context << Instruction::DUP1;
+					ArrayUtils(m_context).convertLengthToSize(targetType, true);
+					// stack: <source ref> (variably sized) <length> <size>
+					if (targetType.isDynamicallySized())
+						m_context << u256(0x20) << Instruction::ADD;
+					allocateMemory();
+					// stack: <source ref> (variably sized) <length> <mem start>
+					m_context << Instruction::DUP1;
+					moveIntoStack(2 + stackSize);
+					if (targetType.isDynamicallySized())
+					{
+						m_context << Instruction::DUP2;
+						storeInMemoryDynamic(*TypeProvider::uint256());
+					}
+					// stack: <mem start> <source ref> (variably sized) <length> <mem data pos>
+					if (targetType.baseType()->isValueType())
+					{
+						copyToStackTop(2 + stackSize, stackSize);
+						ArrayUtils(m_context).copyArrayToMemory(typeOnStack);
+					}
+					else
+					{
+						m_context << u256(0) << Instruction::SWAP1;
+						// stack: <mem start> <source ref> (variably sized) <length> <counter> <mem data pos>
+						auto repeat = m_context.newTag();
+						m_context << repeat;
+						m_context << Instruction::DUP3 << Instruction::DUP3;
+						m_context << Instruction::LT << Instruction::ISZERO;
+						auto loopEnd = m_context.appendConditionalJump();
+						copyToStackTop(3 + stackSize, stackSize);
+						copyToStackTop(2 + stackSize, 1);
+						ArrayUtils(m_context).accessIndex(typeOnStack, false);
+						if (typeOnStack.location() == DataLocation::Storage)
+							StorageItem(m_context, *typeOnStack.baseType()).retrieveValue(SourceLocation(), true);
+						convertType(*typeOnStack.baseType(), *targetType.baseType(), _cleanupNeeded);
+						storeInMemoryDynamic(*targetType.baseType(), true);
+						m_context << Instruction::SWAP1 << u256(1) << Instruction::ADD;
+						m_context << Instruction::SWAP1;
+						m_context.appendJumpTo(repeat);
+						m_context << loopEnd;
+						m_context << Instruction::POP;
+					}
+					// stack: <mem start> <source ref> (variably sized) <length> <mem data pos updated>
+					popStackSlots(2 + stackSize);
+					// Stack: <mem start>
 				}
-				// stack: <mem start> <source ref> (variably sized) <length> <mem data pos updated>
-				popStackSlots(2 + stackSize);
-				// Stack: <mem start>
 			}
 			break;
 		}

libsolidity/codegen/YulUtilFunctions.cpp

@@ -1098,10 +1098,9 @@ string YulUtilFunctions::extractByteArrayLengthFunction()
 	});
 }
 
-std::string YulUtilFunctions::resizeDynamicArrayFunction(ArrayType const& _type)
+std::string YulUtilFunctions::resizeArrayFunction(ArrayType const& _type)
 {
 	solAssert(_type.location() == DataLocation::Storage, "");
-	solAssert(_type.isDynamicallySized(), "");
 	solUnimplementedAssert(_type.baseType()->storageBytes() <= 32, "...");
 
 	if (_type.isByteArray())
@@ -1117,8 +1116,10 @@ std::string YulUtilFunctions::resizeDynamicArrayFunction(ArrayType const& _type)
 
 				let oldLen := <fetchLength>(array)
 
-				// Store new length
-				sstore(array, newLen)
+				<?isDynamic>
+					// Store new length
+					sstore(array, newLen)
+				</isDynamic>
 
 				// Size was reduced, clear end of array
 				if lt(newLen, oldLen) {
@@ -1139,6 +1140,7 @@ std::string YulUtilFunctions::resizeDynamicArrayFunction(ArrayType const& _type)
 			("functionName", functionName)
 			("panic", panicFunction(PanicCode::ResourceError))
 			("fetchLength", arrayLengthFunction(_type))
+			("isDynamic", _type.isDynamicallySized())
 			("convertToSize", arrayConvertLengthToSize(_type))
 			("dataPosition", arrayDataAreaFunction(_type))
 			("clearStorageRange", clearStorageRangeFunction(*_type.baseType()))
@@ -1523,7 +1525,7 @@ string YulUtilFunctions::clearStorageArrayFunction(ArrayType const& _type)
 		)")
 		("functionName", functionName)
 		("dynamic", _type.isDynamicallySized())
-		("resizeArray", _type.isDynamicallySized() ? resizeDynamicArrayFunction(_type) : "")
+		("resizeArray", _type.isDynamicallySized() ? resizeArrayFunction(_type) : "")
 		(
 			"clearRange",
 			clearStorageRangeFunction(
@@ -1595,6 +1597,9 @@ string YulUtilFunctions::copyArrayToStorageFunction(ArrayType const& _fromType,
 		*_fromType.copyForLocation(_toType.location(), _toType.isPointer()) == dynamic_cast<ReferenceType const&>(_toType),
 		""
 	);
+	if (!_toType.isDynamicallySized())
+		solAssert(!_fromType.isDynamicallySized() && _fromType.length() <= _toType.length(), "");
+
 	if (_fromType.isByteArray())
 		return copyByteArrayToStorageFunction(_fromType, _toType);
 	if (_fromType.dataStoredIn(DataLocation::Storage) && _toType.baseType()->isValueType())
@@ -1606,9 +1611,8 @@ string YulUtilFunctions::copyArrayToStorageFunction(ArrayType const& _fromType,
 			function <functionName>(slot, value<?isFromDynamicCalldata>, len</isFromDynamicCalldata>) {
 				<?fromStorage> if eq(slot, value) { leave } </fromStorage>
 				let length := <arrayLength>(value<?isFromDynamicCalldata>, len</isFromDynamicCalldata>)
-				<?isToDynamic>
-					<resizeArray>(slot, length)
-				</isToDynamic>
+
+				<resizeArray>(slot, length)
 
 				let srcPtr := <srcDataLocation>(value)
 
@@ -1662,7 +1666,6 @@ string YulUtilFunctions::copyArrayToStorageFunction(ArrayType const& _fromType,
 		bool fromMemory = _fromType.dataStoredIn(DataLocation::Memory);
 		templ("fromMemory", fromMemory);
 		templ("fromCalldata", fromCalldata);
-		templ("isToDynamic", _toType.isDynamicallySized());
 		templ("srcDataLocation", arrayDataAreaFunction(_fromType));
 		if (fromCalldata)
 		{
@@ -1671,8 +1674,7 @@ string YulUtilFunctions::copyArrayToStorageFunction(ArrayType const& _fromType,
 			if (_fromType.baseType()->isDynamicallyEncoded())
 				templ("accessCalldataTail", accessCalldataTailFunction(*_fromType.baseType()));
 		}
-		if (_toType.isDynamicallySized())
-			templ("resizeArray", resizeDynamicArrayFunction(_toType));
+		templ("resizeArray", resizeArrayFunction(_toType));
 		templ("arrayLength",arrayLengthFunction(_fromType));
 		templ("isValueType", _fromType.baseType()->isValueType());
 		templ("dstDataLocation", arrayDataAreaFunction(_toType));
@@ -1791,6 +1793,8 @@ string YulUtilFunctions::copyValueArrayStorageToStorageFunction(ArrayType const&
 	solAssert(_fromType.dataStoredIn(DataLocation::Storage) && _toType.baseType()->isValueType(), "");
 	solAssert(_toType.dataStoredIn(DataLocation::Storage), "");
 
+	solUnimplementedAssert(_fromType.storageStride() == _toType.storageStride(), "");
+
 	string functionName = "copy_array_to_storage_from_" + _fromType.identifier() + "_to_" + _toType.identifier();
 	return m_functionCollector.createFunction(functionName, [&](){
 		Whiskers templ(R"(
@@ -1799,9 +1803,7 @@ string YulUtilFunctions::copyValueArrayStorageToStorageFunction(ArrayType const&
 				let length := <arrayLength>(src)
 				// Make sure array length is sane
 				if gt(length, 0xffffffffffffffff) { <panic>() }
-				<?isToDynamic>
-					<resizeArray>(dst, length)
-				</isToDynamic>
+				<resizeArray>(dst, length)
 
 				let srcPtr := <srcDataLocation>(src)
 
@@ -1821,9 +1823,7 @@ string YulUtilFunctions::copyValueArrayStorageToStorageFunction(ArrayType const&
 		if (_fromType.dataStoredIn(DataLocation::Storage))
 			solAssert(!_fromType.isValueType(), "");
 		templ("functionName", functionName);
-		templ("isToDynamic", _toType.isDynamicallySized());
-		if (_toType.isDynamicallySized())
-			templ("resizeArray", resizeDynamicArrayFunction(_toType));
+		templ("resizeArray", resizeArrayFunction(_toType));
 		templ("arrayLength",arrayLengthFunction(_fromType));
 		templ("panic", panicFunction(PanicCode::ResourceError));
 		templ("srcDataLocation", arrayDataAreaFunction(_fromType));

libsolidity/codegen/YulUtilFunctions.h

@@ -194,8 +194,9 @@ public:
 	std::string extractByteArrayLengthFunction();
 
 	/// @returns the name of a function that resizes a storage array
+	/// for statically sized arrays, it will just clean-up elements of array starting from newLen until the end
 	/// signature: (array, newLen)
-	std::string resizeDynamicArrayFunction(ArrayType const& _type);
+	std::string resizeArrayFunction(ArrayType const& _type);
 
 	/// @returns the name of a function that reduces the size of a storage array by one element
 	/// signature: (array)

libsolidity/codegen/ir/IRGenerator.cpp

@@ -249,6 +249,7 @@ string IRGenerator::generateFunction(FunctionDefinition const& _function)
 {
 	string functionName = IRNames::function(_function);
 	return m_context.functionCollector().createFunction(functionName, [&]() {
+		solUnimplementedAssert(_function.modifiers().empty(), "Modifiers not implemented yet.");
 		Whiskers t(R"(
 			function <functionName>(<params>)<?+retParams> -> <retParams></+retParams> {
 				<initReturnVariables>
@@ -521,8 +522,16 @@ void IRGenerator::generateImplicitConstructors(ContractDefinition const& _contra
 			)");
 			vector<string> params;
 			if (contract->constructor())
+			{
+				for (auto const& modifierInvocation: contract->constructor()->modifiers())
+					// This can be ContractDefinition too for super arguments. That is supported.
+					solUnimplementedAssert(
+						!dynamic_cast<ModifierDefinition const*>(modifierInvocation->name().annotation().referencedDeclaration),
+						"Modifiers not implemented yet."
+					);
 				for (ASTPointer<VariableDeclaration> const& varDecl: contract->constructor()->parameters())
 					params += m_context.addLocalVariable(*varDecl).stackSlots();
+			}
 			t("params", joinHumanReadable(params));
 			vector<string> baseParams = listAllParams(baseConstructorParams);
 			t("baseParams", joinHumanReadable(baseParams));

libsolidity/codegen/ir/IRGeneratorForStatements.cpp

@@ -712,10 +712,16 @@ void IRGeneratorForStatements::endVisit(UnaryOperation const& _unaryOperation)
 		else
 			solUnimplementedAssert(false, "Unary operator not yet implemented");
 	}
+	else if (resultType.category() == Type::Category::FixedBytes)
+	{
+		solAssert(op == Token::BitNot, "Only bitwise negation is allowed for FixedBytes");
+		solAssert(resultType == type(_unaryOperation.subExpression()), "Result type doesn't match!");
+		appendSimpleUnaryOperation(_unaryOperation, _unaryOperation.subExpression());
+	}
 	else if (resultType.category() == Type::Category::Bool)
 	{
 		solAssert(
-			_unaryOperation.getOperator() != Token::BitNot,
+			op != Token::BitNot,
 			"Bitwise Negation can't be done on bool!"
 		);
 
@@ -1794,6 +1800,11 @@ void IRGeneratorForStatements::endVisit(MemberAccess const& _memberAccess)
 					", " <<
 					offset <<
 					")\n";
+			else if (
+				dynamic_cast<ArrayType const*>(_memberAccess.annotation().type) ||
+				dynamic_cast<StructType const*>(_memberAccess.annotation().type)
+			)
+				define(_memberAccess) << offset << "\n";
 			else
 				define(_memberAccess) <<
 					m_utils.readFromCalldata(*_memberAccess.annotation().type) <<

libsolidity/formal/BMC.cpp

@@ -162,6 +162,7 @@ void BMC::endVisit(FunctionDefinition const& _function)
 		smtutil::Expression constraints = m_context.assertions();
 		checkVerificationTargets(constraints);
 		m_verificationTargets.clear();
+		m_pathConditions.clear();
 	}
 
 	SMTEncoder::endVisit(_function);
@@ -184,7 +185,26 @@ bool BMC::visit(IfStatement const& _node)
 		);
 	m_context.popSolver();
 
-	SMTEncoder::visit(_node);
+	_node.condition().accept(*this);
+	auto conditionExpr = expr(_node.condition());
+	// visit true branch
+	auto [indicesEndTrue, trueEndPathCondition] = visitBranch(&_node.trueStatement(), conditionExpr);
+	auto touchedVars = touchedVariables(_node.trueStatement());
+
+	// visit false branch
+	decltype(indicesEndTrue) indicesEndFalse;
+	auto falseEndPathCondition = currentPathConditions() && !conditionExpr;
+	if (_node.falseStatement())
+	{
+		std::tie(indicesEndFalse, falseEndPathCondition) = visitBranch(_node.falseStatement(), !conditionExpr);
+		touchedVars += touchedVariables(*_node.falseStatement());
+	}
+	else
+		indicesEndFalse = copyVariableIndices();
+
+	// merge the information from branches
+	setPathCondition(trueEndPathCondition || falseEndPathCondition);
+	mergeVariables(touchedVars, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
 
 	return false;
 }
@@ -224,7 +244,7 @@ bool BMC::visit(WhileStatement const& _node)
 	decltype(indicesBeforeLoop) indicesAfterLoop;
 	if (_node.isDoWhile())
 	{
-		indicesAfterLoop = visitBranch(&_node.body());
+		indicesAfterLoop = visitBranch(&_node.body()).first;
 		// TODO the assertions generated in the body should still be active in the condition
 		_node.condition().accept(*this);
 		if (isRootFunction())
@@ -244,7 +264,7 @@ bool BMC::visit(WhileStatement const& _node)
 				&_node.condition()
 			);
 
-		indicesAfterLoop = visitBranch(&_node.body(), expr(_node.condition()));
+		indicesAfterLoop = visitBranch(&_node.body(), expr(_node.condition())).first;
 	}
 
 	// We reset the execution to before the loop
@@ -406,6 +426,12 @@ void BMC::endVisit(FunctionCall const& _funCall)
 	}
 }
 
+void BMC::endVisit(Return const& _return)
+{
+	SMTEncoder::endVisit(_return);
+	setPathCondition(smtutil::Expression(false));
+}
+
 /// Visitor helpers.
 
 void BMC::visitAssert(FunctionCall const& _funCall)
@@ -467,7 +493,9 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 		// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
 		// is that there we don't have `_funCall`.
 		pushCallStack({funDef, &_funCall});
+		pushPathCondition(currentPathConditions());
 		funDef->accept(*this);
+		popPathCondition();
 	}
 
 	createReturnedExpressions(_funCall);
@@ -968,3 +996,14 @@ smtutil::CheckResult BMC::checkSatisfiable()
 	return checkSatisfiableAndGenerateModel({}).first;
 }
 
+void BMC::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value)
+{
+	auto oldVar = _symVar.currentValue();
+	auto newVar = _symVar.increaseIndex();
+	m_context.addAssertion(smtutil::Expression::ite(
+		currentPathConditions(),
+		newVar == _value,
+		newVar == oldVar
+	));
+}
+

libsolidity/formal/BMC.h

@@ -90,6 +90,7 @@ private:
 	bool visit(ForStatement const& _node) override;
 	void endVisit(UnaryOperation const& _node) override;
 	void endVisit(FunctionCall const& _node) override;
+	void endVisit(Return const& _node) override;
 	//@}
 
 	/// Visitor helpers.
@@ -97,6 +98,7 @@ private:
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);
 	void visitAddMulMod(FunctionCall const& _funCall) override;
+	void assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value) override;
 	/// Visits the FunctionDefinition of the called function
 	/// if available and inlines the return value.
 	void inlineFunctionCall(FunctionCall const& _funCall);

libsolidity/formal/SMTEncoder.cpp

@@ -155,8 +155,10 @@ void SMTEncoder::visitFunctionOrModifier()
 
 	if (m_modifierDepthStack.back() == static_cast<int>(function.modifiers().size()))
 	{
+		pushPathCondition(currentPathConditions());
 		if (function.isImplemented())
 			function.body().accept(*this);
+		popPathCondition();
 	}
 	else
 	{
@@ -193,6 +195,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation,
 	initializeFunctionCallParameters(*_definition, args);
 
 	pushCallStack({_definition, _invocation});
+	pushPathCondition(currentPathConditions());
 	if (auto modifier = dynamic_cast<ModifierDefinition const*>(_definition))
 	{
 		if (modifier->isImplemented())
@@ -205,6 +208,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation,
 			function->accept(*this);
 		// Functions are popped from the callstack in endVisit(FunctionDefinition)
 	}
+	popPathCondition();
 }
 
 void SMTEncoder::inlineConstructorHierarchy(ContractDefinition const& _contract)
@@ -288,26 +292,6 @@ bool SMTEncoder::visit(TryCatchClause const& _clause)
 	return false;
 }
 
-bool SMTEncoder::visit(IfStatement const& _node)
-{
-	_node.condition().accept(*this);
-
-	auto indicesEndTrue = visitBranch(&_node.trueStatement(), expr(_node.condition()));
-	auto touchedVars = touchedVariables(_node.trueStatement());
-	decltype(indicesEndTrue) indicesEndFalse;
-	if (_node.falseStatement())
-	{
-		indicesEndFalse = visitBranch(_node.falseStatement(), !expr(_node.condition()));
-		touchedVars += touchedVariables(*_node.falseStatement());
-	}
-	else
-		indicesEndFalse = copyVariableIndices();
-
-	mergeVariables(touchedVars, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
-
-	return false;
-}
-
 void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
 {
 	if (_varDecl.declarations().size() != 1)
@@ -598,10 +582,10 @@ bool SMTEncoder::visit(Conditional const& _op)
 {
 	_op.condition().accept(*this);
 
-	auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition()));
+	auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition())).first;
 	auto touchedVars = touchedVariables(_op.trueExpression());
 
-	auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition()));
+	auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition())).first;
 	touchedVars += touchedVariables(_op.falseExpression());
 
 	mergeVariables(touchedVars, expr(_op.condition()), indicesEndTrue, indicesEndFalse);
@@ -1749,13 +1733,13 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op)
 		_op.leftExpression().accept(*this);
 		if (_op.getOperator() == Token::And)
 		{
-			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression()));
+			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first;
 			mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 			defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
 		}
 		else
 		{
-			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression()));
+			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first;
 			mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 			defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
 		}
@@ -1969,22 +1953,29 @@ void SMTEncoder::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression
 	m_context.addAssertion(_symVar.increaseIndex() == _value);
 }
 
-SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression _condition)
+pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
+	ASTNode const* _statement,
+	smtutil::Expression _condition
+)
 {
 	return visitBranch(_statement, &_condition);
 }
 
-SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition)
+pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
+	ASTNode const* _statement,
+	smtutil::Expression const* _condition
+)
 {
 	auto indicesBeforeBranch = copyVariableIndices();
 	if (_condition)
 		pushPathCondition(*_condition);
 	_statement->accept(*this);
+	auto pathConditionOnExit = currentPathConditions();
 	if (_condition)
 		popPathCondition();
 	auto indicesAfterBranch = copyVariableIndices();
 	resetVariableIndices(indicesBeforeBranch);
-	return indicesAfterBranch;
+	return {indicesAfterBranch, pathConditionOnExit};
 }
 
 void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector<smtutil::Expression> const& _callArgs)
@@ -2240,6 +2231,14 @@ void SMTEncoder::pushPathCondition(smtutil::Expression const& _e)
 	m_pathConditions.push_back(currentPathConditions() && _e);
 }
 
+void SMTEncoder::setPathCondition(smtutil::Expression const& _e)
+{
+	if (m_pathConditions.empty())
+		m_pathConditions.push_back(_e);
+	else
+		m_pathConditions.back() = _e;
+}
+
 smtutil::Expression SMTEncoder::currentPathConditions()
 {
 	if (m_pathConditions.empty())

libsolidity/formal/SMTEncoder.h

@@ -89,7 +89,7 @@ protected:
 	bool visit(FunctionDefinition const& _node) override;
 	void endVisit(FunctionDefinition const& _node) override;
 	bool visit(PlaceholderStatement const& _node) override;
-	bool visit(IfStatement const& _node) override;
+	bool visit(IfStatement const&) override { return false; }
 	bool visit(WhileStatement const&) override { return false; }
 	bool visit(ForStatement const&) override { return false; }
 	void endVisit(VariableDeclarationStatement const& _node) override;
@@ -197,7 +197,7 @@ protected:
 
 	/// Handles the actual assertion of the new value to the encoding context.
 	/// Other assignment methods should use this one in the end.
-	void assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value);
+	virtual void assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value);
 
 	void assignment(VariableDeclaration const& _variable, Expression const& _value);
 	/// Handles assignments to variables of different types.
@@ -219,9 +219,10 @@ protected:
 
 	/// Visits the branch given by the statement, pushes and pops the current path conditions.
 	/// @param _condition if present, asserts that this condition is true within the branch.
-	/// @returns the variable indices after visiting the branch.
-	VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition = nullptr);
-	VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression _condition);
+	/// @returns the variable indices after visiting the branch and the expression representing
+	/// the path condition at the end of the branch.
+	std::pair<VariableIndices, smtutil::Expression> visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition = nullptr);
+	std::pair<VariableIndices, smtutil::Expression> visitBranch(ASTNode const* _statement, smtutil::Expression _condition);
 
 	using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
 
@@ -263,6 +264,8 @@ protected:
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smtutil::Expression _value);
 
+	/// Overwrites the current path condition
+	void setPathCondition(smtutil::Expression const& _e);
 	/// Adds a new path condition
 	void pushPathCondition(smtutil::Expression const& _e);
 	/// Remove the last path condition