Merge pull request #9925 from ethereum/develop

Merge develop into breaking.

Changelog.md

@@ -3,6 +3,8 @@
 Breaking Changes:
  * Type System: Unary negation can only be used on signed integers, not on unsigned integers.
 
+Compiler Features:
+ * SMTChecker: Support ``addmod`` and ``mulmod``.
 
 ### 0.7.3 (unreleased)
 

libsolidity/CMakeLists.txt

@@ -104,6 +104,8 @@ set(sources
 	formal/ModelChecker.h
 	formal/Predicate.cpp
 	formal/Predicate.h
+	formal/PredicateInstance.cpp
+	formal/PredicateInstance.h
 	formal/PredicateSort.cpp
 	formal/PredicateSort.h
 	formal/SMTEncoder.cpp

libsolidity/analysis/ImmutableValidator.cpp

@@ -125,7 +125,7 @@ bool ImmutableValidator::visit(WhileStatement const& _whileStatement)
 void ImmutableValidator::endVisit(Identifier const& _identifier)
 {
 	if (auto const callableDef = dynamic_cast<CallableDeclaration const*>(_identifier.annotation().referencedDeclaration))
-		visitCallableIfNew(callableDef->resolveVirtual(m_currentContract));
+		visitCallableIfNew(*_identifier.annotation().requiredLookup == VirtualLookup::Virtual ? callableDef->resolveVirtual(m_currentContract) : *callableDef);
 	if (auto const varDecl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
 		analyseVariableReference(*varDecl, _identifier);
 }

libsolidity/analysis/TypeChecker.cpp

@@ -2546,8 +2546,10 @@ bool TypeChecker::visit(MemberAccess const& _memberAccess)
 	TypePointer exprType = type(_memberAccess.expression());
 	ASTString const& memberName = _memberAccess.memberName();
 
+	auto& annotation = _memberAccess.annotation();
+
 	// Retrieve the types of the arguments if this is used to call a function.
-	auto const& arguments = _memberAccess.annotation().arguments;
+	auto const& arguments = annotation.arguments;
 	MemberList::MemberMap possibleMembers = exprType->members(currentDefinitionScope()).membersByName(memberName);
 	size_t const initialMemberCount = possibleMembers.size();
 	if (initialMemberCount > 1 && arguments)
@@ -2563,8 +2565,6 @@ bool TypeChecker::visit(MemberAccess const& _memberAccess)
 				++it;
 	}
 
-	auto& annotation = _memberAccess.annotation();
-
 	annotation.isConstant = false;
 
 	if (possibleMembers.empty())
@@ -2663,6 +2663,8 @@ bool TypeChecker::visit(MemberAccess const& _memberAccess)
 	annotation.referencedDeclaration = possibleMembers.front().declaration;
 	annotation.type = possibleMembers.front().type;
 
+	VirtualLookup requiredLookup = VirtualLookup::Static;
+
 	if (auto funType = dynamic_cast<FunctionType const*>(annotation.type))
 	{
 		solAssert(
@@ -2681,8 +2683,15 @@ bool TypeChecker::visit(MemberAccess const& _memberAccess)
 				_memberAccess.location(),
 				"Using \"." + memberName + "(...)\" is deprecated. Use \"{" + memberName + ": ...}\" instead."
 			);
+
+		if (!funType->bound())
+			if (auto contractType = dynamic_cast<ContractType const*>(exprType))
+				requiredLookup = contractType->isSuper() ? VirtualLookup::Super : VirtualLookup::Virtual;
+
 	}
 
+	annotation.requiredLookup = requiredLookup;
+
 	if (auto const* structType = dynamic_cast<StructType const*>(exprType))
 		annotation.isLValue = !structType->dataStoredIn(DataLocation::CallData);
 	else if (exprType->category() == Type::Category::Array)
@@ -3078,6 +3087,10 @@ bool TypeChecker::visit(Identifier const& _identifier)
 
 	annotation.isConstant = isConstant;
 
+	annotation.requiredLookup =
+		dynamic_cast<CallableDeclaration const*>(annotation.referencedDeclaration) ?
+		VirtualLookup::Virtual : VirtualLookup::Static;
+
 	// Check for deprecated function names.
 	// The check is done here for the case without an actual function call.
 	if (FunctionType const* fType = dynamic_cast<FunctionType const*>(_identifier.annotation().type))

libsolidity/ast/AST.h

@@ -566,7 +566,10 @@ public:
 		ASTPointer<UserDefinedTypeName> _baseName,
 		std::unique_ptr<std::vector<ASTPointer<Expression>>> _arguments
 	):
-		ASTNode(_id, _location), m_baseName(std::move(_baseName)), m_arguments(std::move(_arguments)) {}
+		ASTNode(_id, _location), m_baseName(std::move(_baseName)), m_arguments(std::move(_arguments))
+	{
+		solAssert(m_baseName != nullptr, "Name cannot be null.");
+	}
 
 	void accept(ASTVisitor& _visitor) override;
 	void accept(ASTConstVisitor& _visitor) const override;
@@ -596,7 +599,10 @@ public:
 		ASTPointer<UserDefinedTypeName> _libraryName,
 		ASTPointer<TypeName> _typeName
 	):
-		ASTNode(_id, _location), m_libraryName(std::move(_libraryName)), m_typeName(std::move(_typeName)) {}
+		ASTNode(_id, _location), m_libraryName(std::move(_libraryName)), m_typeName(std::move(_typeName))
+	{
+		solAssert(m_libraryName != nullptr, "Name cannot be null.");
+	}
 
 	void accept(ASTVisitor& _visitor) override;
 	void accept(ASTConstVisitor& _visitor) const override;
@@ -1052,7 +1058,10 @@ public:
 		ASTPointer<Identifier> _name,
 		std::unique_ptr<std::vector<ASTPointer<Expression>>> _arguments
 	):
-		ASTNode(_id, _location), m_modifierName(std::move(_name)), m_arguments(std::move(_arguments)) {}
+		ASTNode(_id, _location), m_modifierName(std::move(_name)), m_arguments(std::move(_arguments))
+	{
+		solAssert(m_modifierName != nullptr, "Name cannot be null.");
+	}
 
 	void accept(ASTVisitor& _visitor) override;
 	void accept(ASTConstVisitor& _visitor) const override;
@@ -1195,6 +1204,7 @@ class UserDefinedTypeName: public TypeName
 public:
 	UserDefinedTypeName(int64_t _id, SourceLocation const& _location, std::vector<ASTString> _namePath):
 		TypeName(_id, _location), m_namePath(std::move(_namePath)) {}
+
 	void accept(ASTVisitor& _visitor) override;
 	void accept(ASTConstVisitor& _visitor) const override;
 

libsolidity/ast/ASTAnnotations.h

@@ -264,6 +264,8 @@ struct IdentifierAnnotation: ExpressionAnnotation
 {
 	/// Referenced declaration, set at latest during overload resolution stage.
 	Declaration const* referencedDeclaration = nullptr;
+	/// What kind of lookup needs to be done (static, virtual, super) find the declaration.
+	SetOnce<VirtualLookup> requiredLookup;
 	/// List of possible declarations it could refer to (can contain duplicates).
 	std::vector<Declaration const*> candidateDeclarations;
 	/// List of possible declarations it could refer to.
@@ -274,6 +276,8 @@ struct MemberAccessAnnotation: ExpressionAnnotation
 {
 	/// Referenced declaration, set at latest during overload resolution stage.
 	Declaration const* referencedDeclaration = nullptr;
+	/// What kind of lookup needs to be done (static, virtual, super) find the declaration.
+	SetOnce<VirtualLookup> requiredLookup;
 };
 
 struct BinaryOperationAnnotation: ExpressionAnnotation

libsolidity/ast/ASTEnums.h

@@ -30,6 +30,9 @@
 namespace solidity::frontend
 {
 
+/// Possible lookups for function resolving
+enum class VirtualLookup { Static, Virtual, Super };
+
 // How a function can mutate the EVM state.
 enum class StateMutability { Pure, View, NonPayable, Payable };
 

libsolidity/ast/Types.h

@@ -1380,7 +1380,9 @@ private:
 	bool const m_arbitraryParameters = false;
 	bool const m_gasSet = false; ///< true iff the gas value to be used is on the stack
 	bool const m_valueSet = false; ///< true iff the value to be sent is on the stack
-	bool const m_bound = false; ///< true iff the function is called as arg1.fun(arg2, ..., argn)
+	/// true iff the function is called as arg1.fun(arg2, ..., argn).
+	/// This is achieved through the "using for" directive.
+	bool const m_bound = false;
 	Declaration const* m_declaration = nullptr;
 	bool m_saltSet = false; ///< true iff the salt value to be used is on the stack
 };

libsolidity/codegen/ContractCompiler.cpp

@@ -1299,6 +1299,8 @@ void ContractCompiler::appendModifierOrFunctionCode()
 			appendModifierOrFunctionCode();
 		else
 		{
+			solAssert(*modifierInvocation->name()->annotation().requiredLookup == VirtualLookup::Virtual, "");
+
 			ModifierDefinition const& modifier = dynamic_cast<ModifierDefinition const&>(
 				*modifierInvocation->name()->annotation().referencedDeclaration
 			).resolveVirtual(m_context.mostDerivedContract());

libsolidity/codegen/ExpressionCompiler.cpp

@@ -595,6 +595,7 @@ bool ExpressionCompiler::visit(FunctionCall const& _functionCall)
 						// Do not directly visit the identifier, because this way, we can avoid
 						// the runtime entry label to be created at the creation time context.
 						CompilerContext::LocationSetter locationSetter2(m_context, *identifier);
+						solAssert(*identifier->annotation().requiredLookup == VirtualLookup::Virtual, "");
 						utils().pushCombinedFunctionEntryLabel(
 							functionDef->resolveVirtual(m_context.mostDerivedContract()),
 							false
@@ -1311,6 +1312,7 @@ bool ExpressionCompiler::visit(MemberAccess const& _memberAccess)
 			if (funType->kind() == FunctionType::Kind::Internal)
 			{
 				FunctionDefinition const& funDef = dynamic_cast<decltype(funDef)>(funType->declaration());
+				solAssert(*_memberAccess.annotation().requiredLookup == VirtualLookup::Static, "");
 				utils().pushCombinedFunctionEntryLabel(funDef);
 				utils().moveIntoStack(funType->selfType()->sizeOnStack(), 1);
 			}
@@ -1346,7 +1348,10 @@ bool ExpressionCompiler::visit(MemberAccess const& _memberAccess)
 					// internal library function call, this would push the library address forcing
 					// us to link against it although we actually do not need it.
 					if (auto const* function = dynamic_cast<FunctionDefinition const*>(_memberAccess.annotation().referencedDeclaration))
+					{
+						solAssert(*_memberAccess.annotation().requiredLookup == VirtualLookup::Static, "");
 						utils().pushCombinedFunctionEntryLabel(*function);
+					}
 					else
 						solAssert(false, "Function not found in member access");
 					break;
@@ -1460,6 +1465,7 @@ bool ExpressionCompiler::visit(MemberAccess const& _memberAccess)
 		if (type.isSuper())
 		{
 			solAssert(!!_memberAccess.annotation().referencedDeclaration, "Referenced declaration not resolved.");
+			solAssert(*_memberAccess.annotation().requiredLookup == VirtualLookup::Super, "");
 			utils().pushCombinedFunctionEntryLabel(m_context.superFunction(
 				dynamic_cast<FunctionDefinition const&>(*_memberAccess.annotation().referencedDeclaration),
 				type.contractDefinition()
@@ -1742,6 +1748,7 @@ bool ExpressionCompiler::visit(MemberAccess const& _memberAccess)
 			auto const* funDef = dynamic_cast<FunctionDefinition const*>(_memberAccess.annotation().referencedDeclaration);
 			solAssert(funDef && funDef->isFree(), "");
 			solAssert(funType->kind() == FunctionType::Kind::Internal, "");
+			solAssert(*_memberAccess.annotation().requiredLookup == VirtualLookup::Static, "");
 			utils().pushCombinedFunctionEntryLabel(*funDef);
 		}
 		break;
@@ -1933,11 +1940,14 @@ void ExpressionCompiler::endVisit(Identifier const& _identifier)
 		}
 	}
 	else if (FunctionDefinition const* functionDef = dynamic_cast<FunctionDefinition const*>(declaration))
+	{
 		// If the identifier is called right away, this code is executed in visit(FunctionCall...), because
 		// we want to avoid having a reference to the runtime function entry point in the
 		// constructor context, since this would force the compiler to include unreferenced
 		// internal functions in the runtime context.
+		solAssert(*_identifier.annotation().requiredLookup == VirtualLookup::Virtual, "");
 		utils().pushCombinedFunctionEntryLabel(functionDef->resolveVirtual(m_context.mostDerivedContract()));
+	}
 	else if (auto variable = dynamic_cast<VariableDeclaration const*>(declaration))
 		appendVariable(*variable, static_cast<Expression const&>(_identifier));
 	else if (auto contract = dynamic_cast<ContractDefinition const*>(declaration))

libsolidity/codegen/ir/IRGeneratorForStatements.cpp

@@ -839,7 +839,10 @@ void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall)
 			solAssert(functionType->declaration() == *functionDef, "");
 
 			if (identifier)
+			{
+				solAssert(*identifier->annotation().requiredLookup == VirtualLookup::Virtual, "");
 				functionDef = &functionDef->resolveVirtual(m_context.mostDerivedContract());
+			}
 			else
 			{
 				ContractType const* type = dynamic_cast<ContractType const*>(memberAccess->expression().annotation().type);
@@ -847,6 +850,7 @@ void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall)
 				{
 					ContractDefinition const* super = type->contractDefinition().superContract(m_context.mostDerivedContract());
 					solAssert(super, "Super contract not available.");
+					solAssert(*memberAccess->annotation().requiredLookup == VirtualLookup::Super, "");
 					functionDef = &functionDef->resolveVirtual(m_context.mostDerivedContract(), super);
 				}
 			}
@@ -2086,6 +2090,7 @@ void IRGeneratorForStatements::endVisit(Identifier const& _identifier)
 	}
 	else if (FunctionDefinition const* functionDef = dynamic_cast<FunctionDefinition const*>(declaration))
 	{
+		solAssert(*_identifier.annotation().requiredLookup == VirtualLookup::Virtual, "");
 		FunctionDefinition const& resolvedFunctionDef = functionDef->resolveVirtual(m_context.mostDerivedContract());
 		define(_identifier) << to_string(resolvedFunctionDef.id()) << "\n";
 

libsolidity/formal/BMC.cpp

@@ -390,8 +390,6 @@ void BMC::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::SHA256:
 	case FunctionType::Kind::RIPEMD160:
 	case FunctionType::Kind::BlockHash:
-	case FunctionType::Kind::AddMod:
-	case FunctionType::Kind::MulMod:
 		SMTEncoder::endVisit(_funCall);
 		abstractFunctionCall(_funCall);
 		break;
@@ -410,6 +408,9 @@ void BMC::endVisit(FunctionCall const& _funCall)
 		);
 		break;
 	}
+	case FunctionType::Kind::AddMod:
+	case FunctionType::Kind::MulMod:
+		[[fallthrough]];
 	default:
 		SMTEncoder::endVisit(_funCall);
 		break;
@@ -443,6 +444,18 @@ void BMC::visitRequire(FunctionCall const& _funCall)
 		);
 }
 
+void BMC::visitAddMulMod(FunctionCall const& _funCall)
+{
+	solAssert(_funCall.arguments().at(2), "");
+	addVerificationTarget(
+		VerificationTarget::Type::DivByZero,
+		expr(*_funCall.arguments().at(2)),
+		&_funCall
+	);
+
+	SMTEncoder::visitAddMulMod(_funCall);
+}
+
 void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 {
 	solAssert(shouldInlineFunctionCall(_funCall), "");

libsolidity/formal/BMC.h

@@ -95,6 +95,7 @@ private:
 	//@{
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);
+	void visitAddMulMod(FunctionCall const& _funCall) override;
 	/// Visits the FunctionDefinition of the called function
 	/// if available and inlines the return value.
 	void inlineFunctionCall(FunctionCall const& _funCall);

libsolidity/formal/CHC.cpp

@@ -22,6 +22,7 @@
 #include <libsmtutil/Z3CHCInterface.h>
 #endif
 
+#include <libsolidity/formal/PredicateInstance.h>
 #include <libsolidity/formal/PredicateSort.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
@@ -101,10 +102,9 @@ bool CHC::visit(ContractDefinition const& _contract)
 	m_constructorSummaryPredicate = createSymbolicBlock(
 		constructorSort(*m_currentContract),
 		"summary_constructor_" + contractSuffix(_contract),
+		PredicateType::ConstructorSummary,
 		&_contract
 	);
-	auto stateExprs = currentStateVariables();
-	setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
 
 	SMTEncoder::visit(_contract);
 	return false;
@@ -115,12 +115,13 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	auto implicitConstructorPredicate = createSymbolicBlock(
 		implicitConstructorSort(),
 		"implicit_constructor_" + contractSuffix(_contract),
+		PredicateType::ImplicitConstructor,
 		&_contract
 	);
 	auto implicitConstructor = (*implicitConstructorPredicate)({});
 	addRule(implicitConstructor, implicitConstructor.name);
 	m_currentBlock = implicitConstructor;
-	m_context.addAssertion(m_error.currentValue() == 0);
+	m_context.addAssertion(errorFlag().currentValue() == 0);
 
 	if (auto constructor = _contract.constructor())
 		constructor->accept(*this);
@@ -129,12 +130,10 @@ void CHC::endVisit(ContractDefinition const& _contract)
 
 	connectBlocks(m_currentBlock, summary(_contract));
 
-	clearIndices(m_currentContract, nullptr);
+	setCurrentBlock(*m_constructorSummaryPredicate);
-	vector<smtutil::Expression> symbArgs = currentFunctionVariables(*m_currentContract);
-	setCurrentBlock(*m_constructorSummaryPredicate, &symbArgs);
 
-	addAssertVerificationTarget(m_currentContract, m_currentBlock, smtutil::Expression(true), m_error.currentValue());
+	addAssertVerificationTarget(m_currentContract, m_currentBlock, smtutil::Expression(true), errorFlag().currentValue());
-	connectBlocks(m_currentBlock, interface(), m_error.currentValue() == 0);
+	connectBlocks(m_currentBlock, interface(), errorFlag().currentValue() == 0);
 
 	SMTEncoder::endVisit(_contract);
 }
@@ -162,10 +161,10 @@ bool CHC::visit(FunctionDefinition const& _function)
 
 	initFunction(_function);
 
-	auto functionEntryBlock = createBlock(m_currentFunction);
+	auto functionEntryBlock = createBlock(m_currentFunction, PredicateType::FunctionEntry);
-	auto bodyBlock = createBlock(&m_currentFunction->body());
+	auto bodyBlock = createBlock(&m_currentFunction->body(), PredicateType::FunctionBlock);
 
-	auto functionPred = predicate(*functionEntryBlock, currentFunctionVariables());
+	auto functionPred = predicate(*functionEntryBlock);
 	auto bodyPred = predicate(*bodyBlock);
 
 	if (_function.isConstructor())
@@ -173,7 +172,7 @@ bool CHC::visit(FunctionDefinition const& _function)
 	else
 		addRule(functionPred, functionPred.name);
 
-	m_context.addAssertion(m_error.currentValue() == 0);
+	m_context.addAssertion(errorFlag().currentValue() == 0);
 	for (auto const* var: m_stateVariables)
 		m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var));
 	for (auto const& var: _function.parameters())
@@ -217,29 +216,28 @@ void CHC::endVisit(FunctionDefinition const& _function)
 			auto constructorExit = createSymbolicBlock(
 				constructorSort(*m_currentContract),
 				"constructor_exit_" + suffix,
+				PredicateType::ConstructorSummary,
 				m_currentContract
 			);
-			connectBlocks(m_currentBlock, predicate(*constructorExit, currentFunctionVariables(*m_currentContract)));
+			connectBlocks(m_currentBlock, predicate(*constructorExit));
 
-			clearIndices(m_currentContract, m_currentFunction);
+			setCurrentBlock(*constructorExit);
-			auto stateExprs = currentFunctionVariables(*m_currentContract);
-			setCurrentBlock(*constructorExit, &stateExprs);
 		}
 		else
 		{
-			auto assertionError = m_error.currentValue();
+			auto assertionError = errorFlag().currentValue();
 			auto sum = summary(_function);
 			connectBlocks(m_currentBlock, sum);
 
 			auto iface = interface();
 
-			auto stateExprs = initialStateVariables();
+			setCurrentBlock(*m_interfaces.at(m_currentContract));
-			setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
 
+			auto ifacePre = (*m_interfaces.at(m_currentContract))(initialStateVariables());
 			if (_function.isPublic())
 			{
-				addAssertVerificationTarget(&_function, m_currentBlock, sum, assertionError);
+				addAssertVerificationTarget(&_function, ifacePre, sum, assertionError);
-				connectBlocks(m_currentBlock, iface, sum && (assertionError == 0));
+				connectBlocks(ifacePre, iface, sum && (assertionError == 0));
 			}
 		}
 		m_currentFunction = nullptr;
@@ -258,10 +256,10 @@ bool CHC::visit(IfStatement const& _if)
 	solAssert(m_currentFunction, "");
 	auto const& functionBody = m_currentFunction->body();
 
-	auto ifHeaderBlock = createBlock(&_if, "if_header_");
+	auto ifHeaderBlock = createBlock(&_if, PredicateType::FunctionBlock, "if_header_");
-	auto trueBlock = createBlock(&_if.trueStatement(), "if_true_");
+	auto trueBlock = createBlock(&_if.trueStatement(), PredicateType::FunctionBlock, "if_true_");
-	auto falseBlock = _if.falseStatement() ? createBlock(_if.falseStatement(), "if_false_") : nullptr;
+	auto falseBlock = _if.falseStatement() ? createBlock(_if.falseStatement(), PredicateType::FunctionBlock, "if_false_") : nullptr;
-	auto afterIfBlock = createBlock(&functionBody);
+	auto afterIfBlock = createBlock(&functionBody, PredicateType::FunctionBlock);
 
 	connectBlocks(m_currentBlock, predicate(*ifHeaderBlock));
 
@@ -305,9 +303,9 @@ bool CHC::visit(WhileStatement const& _while)
 	auto const& functionBody = m_currentFunction->body();
 
 	auto namePrefix = string(_while.isDoWhile() ? "do_" : "") + "while";
-	auto loopHeaderBlock = createBlock(&_while, namePrefix + "_header_");
+	auto loopHeaderBlock = createBlock(&_while, PredicateType::FunctionBlock, namePrefix + "_header_");
-	auto loopBodyBlock = createBlock(&_while.body(), namePrefix + "_body_");
+	auto loopBodyBlock = createBlock(&_while.body(), PredicateType::FunctionBlock, namePrefix + "_body_");
-	auto afterLoopBlock = createBlock(&functionBody);
+	auto afterLoopBlock = createBlock(&functionBody, PredicateType::FunctionBlock);
 
 	auto outerBreakDest = m_breakDest;
 	auto outerContinueDest = m_continueDest;
@@ -354,11 +352,11 @@ bool CHC::visit(ForStatement const& _for)
 	solAssert(m_currentFunction, "");
 	auto const& functionBody = m_currentFunction->body();
 
-	auto loopHeaderBlock = createBlock(&_for, "for_header_");
+	auto loopHeaderBlock = createBlock(&_for, PredicateType::FunctionBlock, "for_header_");
-	auto loopBodyBlock = createBlock(&_for.body(), "for_body_");
+	auto loopBodyBlock = createBlock(&_for.body(), PredicateType::FunctionBlock, "for_body_");
-	auto afterLoopBlock = createBlock(&functionBody);
+	auto afterLoopBlock = createBlock(&functionBody, PredicateType::FunctionBlock);
 	auto postLoop = _for.loopExpression();
-	auto postLoopBlock = postLoop ? createBlock(postLoop, "for_post_") : nullptr;
+	auto postLoopBlock = postLoop ? createBlock(postLoop, PredicateType::FunctionBlock, "for_post_") : nullptr;
 
 	auto outerBreakDest = m_breakDest;
 	auto outerContinueDest = m_continueDest;
@@ -460,7 +458,7 @@ void CHC::endVisit(Break const& _break)
 {
 	solAssert(m_breakDest, "");
 	connectBlocks(m_currentBlock, predicate(*m_breakDest));
-	auto breakGhost = createBlock(&_break, "break_ghost_");
+	auto breakGhost = createBlock(&_break, PredicateType::FunctionBlock, "break_ghost_");
 	m_currentBlock = predicate(*breakGhost);
 }
 
@@ -468,7 +466,7 @@ void CHC::endVisit(Continue const& _continue)
 {
 	solAssert(m_continueDest, "");
 	connectBlocks(m_currentBlock, predicate(*m_continueDest));
-	auto continueGhost = createBlock(&_continue, "continue_ghost_");
+	auto continueGhost = createBlock(&_continue, PredicateType::FunctionBlock, "continue_ghost_");
 	m_currentBlock = predicate(*continueGhost);
 }
 
@@ -485,18 +483,36 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 	else
 		m_functionAssertions[m_currentFunction].insert(&_funCall);
 
-	auto previousError = m_error.currentValue();
+	auto previousError = errorFlag().currentValue();
-	m_error.increaseIndex();
+	errorFlag().increaseIndex();
 
 	connectBlocks(
 		m_currentBlock,
 		m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction),
 		currentPathConditions() && !m_context.expression(*args.front())->currentValue() && (
-			m_error.currentValue() == newErrorId(_funCall)
+			errorFlag().currentValue() == newErrorId(_funCall)
 		)
 	);
 
-	m_context.addAssertion(m_error.currentValue() == previousError);
+	m_context.addAssertion(errorFlag().currentValue() == previousError);
+}
+
+void CHC::visitAddMulMod(FunctionCall const& _funCall)
+{
+	auto previousError = errorFlag().currentValue();
+	errorFlag().increaseIndex();
+
+	addVerificationTarget(
+		&_funCall,
+		VerificationTarget::Type::DivByZero,
+		errorFlag().currentValue()
+	);
+
+	solAssert(_funCall.arguments().at(2), "");
+	smtutil::Expression target = expr(*_funCall.arguments().at(2)) == 0 && errorFlag().currentValue() == newErrorId(_funCall);
+	m_context.addAssertion((errorFlag().currentValue() == previousError) || target);
+
+	SMTEncoder::visitAddMulMod(_funCall);
 }
 
 void CHC::internalFunctionCall(FunctionCall const& _funCall)
@@ -518,22 +534,26 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 			m_context.addAssertion(interface(*contract));
 	}
 
-	auto previousError = m_error.currentValue();
+	auto previousError = errorFlag().currentValue();
 
 	m_context.addAssertion(predicate(_funCall));
 
 	connectBlocks(
 		m_currentBlock,
 		(m_currentFunction && !m_currentFunction->isConstructor()) ? summary(*m_currentFunction) : summary(*m_currentContract),
-		(m_error.currentValue() > 0)
+		(errorFlag().currentValue() > 0)
 	);
-	m_context.addAssertion(m_error.currentValue() == 0);
+	m_context.addAssertion(errorFlag().currentValue() == 0);
-	m_error.increaseIndex();
+	errorFlag().increaseIndex();
-	m_context.addAssertion(m_error.currentValue() == previousError);
+	m_context.addAssertion(errorFlag().currentValue() == previousError);
 }
 
 void CHC::externalFunctionCall(FunctionCall const& _funCall)
 {
+	/// In external function calls we do not add a "predicate call"
+	/// because we do not trust their function body anyway,
+	/// so we just add the nondet_interface predicate.
+
 	solAssert(m_currentContract, "");
 
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
@@ -558,7 +578,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables());
 	m_context.addAssertion(nondet);
 
-	m_context.addAssertion(m_error.currentValue() == 0);
+	m_context.addAssertion(errorFlag().currentValue() == 0);
 }
 
 void CHC::unknownFunctionCall(FunctionCall const&)
@@ -583,13 +603,13 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
 	auto symbArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
 	solAssert(symbArray, "");
 
-	auto previousError = m_error.currentValue();
+	auto previousError = errorFlag().currentValue();
-	m_error.increaseIndex();
+	errorFlag().increaseIndex();
 
-	addVerificationTarget(&_arrayPop, VerificationTarget::Type::PopEmptyArray, m_error.currentValue());
+	addVerificationTarget(&_arrayPop, VerificationTarget::Type::PopEmptyArray, errorFlag().currentValue());
 
-	smtutil::Expression target = (symbArray->length() <= 0) && (m_error.currentValue() == newErrorId(_arrayPop));
+	smtutil::Expression target = (symbArray->length() <= 0) && (errorFlag().currentValue() == newErrorId(_arrayPop));
-	m_context.addAssertion((m_error.currentValue() == previousError) || target);
+	m_context.addAssertion((errorFlag().currentValue() == previousError) || target);
 }
 
 pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
@@ -613,8 +633,8 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 	if (_op == Token::Mod || (_op == Token::Div && !intType->isSigned()))
 		return values;
 
-	auto previousError = m_error.currentValue();
+	auto previousError = errorFlag().currentValue();
-	m_error.increaseIndex();
+	errorFlag().increaseIndex();
 
 	VerificationTarget::Type targetType;
 	unsigned errorId = newErrorId(_expression);
@@ -623,24 +643,24 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 	if (_op == Token::Div)
 	{
 		targetType = VerificationTarget::Type::Overflow;
-		target = values.second > intType->maxValue() && m_error.currentValue() == errorId;
+		target = values.second > intType->maxValue() && errorFlag().currentValue() == errorId;
 	}
 	else if (intType->isSigned())
 	{
 		unsigned secondErrorId = newErrorId(_expression);
 		targetType = VerificationTarget::Type::UnderOverflow;
-		target = (values.second < intType->minValue() && m_error.currentValue() == errorId) ||
+		target = (values.second < intType->minValue() && errorFlag().currentValue() == errorId) ||
-			(values.second > intType->maxValue() && m_error.currentValue() == secondErrorId);
+			(values.second > intType->maxValue() && errorFlag().currentValue() == secondErrorId);
 	}
 	else if (_op == Token::Sub)
 	{
 		targetType = VerificationTarget::Type::Underflow;
-		target = values.second < intType->minValue() && m_error.currentValue() == errorId;
+		target = values.second < intType->minValue() && errorFlag().currentValue() == errorId;
 	}
 	else if (_op == Token::Add || _op == Token::Mul)
 	{
 		targetType = VerificationTarget::Type::Overflow;
-		target = values.second > intType->maxValue() && m_error.currentValue() == errorId;
+		target = values.second > intType->maxValue() && errorFlag().currentValue() == errorId;
 	}
 	else
 		solAssert(false, "");
@@ -648,10 +668,10 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 	addVerificationTarget(
 		&_expression,
 		targetType,
-		m_error.currentValue()
+		errorFlag().currentValue()
 	);
 
-	m_context.addAssertion((m_error.currentValue() == previousError) || *target);
+	m_context.addAssertion((errorFlag().currentValue() == previousError) || *target);
 
 	return values;
 }
@@ -700,7 +720,7 @@ void CHC::resetContractAnalysis()
 	m_unknownFunctionCallSeen = false;
 	m_breakDest = nullptr;
 	m_continueDest = nullptr;
-	m_error.resetIndex();
+	errorFlag().resetIndex();
 }
 
 void CHC::eraseKnowledge()
@@ -725,20 +745,14 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
 	}
 }
 
-void CHC::setCurrentBlock(
+void CHC::setCurrentBlock(Predicate const& _block)
-	Predicate const& _block,
-	vector<smtutil::Expression> const* _arguments
-)
 {
 	if (m_context.solverStackHeigh() > 0)
 		m_context.popSolver();
 	solAssert(m_currentContract, "");
 	clearIndices(m_currentContract, m_currentFunction);
 	m_context.pushSolver();
-	if (_arguments)
+	m_currentBlock = predicate(_block);
-		m_currentBlock = predicate(_block, *_arguments);
-	else
-		m_currentBlock = predicate(_block);
 }
 
 set<frontend::Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTNode const* _txRoot)
@@ -766,9 +780,9 @@ SortPointer CHC::sort(ASTNode const* _node)
 	return functionBodySort(*m_currentFunction, m_currentContract);
 }
 
-Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, ASTNode const* _node)
+Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node)
 {
-	auto const* block = Predicate::create(_sort, _name, m_context, _node);
+	auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node);
 	m_interface->registerRelation(block->functor());
 	return block;
 }
@@ -779,8 +793,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 		if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
 		{
 			string suffix = contract->name() + "_" + to_string(contract->id());
-			m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract), "interface_" + suffix);
+			m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract), "interface_" + suffix, PredicateType::Interface, contract);
-			m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract), "nondet_interface_" + suffix);
+			m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract), "nondet_interface_" + suffix, PredicateType::NondetInterface, contract);
 
 			for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*contract))
 				if (!m_context.knownVariable(*var))
@@ -818,7 +832,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 						auto nondetPre = iface(state0 + state1);
 						auto nondetPost = iface(state0 + state2);
 
-						vector<smtutil::Expression> args{m_error.currentValue()};
+						vector<smtutil::Expression> args{errorFlag().currentValue()};
 						args += state1 +
 							applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
 							state2 +
@@ -833,16 +847,13 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 
 smtutil::Expression CHC::interface()
 {
-	auto paramExprs = applyMap(
+	solAssert(m_currentContract, "");
-		m_stateVariables,
+	return interface(*m_currentContract);
-		[this](auto _var) { return m_context.variable(*_var)->currentValue(); }
-	);
-	return (*m_interfaces.at(m_currentContract))(paramExprs);
 }
 
 smtutil::Expression CHC::interface(ContractDefinition const& _contract)
 {
-	return (*m_interfaces.at(&_contract))(stateVariablesAtIndex(0, _contract));
+	return ::interface(*m_interfaces.at(&_contract), _contract, m_context);
 }
 
 smtutil::Expression CHC::error()
@@ -857,27 +868,12 @@ smtutil::Expression CHC::error(unsigned _idx)
 
 smtutil::Expression CHC::summary(ContractDefinition const& _contract)
 {
-	if (auto const* constructor = _contract.constructor())
+	return constructor(*m_constructorSummaryPredicate, _contract, m_context);
-		return (*m_constructorSummaryPredicate)(
-			currentFunctionVariables(*constructor)
-		);
-
-	return (*m_constructorSummaryPredicate)(
-		vector<smtutil::Expression>{m_error.currentValue()} +
-		currentStateVariables()
-	);
 }
 
 smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDefinition const& _contract)
 {
-	vector<smtutil::Expression> args{m_error.currentValue()};
+	return smt::function(*m_summaries.at(&_contract).at(&_function), _function, &_contract, m_context);
-	auto contract = _function.annotation().contract;
-	args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables(_contract);
-	args += applyMap(_function.parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); });
-	args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables(_contract);
-	args += applyMap(_function.parameters(), [this](auto _var) { return currentValue(*_var); });
-	args += applyMap(_function.returnParameters(), [this](auto _var) { return currentValue(*_var); });
-	return (*m_summaries.at(&_contract).at(&_function))(args);
 }
 
 smtutil::Expression CHC::summary(FunctionDefinition const& _function)
@@ -886,11 +882,12 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function)
 	return summary(_function, *m_currentContract);
 }
 
-Predicate const* CHC::createBlock(ASTNode const* _node, string const& _prefix)
+Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType, string const& _prefix)
 {
 	auto block = createSymbolicBlock(
 		sort(_node),
 		"block_" + uniquePrefix() + "_" + _prefix + predicateName(_node),
+		_predType,
 		_node
 	);
 
@@ -903,6 +900,7 @@ Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, Co
 	auto block = createSymbolicBlock(
 		functionSort(_function, &_contract),
 		"summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract),
+		PredicateType::FunctionSummary,
 		&_function
 	);
 
@@ -911,7 +909,7 @@ Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, Co
 
 void CHC::createErrorBlock()
 {
-	m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_target_" + to_string(m_context.newUniqueId()));
+	m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_target_" + to_string(m_context.newUniqueId()), PredicateType::Error);
 	m_interface->registerRelation(m_errorPredicate->functor());
 }
 
@@ -929,11 +927,6 @@ vector<smtutil::Expression> CHC::initialStateVariables()
 	return stateVariablesAtIndex(0);
 }
 
-vector<smtutil::Expression> CHC::initialStateVariables(ContractDefinition const& _contract)
-{
-	return stateVariablesAtIndex(0, _contract);
-}
-
 vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index)
 {
 	solAssert(m_currentContract, "");
@@ -959,46 +952,6 @@ vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const&
 	return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
 }
 
-vector<smtutil::Expression> CHC::currentFunctionVariables()
-{
-	solAssert(m_currentFunction, "");
-	return currentFunctionVariables(*m_currentFunction);
-}
-
-vector<smtutil::Expression> CHC::currentFunctionVariables(FunctionDefinition const& _function)
-{
-	vector<smtutil::Expression> initInputExprs;
-	vector<smtutil::Expression> mutableInputExprs;
-	for (auto const& var: _function.parameters())
-	{
-		initInputExprs.push_back(m_context.variable(*var)->valueAtIndex(0));
-		mutableInputExprs.push_back(m_context.variable(*var)->currentValue());
-	}
-	auto returnExprs = applyMap(_function.returnParameters(), [this](auto _var) { return currentValue(*_var); });
-	return vector<smtutil::Expression>{m_error.currentValue()} +
-		initialStateVariables() +
-		initInputExprs +
-		currentStateVariables() +
-		mutableInputExprs +
-		returnExprs;
-}
-
-vector<smtutil::Expression> CHC::currentFunctionVariables(ContractDefinition const& _contract)
-{
-	if (auto const* constructor = _contract.constructor())
-		return currentFunctionVariables(*constructor);
-
-	return vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables();
-}
-
-vector<smtutil::Expression> CHC::currentBlockVariables()
-{
-	if (m_currentFunction)
-		return currentFunctionVariables() + applyMap(m_currentFunction->localVariables(), [this](auto _var) { return currentValue(*_var); });
-
-	return currentFunctionVariables();
-}
-
 string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contract)
 {
 	string prefix;
@@ -1018,37 +971,64 @@ string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contr
 
 smtutil::Expression CHC::predicate(Predicate const& _block)
 {
-	return _block(currentBlockVariables());
+	switch (_block.type())
-}
+	{
-
+	case PredicateType::Interface:
-smtutil::Expression CHC::predicate(
+		solAssert(m_currentContract, "");
-	Predicate const& _block,
+		return ::interface(_block, *m_currentContract, m_context);
-	vector<smtutil::Expression> const& _arguments
+	case PredicateType::ImplicitConstructor:
-)
+		solAssert(m_currentContract, "");
-{
+		return implicitConstructor(_block, *m_currentContract, m_context);
-	return _block(_arguments);
+	case PredicateType::ConstructorSummary:
+		solAssert(m_currentContract, "");
+		return constructor(_block, *m_currentContract, m_context);
+	case PredicateType::FunctionEntry:
+	case PredicateType::FunctionSummary:
+		solAssert(m_currentFunction, "");
+		return smt::function(_block, *m_currentFunction, m_currentContract, m_context);
+	case PredicateType::FunctionBlock:
+		solAssert(m_currentFunction, "");
+		return functionBlock(_block, *m_currentFunction, m_currentContract, m_context);
+	case PredicateType::Error:
+		return _block({});
+	case PredicateType::NondetInterface:
+		// Nondeterministic interface predicates are handled differently.
+		solAssert(false, "");
+	}
+	solAssert(false, "");
 }
 
 smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 {
+	/// Used only for internal calls.
+
 	auto const* function = functionCallToDefinition(_funCall);
 	if (!function)
 		return smtutil::Expression(true);
 
-	m_error.increaseIndex();
+	errorFlag().increaseIndex();
-	vector<smtutil::Expression> args{m_error.currentValue()};
+	vector<smtutil::Expression> args{errorFlag().currentValue()};
-	auto const* contract = function->annotation().contract;
-	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
-	bool otherContract = contract->isLibrary() ||
-		funType.kind() == FunctionType::Kind::External ||
-		funType.kind() == FunctionType::Kind::BareStaticCall;
 
-	args += otherContract ? stateVariablesAtIndex(0, *contract) : currentStateVariables();
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	solAssert(funType.kind() == FunctionType::Kind::Internal, "");
+
+	/// Internal calls can be made to the contract itself or a library.
+	auto const* contract = function->annotation().contract;
+	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
+	solAssert(contract->isLibrary() || find(hierarchy.begin(), hierarchy.end(), contract) != hierarchy.end(), "");
+
+	/// If the call is to a library, we use that library as the called contract.
+	/// If it is not, we use the current contract even if it is a call to a contract
+	/// up in the inheritance hierarchy, since the interfaces/predicates are different.
+	auto const* calledContract = contract->isLibrary() ? contract : m_currentContract;
+	solAssert(calledContract, "");
+
+	args += currentStateVariables(*calledContract);
 	args += symbolicArguments(_funCall);
-	if (!otherContract)
+	if (!calledContract->isLibrary())
 		for (auto const& var: m_stateVariables)
 			m_context.variable(*var)->increaseIndex();
-	args += otherContract ? stateVariablesAtIndex(1, *contract) : currentStateVariables();
+	args += currentStateVariables(*calledContract);
 
 	for (auto var: function->parameters() + function->returnParameters())
 	{
@@ -1059,11 +1039,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 		args.push_back(currentValue(*var));
 	}
 
-	if (otherContract)
+	return (*m_summaries.at(calledContract).at(function))(args);
-		return (*m_summaries.at(contract).at(function))(args);
-
-	solAssert(m_currentContract, "");
-	return (*m_summaries.at(m_currentContract).at(function))(args);
 }
 
 void CHC::addRule(smtutil::Expression const& _rule, string const& _ruleName)
@@ -1200,6 +1176,11 @@ void CHC::checkVerificationTargets()
 					errorReporterId = overflowErrorId;
 				}
 			}
+			else if (target.type == VerificationTarget::Type::DivByZero)
+			{
+				satMsg = "Division by zero happens here.";
+				errorReporterId = 4281_error;
+			}
 			else
 				solAssert(false, "");
 
@@ -1427,3 +1408,8 @@ unsigned CHC::newErrorId(frontend::Expression const& _expr)
 	m_errorIds.emplace(_expr.id(), errorId);
 	return errorId;
 }
+
+SymbolicIntVariable& CHC::errorFlag()
+{
+	return m_context.state().errorFlag();
+}

libsolidity/formal/CHC.h

@@ -83,6 +83,7 @@ private:
 	void endVisit(Continue const& _node) override;
 
 	void visitAssert(FunctionCall const& _funCall);
+	void visitAddMulMod(FunctionCall const& _funCall) override;
 	void internalFunctionCall(FunctionCall const& _funCall);
 	void externalFunctionCall(FunctionCall const& _funCall);
 	void unknownFunctionCall(FunctionCall const& _funCall);
@@ -111,7 +112,7 @@ private:
 	void resetContractAnalysis();
 	void eraseKnowledge();
 	void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
-	void setCurrentBlock(Predicate const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr);
+	void setCurrentBlock(Predicate const& _block);
 	std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
 	//@}
 
@@ -124,7 +125,7 @@ private:
 	/// Predicate helpers.
 	//@{
 	/// @returns a new block of given _sort and _name.
-	Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, ASTNode const* _node = nullptr);
+	Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, PredicateType _predType, ASTNode const* _node = nullptr);
 
 	/// Creates summary predicates for all functions of all contracts
 	/// in a given _source.
@@ -138,7 +139,7 @@ private:
 	smtutil::Expression error(unsigned _idx);
 
 	/// Creates a block for the given _node.
-	Predicate const* createBlock(ASTNode const* _node, std::string const& _prefix = "");
+	Predicate const* createBlock(ASTNode const* _node, PredicateType _predType, std::string const& _prefix = "");
 	/// Creates a call block for the given function _function from contract _contract.
 	/// The contract is needed here because of inheritance.
 	Predicate const* createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract);
@@ -152,29 +153,16 @@ private:
 	/// @returns the symbolic values of the state variables at the beginning
 	/// of the current transaction.
 	std::vector<smtutil::Expression> initialStateVariables();
-	std::vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract);
 	std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index);
 	std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract);
 	/// @returns the current symbolic values of the current state variables.
 	std::vector<smtutil::Expression> currentStateVariables();
 	std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract);
 
-	/// @returns the current symbolic values of the current function's
-	/// input and output parameters.
-	std::vector<smtutil::Expression> currentFunctionVariables();
-	std::vector<smtutil::Expression> currentFunctionVariables(FunctionDefinition const& _function);
-	std::vector<smtutil::Expression> currentFunctionVariables(ContractDefinition const& _contract);
-
-	/// @returns the same as currentFunctionVariables plus
-	/// local variables.
-	std::vector<smtutil::Expression> currentBlockVariables();
-
 	/// @returns the predicate name for a given node.
 	std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr);
-	/// @returns a predicate application over the current scoped variables.
+	/// @returns a predicate application after checking the predicate's type.
 	smtutil::Expression predicate(Predicate const& _block);
-	/// @returns a predicate application over @param _arguments.
-	smtutil::Expression predicate(Predicate const& _block, std::vector<smtutil::Expression> const& _arguments);
 	/// @returns the summary predicate for the called function.
 	smtutil::Expression predicate(FunctionCall const& _funCall);
 	/// @returns a predicate that defines a constructor summary.
@@ -245,6 +233,8 @@ private:
 	/// @returns a new unique error id associated with _expr and stores
 	/// it into m_errorIds.
 	unsigned newErrorId(Expression const& _expr);
+
+	smt::SymbolicIntVariable& errorFlag();
 	//@}
 
 	/// Predicates.
@@ -269,13 +259,6 @@ private:
 
 	/// Function predicates.
 	std::map<ContractDefinition const*, std::map<FunctionDefinition const*, Predicate const*>> m_summaries;
-
-	smt::SymbolicIntVariable m_error{
-		TypeProvider::uint256(),
-		TypeProvider::uint256(),
-		"error",
-		m_context
-	};
 	//@}
 
 	/// Variables.

libsolidity/formal/Predicate.cpp

@@ -36,6 +36,7 @@ map<string, Predicate> Predicate::m_predicates;
 Predicate const* Predicate::create(
 	SortPointer _sort,
 	string _name,
+	PredicateType _type,
 	EncodingContext& _context,
 	ASTNode const* _node
 )
@@ -46,15 +47,17 @@ Predicate const* Predicate::create(
 	return &m_predicates.emplace(
 		std::piecewise_construct,
 		std::forward_as_tuple(functorName),
-		std::forward_as_tuple(move(predicate), _node)
+		std::forward_as_tuple(move(predicate), _type, _node)
 	).first->second;
 }
 
 Predicate::Predicate(
 	smt::SymbolicFunctionVariable&& _predicate,
+	PredicateType _type,
 	ASTNode const* _node
 ):
 	m_predicate(move(_predicate)),
+	m_type(_type),
 	m_node(_node)
 {
 }

libsolidity/formal/Predicate.h

@@ -30,6 +30,18 @@
 namespace solidity::frontend
 {
 
+enum class PredicateType
+{
+	Interface,
+	NondetInterface,
+	ImplicitConstructor,
+	ConstructorSummary,
+	FunctionEntry,
+	FunctionSummary,
+	FunctionBlock,
+	Error
+};
+
 /**
  * Represents a predicate used by the CHC engine.
  */
@@ -39,12 +51,14 @@ public:
 	static Predicate const* create(
 		smtutil::SortPointer _sort,
 		std::string _name,
+		PredicateType _type,
 		smt::EncodingContext& _context,
 		ASTNode const* _node = nullptr
 	);
 
 	Predicate(
 		smt::SymbolicFunctionVariable&& _predicate,
+		PredicateType _type,
 		ASTNode const* _node = nullptr
 	);
 
@@ -88,6 +102,8 @@ public:
 	/// @returns true if this predicate represents an interface.
 	bool isInterface() const;
 
+	PredicateType type() const { return m_type; }
+
 	/// @returns a formatted string representing a call to this predicate
 	/// with _args.
 	std::string formatSummaryCall(std::vector<std::string> const& _args) const;
@@ -108,6 +124,9 @@ private:
 	/// The actual SMT expression.
 	smt::SymbolicFunctionVariable m_predicate;
 
+	/// The type of this predicate.
+	PredicateType m_type;
+
 	/// The ASTNode that this predicate represents.
 	/// nullptr if this predicate is not associated with a specific program AST node.
 	ASTNode const* m_node = nullptr;

libsolidity/formal/PredicateInstance.cpp

@@ -0,0 +1,120 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolidity/formal/PredicateInstance.h>
+
+#include <libsolidity/formal/EncodingContext.h>
+#include <libsolidity/formal/SMTEncoder.h>
+
+using namespace std;
+using namespace solidity::util;
+using namespace solidity::smtutil;
+
+namespace solidity::frontend::smt
+{
+
+smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
+{
+	return _pred(currentStateVariables(_contract, _context));
+}
+
+smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
+{
+	if (auto const* constructor = _contract.constructor())
+		return _pred(currentFunctionVariables(*constructor, &_contract, _context));
+
+	return _pred(
+		vector<smtutil::Expression>{_context.state().errorFlag().currentValue()} +
+		currentStateVariables(_contract, _context)
+	);
+}
+
+/// Currently it does not have arguments but it will have tx data in the future.
+smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext&)
+{
+	return _pred({});
+}
+
+smtutil::Expression function(
+	Predicate const& _pred,
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+)
+{
+	return _pred(currentFunctionVariables(_function, _contract, _context));
+}
+
+smtutil::Expression functionBlock(
+	Predicate const& _pred,
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+)
+{
+	return _pred(currentBlockVariables(_function, _contract, _context));
+}
+
+/// Helpers
+
+vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract, EncodingContext& _context)
+{
+	return stateVariablesAtIndex(0, _contract, _context);
+}
+
+vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract, EncodingContext& _context)
+{
+	return applyMap(
+		SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
+		[&](auto _var) { return _context.variable(*_var)->valueAtIndex(_index); }
+	);
+}
+
+vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract, EncodingContext& _context)
+{
+	return applyMap(
+		SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
+		[&](auto _var) { return _context.variable(*_var)->currentValue(); }
+	);
+}
+
+vector<smtutil::Expression> currentFunctionVariables(
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+)
+{
+	vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue()};
+	exprs += _contract ? initialStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
+	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
+	exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
+	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
+	exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
+	return exprs;
+}
+
+vector<smtutil::Expression> currentBlockVariables(FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context)
+{
+	return currentFunctionVariables(_function, _contract, _context) +
+		applyMap(
+			_function.localVariables(),
+			[&](auto _var) { return _context.variable(*_var)->currentValue(); }
+		);
+}
+
+}

libsolidity/formal/PredicateInstance.h

@@ -0,0 +1,73 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <libsolidity/formal/Predicate.h>
+
+namespace solidity::frontend::smt
+{
+
+class EncodingContext;
+
+/**
+ * This file represents the specification for building CHC predicate instances.
+ * The predicates follow the specification in PredicateSort.h.
+ * */
+
+smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
+
+smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
+
+smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
+
+smtutil::Expression function(
+	Predicate const& _pred,
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+);
+
+smtutil::Expression functionBlock(
+	Predicate const& _pred,
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+);
+
+/// Helpers
+
+std::vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract, EncodingContext& _context);
+
+std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract, EncodingContext& _context);
+
+std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract, EncodingContext& _context);
+
+std::vector<smtutil::Expression> currentFunctionVariables(
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+);
+
+std::vector<smtutil::Expression> currentBlockVariables(
+	FunctionDefinition const& _function,
+	ContractDefinition const* _contract,
+	EncodingContext& _context
+);
+
+}

libsolidity/formal/SMTEncoder.cpp

@@ -632,8 +632,10 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::SHA256:
 	case FunctionType::Kind::RIPEMD160:
 	case FunctionType::Kind::BlockHash:
+		break;
 	case FunctionType::Kind::AddMod:
 	case FunctionType::Kind::MulMod:
+		visitAddMulMod(_funCall);
 		break;
 	case FunctionType::Kind::Send:
 	case FunctionType::Kind::Transfer:
@@ -738,6 +740,24 @@ void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
 		m_context.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
 
+void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall)
+{
+	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	auto kind = funType.kind();
+	solAssert(kind == FunctionType::Kind::AddMod || kind == FunctionType::Kind::MulMod, "");
+	auto const& args = _funCall.arguments();
+	solAssert(args.at(0) && args.at(1) && args.at(2), "");
+	auto x = expr(*args.at(0));
+	auto y = expr(*args.at(1));
+	auto k = expr(*args.at(2));
+	m_context.addAssertion(k != 0);
+
+	if (kind == FunctionType::Kind::AddMod)
+		defineExpr(_funCall, (x + y) % k);
+	else
+		defineExpr(_funCall, (x * y) % k);
+}
+
 void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
 {
 	auto const& args = _funCall.arguments();

libsolidity/formal/SMTEncoder.h

@@ -137,6 +137,7 @@ protected:
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);
 	void visitGasLeft(FunctionCall const& _funCall);
+	virtual void visitAddMulMod(FunctionCall const& _funCall);
 	void visitObjectCreation(FunctionCall const& _funCall);
 	void visitTypeConversion(FunctionCall const& _funCall);
 	void visitFunctionIdentifier(Identifier const& _identifier);

libsolidity/formal/SymbolicState.cpp

@@ -33,6 +33,7 @@ void SymbolicState::reset()
 {
 	m_thisAddress.resetIndex();
 	m_balances.resetIndex();
+	m_error.resetIndex();
 }
 
 // Blockchain
@@ -52,6 +53,11 @@ smtutil::Expression SymbolicState::balance(smtutil::Expression _address)
 	return smtutil::Expression::select(m_balances.elements(), move(_address));
 }
 
+SymbolicIntVariable& SymbolicState::errorFlag()
+{
+	return m_error;
+}
+
 void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
 {
 	unsigned indexBefore = m_balances.index();

libsolidity/formal/SymbolicState.h

@@ -46,6 +46,9 @@ public:
 	smtutil::Expression balance();
 	/// @returns the symbolic balance of an address.
 	smtutil::Expression balance(smtutil::Expression _address);
+
+	SymbolicIntVariable& errorFlag();
+
 	/// Transfer _value from _from to _to.
 	void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value);
 	//@}
@@ -68,6 +71,13 @@ private:
 		"balances",
 		m_context
 	};
+
+	smt::SymbolicIntVariable m_error{
+		TypeProvider::uint256(),
+		TypeProvider::uint256(),
+		"error",
+		m_context
+	};
 };
 
 }

libsolutil/CMakeLists.txt

@@ -20,6 +20,7 @@ set(sources
 	Keccak256.cpp
 	Keccak256.h
 	LazyInit.h
+	LEB128.h
 	picosha2.h
 	Result.h
 	SetOnce.h

libsolutil/LEB128.h

@@ -0,0 +1,59 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+#pragma once
+
+
+#include <libsolutil/Common.h>
+
+namespace solidity::util
+{
+
+inline bytes lebEncode(uint64_t _n)
+{
+	bytes encoded;
+	while (_n > 0x7f)
+	{
+		encoded.emplace_back(uint8_t(0x80 | (_n & 0x7f)));
+		_n >>= 7;
+	}
+	encoded.emplace_back(_n);
+	return encoded;
+}
+
+// signed right shift is an arithmetic right shift
+static_assert((-1 >> 1) == -1, "Arithmetic shift not supported.");
+
+inline bytes lebEncodeSigned(int64_t _n)
+{
+	// Based on https://github.com/llvm/llvm-project/blob/master/llvm/include/llvm/Support/LEB128.h
+	bytes result;
+	bool more;
+	do
+	{
+		uint8_t v = _n & 0x7f;
+		_n >>= 7;
+		more = !((((_n == 0) && ((v & 0x40) == 0)) || ((_n == -1) && ((v & 0x40) != 0))));
+		if (more)
+			v |= 0x80; // Mark this byte to show that more bytes will follow.
+		result.emplace_back(v);
+	}
+	while (more);
+	return result;
+}
+
+}

libyul/backends/wasm/BinaryTransform.cpp

@@ -24,6 +24,7 @@
 #include <libyul/Exceptions.h>
 #include <libsolutil/CommonData.h>
 #include <libsolutil/Visitor.h>
+#include <libsolutil/LEB128.h>
 
 #include <boost/range/adaptor/reversed.hpp>
 #include <boost/range/adaptor/map.hpp>
@@ -239,28 +240,6 @@ static map<string, uint8_t> const builtins = {
 	{"i64.extend_i32_u", 0xad},
 };
 
-bytes lebEncode(uint64_t _n)
-{
-	bytes encoded;
-	while (_n > 0x7f)
-	{
-		encoded.emplace_back(uint8_t(0x80 | (_n & 0x7f)));
-		_n >>= 7;
-	}
-	encoded.emplace_back(_n);
-	return encoded;
-}
-
-bytes lebEncodeSigned(int64_t _n)
-{
-	if (_n >= 0 && _n < 0x40)
-		return toBytes(uint8_t(uint64_t(_n) & 0xff));
-	else if (-_n > 0 && -_n < 0x40)
-		return toBytes(uint8_t(uint64_t(_n + 0x80) & 0xff));
-	else
-		return toBytes(uint8_t(0x80 | uint8_t(_n & 0x7f))) + lebEncodeSigned(_n / 0x80);
-}
-
 bytes prefixSize(bytes _data)
 {
 	size_t size = _data.size();

scripts/error_codes.py

@@ -223,7 +223,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
         "1123", "1133", "1220", "1584", "1823", "1950",
         "1988", "2418", "2461", "2512", "2592", "2657", "2800", "2842", "2856",
         "3263", "3356", "3441", "3682", "3876",
-        "3893", "3997", "4010", "4802", "4805", "4828",
+        "3893", "3997", "4010", "4281", "4802", "4805", "4828",
         "4904", "4990", "5052", "5073", "5170", "5188", "5272", "5333", "5347", "5473",
         "5622", "6041", "6052", "6272", "6708", "6792", "6931", "7110", "7128", "7186",
         "7589", "7593", "7653", "7812", "7885", "8065", "8084", "8140",

test/CMakeLists.txt

@@ -35,6 +35,7 @@ set(libsolutil_sources
     libsolutil/JSON.cpp
     libsolutil/Keccak256.cpp
     libsolutil/LazyInit.cpp
+    libsolutil/LEB128.cpp
     libsolutil/StringUtils.cpp
     libsolutil/SwarmHash.cpp
     libsolutil/UTF8.cpp

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol

@@ -14,13 +14,11 @@ contract LoopFor2 {
 			c[i] = b[i];
 			++i;
 		}
-		// Fails as false positive.
 		assert(b[0] == c[0]);
 		assert(a[0] == 900);
 		assert(b[0] == 900);
 	}
 }
 // ----
-// Warning 6328: (320-339): CHC: Assertion violation happens here.
+// Warning 6328: (290-309): CHC: Assertion violation happens here.
-// Warning 6328: (343-362): CHC: Assertion violation happens here.
+// Warning 6328: (313-332): CHC: Assertion violation happens here.
-// Warning 4661: (296-316): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/math/addmod_1.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		assert(addmod(2**256 - 1, 10, 9) == 7);
+		uint y = 0;
+		uint x = addmod(2**256 - 1, 10, y);
+		assert(x == 1);
+	}
+	function g(uint x, uint y, uint k) public pure returns (uint) {
+		return addmod(x, y, k);
+	}
+}
+// ----
+// Warning 1218: (83-108): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (141-166): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (76-114): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (170-184): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (263-278): CHC: Error trying to invoke SMT solver.
+// Warning 3046: (141-166): BMC: Division by zero happens here.
+// Warning 3046: (263-278): BMC: Division by zero happens here.

test/libsolidity/smtCheckerTests/math/addmod_mulmod.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function test() public pure {
+		uint x;
+		if ((2**255 + 2**255) % 7 != addmod(2**255, 2**255, 7)) x = 1;
+		if ((2**255 + 2**255) % 7 != addmod(2**255, 2**255, 7)) x = 2;
+		assert(x == 0);
+	}
+}
+// ----
+// Warning 1218: (118-143): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (183-208): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (219-233): CHC: Error trying to invoke SMT solver.
+// Warning 6838: (93-143): BMC: Condition is always false.
+// Warning 6838: (158-208): BMC: Condition is always false.

test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol

@@ -0,0 +1,35 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(uint256 d) public pure {
+		uint x = addmod(1, 2, d);
+		assert(x < d);
+	}
+
+	function g(uint256 d) public pure {
+		uint x = mulmod(1, 2, d);
+		assert(x < d);
+	}
+
+	function h() public pure returns (uint256) {
+		uint x = mulmod(0, 1, 2);
+		uint y = mulmod(1, 0, 2);
+		assert(x == y);
+		uint z = addmod(0, 1, 2);
+		uint t = addmod(1, 0, 2);
+		assert(z == t);
+	}
+}
+// ----
+// Warning 1218: (94-109): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (113-126): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (180-195): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (199-212): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (275-290): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (303-318): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (349-364): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (377-392): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (322-336): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (396-410): CHC: Error trying to invoke SMT solver.
+// Warning 3046: (94-109): BMC: Division by zero happens here.
+// Warning 3046: (180-195): BMC: Division by zero happens here.

test/libsolidity/smtCheckerTests/math/addmulmod.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function test_addmod(uint x, uint y) public pure {
+		require(x % 13 == 0);
+		require(y % 13 == 0);
+
+		uint z = addmod(x, y, 13);
+		assert(z == 0);
+	}
+	function test_mulmod(uint x, uint y) public pure {
+		require(x % 13 == 0);
+		require(y % 13 == 0);
+
+		uint z = mulmod(x, y, 13);
+		assert(z == 0);
+	}
+}
+// ----
+// Warning 1218: (158-174): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (178-192): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (309-325): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (329-343): CHC: Error trying to invoke SMT solver.
+// Warning 7812: (329-343): BMC: Assertion violation might happen here.

test/libsolidity/smtCheckerTests/math/mulmod_1.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		assert(mulmod(2**256 - 1, 2, 14) == 2);
+		uint y = 0;
+		uint x = mulmod(2**256 - 1, 10, y);
+		assert(x == 1);
+	}
+	function g(uint x, uint y, uint k) public pure returns (uint) {
+		return mulmod(x, y, k);
+	}
+}
+// ----
+// Warning 1218: (83-108): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (141-166): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (76-114): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (170-184): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (263-278): CHC: Error trying to invoke SMT solver.
+// Warning 3046: (141-166): BMC: Division by zero happens here.
+// Warning 3046: (263-278): BMC: Division by zero happens here.

test/libsolutil/LEB128.cpp

@@ -0,0 +1,101 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+/**
+ * Unit tests for LEB128.
+ */
+
+#include <libsolutil/LEB128.h>
+
+#include <boost/test/unit_test.hpp>
+
+using namespace std;
+
+namespace solidity::util::test
+{
+
+BOOST_AUTO_TEST_SUITE(LEB128Test)
+
+BOOST_AUTO_TEST_CASE(encode_unsigned)
+{
+	bytes zero = solidity::util::lebEncode(0);
+	BOOST_REQUIRE(zero.size() == 1);
+	BOOST_REQUIRE(zero[0] == 0x00);
+
+	bytes one = solidity::util::lebEncode(1);
+	BOOST_REQUIRE(one.size() == 1);
+	BOOST_REQUIRE(one[0] == 0x01);
+
+	bytes large = solidity::util::lebEncode(624485);
+	BOOST_REQUIRE(large.size() == 3);
+	BOOST_REQUIRE(large[0] == 0xE5);
+	BOOST_REQUIRE(large[1] == 0x8E);
+	BOOST_REQUIRE(large[2] == 0x26);
+
+	bytes larger = solidity::util::lebEncodeSigned(123456123456);
+	BOOST_REQUIRE(larger.size() == 6);
+	BOOST_REQUIRE(larger[0] == 0xC0);
+	BOOST_REQUIRE(larger[1] == 0xE4);
+	BOOST_REQUIRE(larger[2] == 0xBB);
+	BOOST_REQUIRE(larger[3] == 0xF4);
+	BOOST_REQUIRE(larger[4] == 0xCB);
+	BOOST_REQUIRE(larger[5] == 0x03);
+}
+
+BOOST_AUTO_TEST_CASE(encode_signed)
+{
+	bytes zero = solidity::util::lebEncodeSigned(0);
+	BOOST_REQUIRE(zero.size() == 1);
+	BOOST_REQUIRE(zero[0] == 0x00);
+
+	bytes one = solidity::util::lebEncodeSigned(1);
+	BOOST_REQUIRE(one.size() == 1);
+	BOOST_REQUIRE(one[0] == 0x01);
+
+	bytes negative_one = solidity::util::lebEncodeSigned(-1);
+	BOOST_REQUIRE(negative_one.size() == 1);
+	BOOST_REQUIRE(negative_one[0] == 0x7f);
+
+	bytes negative_two = solidity::util::lebEncodeSigned(-2);
+	BOOST_REQUIRE(negative_two.size() == 1);
+	BOOST_REQUIRE(negative_two[0] == 0x7e);
+
+	bytes large = solidity::util::lebEncodeSigned(624485);
+	BOOST_REQUIRE(large.size() == 3);
+	BOOST_REQUIRE(large[0] == 0xE5);
+	BOOST_REQUIRE(large[1] == 0x8E);
+	BOOST_REQUIRE(large[2] == 0x26);
+
+	bytes negative_large = solidity::util::lebEncodeSigned(-123456);
+	BOOST_REQUIRE(negative_large.size() == 3);
+	BOOST_REQUIRE(negative_large[0] == 0xC0);
+	BOOST_REQUIRE(negative_large[1] == 0xBB);
+	BOOST_REQUIRE(negative_large[2] == 0x78);
+
+	bytes negative_larger = solidity::util::lebEncodeSigned(-123456123456);
+	BOOST_REQUIRE(negative_larger.size() == 6);
+	BOOST_REQUIRE(negative_larger[0] == 0xC0);
+	BOOST_REQUIRE(negative_larger[1] == 0x9B);
+	BOOST_REQUIRE(negative_larger[2] == 0xC4);
+	BOOST_REQUIRE(negative_larger[3] == 0x8B);
+	BOOST_REQUIRE(negative_larger[4] == 0xB4);
+	BOOST_REQUIRE(negative_larger[5] == 0x7C);
+}
+
+BOOST_AUTO_TEST_SUITE_END()
+
+}