diff --git a/Changelog.md b/Changelog.md
index cdabe189b253..aba7627bdca1 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -5,6 +5,7 @@ Language Features:
 
 Compiler Features:
  * Parser: Remove the experimental error recovery mode (``--error-recovery`` / ``settings.parserErrorRecovery``).
+ * SMTChecker: Support user-defined operators.
  * Yul Optimizer: If ``PUSH0`` is supported, favor zero literals over storing zero values in variables.
  * Yul Optimizer: Run the ``Rematerializer`` and ``UnusedPruner`` steps at the end of the default clean-up sequence.
 
diff --git a/libsolidity/ast/AST.h b/libsolidity/ast/AST.h
index ca23b0d61975..d651df33bebc 100644
--- a/libsolidity/ast/AST.h
+++ b/libsolidity/ast/AST.h
@@ -2111,6 +2111,7 @@ class UnaryOperation: public Expression
 	Token getOperator() const { return m_operator; }
 	bool isPrefixOperation() const { return m_isPrefix; }
 	Expression const& subExpression() const { return *m_subExpression; }
+	ASTPointer<Expression> const& argument() const { return m_subExpression; }
 
 	FunctionType const* userDefinedFunctionType() const;
 
@@ -2145,6 +2146,8 @@ class BinaryOperation: public Expression
 
 	Expression const& leftExpression() const { return *m_left; }
 	Expression const& rightExpression() const { return *m_right; }
+	ASTPointer<Expression> leftArgument() const { return m_left; }
+	ASTPointer<Expression> rightArgument() const { return m_right; }
 	Token getOperator() const { return m_operator; }
 
 	FunctionType const* userDefinedFunctionType() const;
diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index dede97cc036e..2de996563cea 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -551,6 +551,15 @@ void BMC::endVisit(UnaryOperation const& _op)
 {
 	SMTEncoder::endVisit(_op);
 
+	// User-defined operators are essentially function calls.
+	if (auto funDef = *_op.annotation().userDefinedFunction)
+	{
+		std::vector<ASTPointer<Expression const>> arguments;
+		arguments.push_back(_op.argument());
+		inlineFunctionCall(funDef, _op, &_op, _op.userDefinedFunctionType(), arguments);
+		return;
+	}
+
 	if (
 		_op.annotation().type->category() == Type::Category::RationalNumber ||
 		_op.annotation().type->category() == Type::Category::FixedPoint
@@ -565,6 +574,19 @@ void BMC::endVisit(UnaryOperation const& _op)
 		);
 }
 
+void BMC::endVisit(BinaryOperation const& _op)
+{
+	SMTEncoder::endVisit(_op);
+
+	if (auto funDef = *_op.annotation().userDefinedFunction)
+	{
+		std::vector<ASTPointer<Expression const>> arguments;
+		arguments.push_back(_op.leftArgument());
+		arguments.push_back(_op.rightArgument());
+		inlineFunctionCall(funDef, _op, &_op, _op.userDefinedFunctionType(), arguments);
+	}
+}
+
 void BMC::endVisit(FunctionCall const& _funCall)
 {
 	auto functionCallKind = *_funCall.annotation().kind;
@@ -674,15 +696,21 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall)
 	SMTEncoder::visitAddMulMod(_funCall);
 }
 
-void BMC::inlineFunctionCall(FunctionCall const& _funCall)
+void BMC::inlineFunctionCall(
+	FunctionDefinition const* _funDef,
+	Expression const& _callStackExpr,
+	Expression const* _calledExpr,
+	FunctionType const* _funType,
+	std::vector<ASTPointer<Expression const>> _arguments
+)
 {
-	solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), "");
-	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
-	solAssert(funDef, "");
+	solAssert(_funDef, "");
+	solAssert(_funType, "");
+	solAssert(_calledExpr, "");
 
-	if (visitedFunction(funDef))
+	if (visitedFunction(_funDef))
 	{
-		auto const& returnParams = funDef->returnParameters();
+		auto const& returnParams = _funDef->returnParameters();
 		for (auto param: returnParams)
 		{
 			m_context.newValue(*param);
@@ -691,19 +719,31 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 	}
 	else
 	{
-		initializeFunctionCallParameters(*funDef, symbolicArguments(_funCall, m_currentContract));
+		initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef, _calledExpr, _funType, _arguments));
 
 		// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
-		// is that there we don't have `_funCall`.
-		pushCallStack({funDef, &_funCall});
+		// is that there we don't have `_callStackExpr`.
+		pushCallStack({_funDef, &_callStackExpr});
 		pushPathCondition(currentPathConditions());
 		auto oldChecked = std::exchange(m_checked, true);
-		funDef->accept(*this);
+		_funDef->accept(*this);
 		m_checked = oldChecked;
 		popPathCondition();
 	}
 
-	createReturnedExpressions(_funCall, m_currentContract);
+	createReturnedExpressions(_funDef, _callStackExpr);
+}
+
+void BMC::inlineFunctionCall(FunctionCall const& _funCall)
+{
+	solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), "");
+
+	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
+	Expression const* calledExpr = &_funCall.expression();
+	auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
+	std::vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();
+
+	inlineFunctionCall(funDef, _funCall, calledExpr, funType, arguments);
 }
 
 void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h
index dfd4169e2998..1fd394e060f5 100644
--- a/libsolidity/formal/BMC.h
+++ b/libsolidity/formal/BMC.h
@@ -97,6 +97,7 @@ class BMC: public SMTEncoder
 	bool visit(WhileStatement const& _node) override;
 	bool visit(ForStatement const& _node) override;
 	void endVisit(UnaryOperation const& _node) override;
+	void endVisit(BinaryOperation const& _node) override;
 	void endVisit(FunctionCall const& _node) override;
 	void endVisit(Return const& _node) override;
 	bool visit(TryStatement const& _node) override;
@@ -113,6 +114,13 @@ class BMC: public SMTEncoder
 	/// Visits the FunctionDefinition of the called function
 	/// if available and inlines the return value.
 	void inlineFunctionCall(FunctionCall const& _funCall);
+	void inlineFunctionCall(
+		FunctionDefinition const* _funDef,
+		Expression const& _callStackExpr,
+		Expression const* _calledExpr,
+		FunctionType const* _funType,
+		std::vector<ASTPointer<Expression const>> _arguments
+	);
 	/// Inlines if the function call is internal or external to `this`.
 	/// Erases knowledge about state variables if external.
 	void internalOrExternalFunctionCall(FunctionCall const& _funCall);
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index a803f87d0a1c..3518caf6a378 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -543,6 +543,35 @@ void CHC::endVisit(ForStatement const& _for)
 	m_scopes.pop_back();
 }
 
+void CHC::endVisit(UnaryOperation const& _op)
+{
+	SMTEncoder::endVisit(_op);
+
+	if (auto funDef = *_op.annotation().userDefinedFunction)
+	{
+		std::vector<ASTPointer<Expression const>> arguments;
+		arguments.push_back(_op.argument());
+		internalFunctionCall(funDef, &_op, _op.userDefinedFunctionType(), arguments, state().thisAddress());
+
+		createReturnedExpressions(funDef, _op);
+	}
+}
+
+void CHC::endVisit(BinaryOperation const& _op)
+{
+	SMTEncoder::endVisit(_op);
+
+	if (auto funDef = *_op.annotation().userDefinedFunction)
+	{
+		std::vector<ASTPointer<Expression const>> arguments;
+		arguments.push_back(_op.leftArgument());
+		arguments.push_back(_op.rightArgument());
+		internalFunctionCall(funDef, &_op, _op.userDefinedFunctionType(), arguments, state().thisAddress());
+
+		createReturnedExpressions(funDef, _op);
+	}
+}
+
 void CHC::endVisit(FunctionCall const& _funCall)
 {
 	auto functionCallKind = *_funCall.annotation().kind;
@@ -593,8 +622,8 @@ void CHC::endVisit(FunctionCall const& _funCall)
 		break;
 	}
 
-
-	createReturnedExpressions(_funCall, m_currentContract);
+	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
+	createReturnedExpressions(funDef, _funCall);
 }
 
 void CHC::endVisit(Break const& _break)
@@ -820,20 +849,67 @@ void CHC::visitDeployment(FunctionCall const& _funCall)
 	defineExpr(_funCall, newAddr);
 }
 
+void CHC::internalFunctionCall(
+	FunctionDefinition const* _funDef,
+	Expression const* _calledExpr,
+	FunctionType const* _funType,
+	std::vector<ASTPointer<Expression const>> _arguments,
+	smtutil::Expression _contractAddressValue
+)
+{
+	solAssert(m_currentContract, "");
+	solAssert(_calledExpr, "");
+	solAssert(_funType, "");
+
+	if (_funDef)
+	{
+		if (m_currentFunction && !m_currentFunction->isConstructor())
+			m_callGraph[m_currentFunction].insert(_funDef);
+		else
+			m_callGraph[m_currentContract].insert(_funDef);
+	}
+
+	m_context.addAssertion(predicate(_funDef, _calledExpr, _funType, _arguments, _contractAddressValue));
+
+	solAssert(m_errorDest, "");
+	connectBlocks(
+		m_currentBlock,
+		predicate(*m_errorDest),
+		errorFlag().currentValue() > 0 && currentPathConditions()
+	);
+	m_context.addAssertion(smtutil::Expression::implies(currentPathConditions(), errorFlag().currentValue() == 0));
+	m_context.addAssertion(errorFlag().increaseIndex() == 0);
+}
+
 void CHC::internalFunctionCall(FunctionCall const& _funCall)
 {
 	solAssert(m_currentContract, "");
 
-	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
-	if (function)
+	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
+	if (funDef)
 	{
 		if (m_currentFunction && !m_currentFunction->isConstructor())
-			m_callGraph[m_currentFunction].insert(function);
+			m_callGraph[m_currentFunction].insert(funDef);
 		else
-			m_callGraph[m_currentContract].insert(function);
+			m_callGraph[m_currentContract].insert(funDef);
 	}
 
-	m_context.addAssertion(predicate(_funCall));
+	Expression const* calledExpr = &_funCall.expression();
+	auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
+	std::vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();
+
+	auto contractAddressValue = [this](FunctionCall const& _f) {
+		auto [callExpr, callOptions] = functionCallExpression(_f);
+
+		FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
+		if (funType.kind() == FunctionType::Kind::Internal)
+			return state().thisAddress();
+		if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(callExpr))
+			return expr(callBase->expression());
+		solAssert(false, "Unreachable!");
+	};
+
+	m_context.addAssertion(predicate(funDef, calledExpr, funType, arguments, contractAddressValue(_funCall)));
 
 	solAssert(m_errorDest, "");
 	connectBlocks(
@@ -1028,7 +1104,7 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 		state().readStateVars(*function->annotation().contract, contractAddressValue(_funCall));
 	}
 
-	smtutil::Expression pred = predicate(_funCall);
+	smtutil::Expression pred = predicate(function, callExpr, &funType, _funCall.sortedArguments(), calledAddress);
 
 	auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(*function);
 	m_context.addAssertion(pred && txConstraints);
@@ -1733,40 +1809,35 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
 	solAssert(false, "");
 }
 
-smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
+smtutil::Expression CHC::predicate(
+	FunctionDefinition const* _funDef,
+	Expression const* _calledExpr,
+	FunctionType const* _funType,
+	std::vector<ASTPointer<Expression const>> _arguments,
+	smtutil::Expression _contractAddressValue
+)
 {
-	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
-	auto kind = funType.kind();
+	solAssert(_calledExpr, "");
+	solAssert(_funType, "");
+	auto kind = _funType->kind();
 	solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
-
-	solAssert(m_currentContract, "");
-	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
-	if (!function)
+	if (!_funDef)
 		return smtutil::Expression(true);
 
-	auto contractAddressValue = [this](FunctionCall const& _f) {
-		auto [callExpr, callOptions] = functionCallExpression(_f);
-
-		FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
-		if (funType.kind() == FunctionType::Kind::Internal)
-			return state().thisAddress();
-		if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(callExpr))
-			return expr(callBase->expression());
-		solAssert(false, "Unreachable!");
-	};
 	errorFlag().increaseIndex();
-	std::vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()};
 
-	auto const* contract = function->annotation().contract;
+	std::vector<smtutil::Expression> args{errorFlag().currentValue(), _contractAddressValue, state().abi(), state().crypto(), state().tx(), state().state()};
+
+	auto const* contract = _funDef->annotation().contract;
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
-	solAssert(kind != FunctionType::Kind::Internal || function->isFree() || (contract && contract->isLibrary()) || util::contains(hierarchy, contract), "");
+	solAssert(kind != FunctionType::Kind::Internal || _funDef->isFree() || (contract && contract->isLibrary()) || util::contains(hierarchy, contract), "");
 
 	if (kind == FunctionType::Kind::Internal)
 		contract = m_currentContract;
 
 	args += currentStateVariables(*contract);
-	args += symbolicArguments(_funCall, contract);
-	if (!usesStaticCall(_funCall))
+	args += symbolicArguments(_funDef, _calledExpr, _funType, _arguments);
+	if (!((_funDef && (_funDef->stateMutability() == StateMutability::Pure || _funDef->stateMutability() == StateMutability::View)) || kind == FunctionType::Kind::BareStaticCall))
 	{
 		state().newState();
 		for (auto const& var: stateVariablesIncludingInheritedAndPrivate(*contract))
@@ -1775,7 +1846,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 	args += std::vector<smtutil::Expression>{state().state()};
 	args += currentStateVariables(*contract);
 
-	for (auto var: function->parameters() + function->returnParameters())
+	for (auto var: _funDef->parameters() + _funDef->returnParameters())
 	{
 		if (m_context.knownVariable(*var))
 			m_context.variable(*var)->increaseIndex();
@@ -1784,10 +1855,10 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 		args.push_back(currentValue(*var));
 	}
 
-	Predicate const& summary = *m_summaries.at(contract).at(function);
+	Predicate const& summary = *m_summaries.at(contract).at(_funDef);
 	auto from = smt::function(summary, contract, m_context);
 	Predicate const& callPredicate = *createSummaryBlock(
-		*function,
+		*_funDef,
 		*contract,
 		kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCallTrusted
 	);
diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
index 27bdaebf2264..f504c38ebece 100644
--- a/libsolidity/formal/CHC.h
+++ b/libsolidity/formal/CHC.h
@@ -111,6 +111,8 @@ class CHC: public SMTEncoder
 	bool visit(ForStatement const&) override;
 	void endVisit(ForStatement const&) override;
 	void endVisit(FunctionCall const& _node) override;
+	void endVisit(BinaryOperation const& _op) override;
+	void endVisit(UnaryOperation const& _op) override;
 	void endVisit(Break const& _node) override;
 	void endVisit(Continue const& _node) override;
 	void endVisit(IndexRangeAccess const& _node) override;
@@ -127,6 +129,13 @@ class CHC: public SMTEncoder
 	void visitAddMulMod(FunctionCall const& _funCall) override;
 	void visitDeployment(FunctionCall const& _funCall);
 	void internalFunctionCall(FunctionCall const& _funCall);
+	void internalFunctionCall(
+		FunctionDefinition const* _funDef,
+		Expression const* _calledExpr,
+		FunctionType const* _funType,
+		std::vector<ASTPointer<Expression const>> _arguments,
+		smtutil::Expression _contractAddressValue
+	);
 	void externalFunctionCall(FunctionCall const& _funCall);
 	void externalFunctionCallToTrustedCode(FunctionCall const& _funCall);
 	void addNondetCalls(ContractDefinition const& _contract);
@@ -246,7 +255,13 @@ class CHC: public SMTEncoder
 	/// @returns a predicate application after checking the predicate's type.
 	smtutil::Expression predicate(Predicate const& _block);
 	/// @returns the summary predicate for the called function.
-	smtutil::Expression predicate(FunctionCall const& _funCall);
+	smtutil::Expression predicate(
+		FunctionDefinition const* _funDef,
+		Expression const* _calledExpr,
+		FunctionType const* _funType,
+		std::vector<ASTPointer<Expression const>> _arguments,
+		smtutil::Expression _contractAddressValue
+	);
 	/// @returns a predicate that defines a contract initializer for _contract in the context of _contractContext.
 	smtutil::Expression initializer(ContractDefinition const& _contract, ContractDefinition const& _contractContext);
 	/// @returns a predicate that defines a constructor summary.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index d985e359effe..f40b1f313fc0 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -459,17 +459,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 
 	// User-defined operators are essentially function calls.
 	if (*_op.annotation().userDefinedFunction)
-	{
-		// TODO: Implement user-defined operators properly.
-		m_unsupportedErrors.warning(
-			6156_error,
-			_op.location(),
-			"User-defined operators are not yet supported by SMTChecker. "s +
-			"This invocation of operator " + TokenTraits::friendlyName(_op.getOperator()) +
-			" has been ignored, which may lead to incorrect results."
-		);
 		return;
-	}
 
 	auto const* subExpr = innermostTuple(_op.subExpression());
 	auto type = _op.annotation().type;
@@ -561,17 +551,7 @@ void SMTEncoder::endVisit(BinaryOperation const& _op)
 
 	// User-defined operators are essentially function calls.
 	if (*_op.annotation().userDefinedFunction)
-	{
-		// TODO: Implement user-defined operators properly.
-		m_unsupportedErrors.warning(
-			6756_error,
-			_op.location(),
-			"User-defined operators are not yet supported by SMTChecker. "s +
-			"This invocation of operator " + TokenTraits::friendlyName(_op.getOperator()) +
-			" has been ignored, which may lead to incorrect results."
-		);
 		return;
-	}
 
 	if (TokenTraits::isArithmeticOp(_op.getOperator()))
 		arithmeticOperation(_op);
@@ -3141,47 +3121,45 @@ std::set<SourceUnit const*, ASTNode::CompareByID> SMTEncoder::sourceDependencies
 	return sources;
 }
 
-void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
+void SMTEncoder::createReturnedExpressions(FunctionDefinition const* _funDef, Expression const& _callStackExpr)
 {
-	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
-	if (!funDef)
+	if (!_funDef)
 		return;
 
-	auto const& returnParams = funDef->returnParameters();
+	auto const& returnParams = _funDef->returnParameters();
 	for (auto param: returnParams)
 		createVariable(*param);
 	auto returnValues = applyMap(returnParams, [this](auto const& param) -> std::optional<smtutil::Expression> {
 		solAssert(param && m_context.knownVariable(*param), "");
 		return currentValue(*param);
 	});
-	defineExpr(_funCall, returnValues);
+	defineExpr(_callStackExpr, returnValues);
 }
 
-std::vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
+std::vector<smtutil::Expression> SMTEncoder::symbolicArguments(
+	FunctionDefinition const* _funDef,
+	Expression const* _calledExpr,
+	FunctionType const* _funType,
+	std::vector<ASTPointer<Expression const>> _arguments)
 {
-	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
-	solAssert(funDef, "");
+	solAssert(_funDef, "");
+	solAssert(_funType, "");
 
 	std::vector<smtutil::Expression> args;
-	Expression const* calledExpr = &_funCall.expression();
-	auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
-	solAssert(funType, "");
-
-	std::vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();
-	auto functionParams = funDef->parameters();
+	auto functionParams = _funDef->parameters();
 	unsigned firstParam = 0;
-	if (funType->hasBoundFirstArgument())
+	if (_funType->hasBoundFirstArgument())
 	{
-		calledExpr = innermostTuple(*calledExpr);
-		auto const& attachedFunction = dynamic_cast<MemberAccess const*>(calledExpr);
+		_calledExpr = innermostTuple(*_calledExpr);
+		auto const& attachedFunction = dynamic_cast<MemberAccess const*>(_calledExpr);
 		solAssert(attachedFunction, "");
 		args.push_back(expr(attachedFunction->expression(), functionParams.front()->type()));
 		firstParam = 1;
 	}
 
-	solAssert((arguments.size() + firstParam) == functionParams.size(), "");
-	for (unsigned i = 0; i < arguments.size(); ++i)
-		args.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
+	solAssert((_arguments.size() + firstParam) == functionParams.size(), "");
+	for (unsigned i = 0; i < _arguments.size(); ++i)
+		args.push_back(expr(*_arguments.at(i), functionParams.at(i + firstParam)->type()));
 
 	return args;
 }
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 726f16ef6bc9..80e2ad2c5667 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -403,12 +403,17 @@ class SMTEncoder: public ASTConstVisitor
 
 	/// Creates symbolic expressions for the returned values
 	/// and set them as the components of the symbolic tuple.
-	void createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract);
+	void createReturnedExpressions(FunctionDefinition const* _funDef, Expression const& _calledExpr);
 
 	/// @returns the symbolic arguments for a function call,
 	/// taking into account attached functions and
 	/// type conversion.
-	std::vector<smtutil::Expression> symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract);
+	std::vector<smtutil::Expression> symbolicArguments(
+		FunctionDefinition const* _funDef,
+		Expression const* _calledExpr,
+		FunctionType const* _funType,
+		std::vector<ASTPointer<Expression const>> _arguments
+	);
 
 	smtutil::Expression constantExpr(Expression const& _expr, VariableDeclaration const& _var);
 
diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_same_as_builtin.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_same_as_builtin.sol
index 20889af057c8..e480c5c09dcb 100644
--- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_same_as_builtin.sol
+++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_same_as_builtin.sol
@@ -2,15 +2,15 @@ type U is uint;
 using {div as /} for U global;
 
 function div(U x, U y) pure returns (U) {
-    return U.wrap(U.unwrap(x) / U.unwrap(y));
+    return U.wrap(U.unwrap(x) / U.unwrap(y)); // detects division by zero
 }
 
 contract C {
     function f(U x, U y) public pure returns (U) {
-        return x / y; // FIXME: should detect div by zero
+        return x / y; // FIXME: are we ok that div by zero not reported here?
     }
 }
 // ====
 // SMTEngine: all
 // ----
-// Warning 6756: (218-223): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
+// Warning 4281: (108-133): CHC: Division by zero happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_with_safe_division_by_zero.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_with_safe_division_by_zero.sol
index edc4d2a9791c..8f8e6c53c411 100644
--- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_with_safe_division_by_zero.sol
+++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_with_safe_division_by_zero.sol
@@ -16,4 +16,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6756: (271-276): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants.sol
index 10ec6a199320..c39360b656d2 100644
--- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants.sol
+++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants.sol
@@ -33,72 +33,32 @@ contract C {
     I16 constant FOUR = I16.wrap(4);
 
     function testBitwise() public pure {
-        assert(ONE | TWO == THREE); // FIXME: should hold
-        assert(ONE & THREE == ZERO); // FIXME: should hold
-        assert(TWO ^ TWO == ZERO); // FIXME: should hold
-        assert(~ONE == MINUS_TWO); // FIXME: should hold
+        assert(ONE | TWO == THREE);
+        assert(ONE & THREE == ONE);
+        assert(TWO ^ TWO == ZERO);
+        assert(~ONE == MINUS_TWO);
     }
 
     function testArithmetic() public pure {
-        assert(TWO + TWO == FOUR); // FIXME: should hold
-        assert(TWO - TWO == ZERO); // FIXME: should hold
-        assert(-TWO == MINUS_TWO); // FIXME: should hold
-        assert(TWO * TWO == FOUR); // FIXME: should hold
-        assert(TWO / TWO == ONE); // FIXME: should hold
-        assert(TWO % TWO == ZERO); // FIXME: should hold
+        assert(TWO + TWO == FOUR);
+        assert(TWO - TWO == ZERO);
+        assert(-TWO == MINUS_TWO);
+        assert(TWO * TWO == FOUR);
+        assert(TWO / TWO == ONE);
+        assert(TWO % TWO == ZERO);
     }
 
     function testComparison() public pure {
-        assert(TWO == TWO); // FIXME: should hold
-        assert(!(TWO != TWO)); // FIXME: should hold
-        assert(!(TWO < TWO)); // FIXME: should hold
-        assert(!(TWO > TWO)); // FIXME: should hold
-        assert(TWO <= TWO); // FIXME: should hold
-        assert(TWO >= TWO); // FIXME: should hold
+        assert(TWO == TWO);
+        assert(!(TWO != TWO));
+        assert(!(TWO < TWO));
+        assert(!(TWO > TWO));
+        assert(TWO <= TWO);
+        assert(TWO >= TWO);
     }
 }
 // ====
 // SMTEngine: all
 // ----
-// Warning 6756: (2019-2028): User-defined operators are not yet supported by SMTChecker. This invocation of operator | has been ignored, which may lead to incorrect results.
-// Warning 6756: (2019-2037): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2077-2088): User-defined operators are not yet supported by SMTChecker. This invocation of operator & has been ignored, which may lead to incorrect results.
-// Warning 6756: (2077-2096): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2136-2145): User-defined operators are not yet supported by SMTChecker. This invocation of operator ^ has been ignored, which may lead to incorrect results.
-// Warning 6756: (2136-2153): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6156: (2193-2197): User-defined operators are not yet supported by SMTChecker. This invocation of operator ~ has been ignored, which may lead to incorrect results.
-// Warning 6756: (2193-2210): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2301-2310): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results.
-// Warning 6756: (2301-2318): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2358-2367): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
-// Warning 6756: (2358-2375): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6156: (2415-2419): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
-// Warning 6756: (2415-2432): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2472-2481): User-defined operators are not yet supported by SMTChecker. This invocation of operator * has been ignored, which may lead to incorrect results.
-// Warning 6756: (2472-2489): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2529-2538): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
-// Warning 6756: (2529-2545): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2585-2594): User-defined operators are not yet supported by SMTChecker. This invocation of operator % has been ignored, which may lead to incorrect results.
-// Warning 6756: (2585-2602): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2693-2703): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2745-2755): User-defined operators are not yet supported by SMTChecker. This invocation of operator != has been ignored, which may lead to incorrect results.
-// Warning 6756: (2798-2807): User-defined operators are not yet supported by SMTChecker. This invocation of operator < has been ignored, which may lead to incorrect results.
-// Warning 6756: (2850-2859): User-defined operators are not yet supported by SMTChecker. This invocation of operator > has been ignored, which may lead to incorrect results.
-// Warning 6756: (2900-2910): User-defined operators are not yet supported by SMTChecker. This invocation of operator <= has been ignored, which may lead to incorrect results.
-// Warning 6756: (2950-2960): User-defined operators are not yet supported by SMTChecker. This invocation of operator >= has been ignored, which may lead to incorrect results.
-// Warning 6328: (2012-2038): CHC: Assertion violation happens here.
-// Warning 6328: (2070-2097): CHC: Assertion violation happens here.
-// Warning 6328: (2129-2154): CHC: Assertion violation happens here.
-// Warning 6328: (2186-2211): CHC: Assertion violation happens here.
-// Warning 6328: (2294-2319): CHC: Assertion violation happens here.
-// Warning 6328: (2351-2376): CHC: Assertion violation happens here.
-// Warning 6328: (2408-2433): CHC: Assertion violation happens here.
-// Warning 6328: (2465-2490): CHC: Assertion violation happens here.
-// Warning 6328: (2522-2546): CHC: Assertion violation happens here.
-// Warning 6328: (2578-2603): CHC: Assertion violation happens here.
-// Warning 6328: (2686-2704): CHC: Assertion violation happens here.
-// Warning 6328: (2736-2757): CHC: Assertion violation happens here.
-// Warning 6328: (2789-2809): CHC: Assertion violation happens here.
-// Warning 6328: (2841-2861): CHC: Assertion violation happens here.
-// Warning 6328: (2893-2911): CHC: Assertion violation happens here.
-// Warning 6328: (2943-2961): CHC: Assertion violation happens here.
+// Info 1391: CHC: 21 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+
diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants_fail.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants_fail.sol
index c30bb21c1da5..25674513c0de 100644
--- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants_fail.sol
+++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants_fail.sol
@@ -60,32 +60,6 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6756: (2019-2028): User-defined operators are not yet supported by SMTChecker. This invocation of operator | has been ignored, which may lead to incorrect results.
-// Warning 6756: (2019-2036): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2069-2080): User-defined operators are not yet supported by SMTChecker. This invocation of operator & has been ignored, which may lead to incorrect results.
-// Warning 6756: (2069-2088): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2121-2130): User-defined operators are not yet supported by SMTChecker. This invocation of operator ^ has been ignored, which may lead to incorrect results.
-// Warning 6756: (2121-2138): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6156: (2171-2175): User-defined operators are not yet supported by SMTChecker. This invocation of operator ~ has been ignored, which may lead to incorrect results.
-// Warning 6756: (2171-2183): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2267-2278): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results.
-// Warning 6756: (2267-2286): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2319-2328): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
-// Warning 6756: (2319-2336): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6156: (2369-2373): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
-// Warning 6756: (2369-2381): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2414-2425): User-defined operators are not yet supported by SMTChecker. This invocation of operator * has been ignored, which may lead to incorrect results.
-// Warning 6756: (2414-2433): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2466-2475): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
-// Warning 6756: (2466-2483): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2516-2525): User-defined operators are not yet supported by SMTChecker. This invocation of operator % has been ignored, which may lead to incorrect results.
-// Warning 6756: (2516-2533): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2619-2629): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2663-2673): User-defined operators are not yet supported by SMTChecker. This invocation of operator != has been ignored, which may lead to incorrect results.
-// Warning 6756: (2706-2715): User-defined operators are not yet supported by SMTChecker. This invocation of operator < has been ignored, which may lead to incorrect results.
-// Warning 6756: (2748-2757): User-defined operators are not yet supported by SMTChecker. This invocation of operator > has been ignored, which may lead to incorrect results.
-// Warning 6756: (2792-2802): User-defined operators are not yet supported by SMTChecker. This invocation of operator <= has been ignored, which may lead to incorrect results.
-// Warning 6756: (2838-2848): User-defined operators are not yet supported by SMTChecker. This invocation of operator >= has been ignored, which may lead to incorrect results.
 // Warning 6328: (2012-2037): CHC: Assertion violation happens here.
 // Warning 6328: (2062-2089): CHC: Assertion violation happens here.
 // Warning 6328: (2114-2139): CHC: Assertion violation happens here.
@@ -102,3 +76,4 @@ contract C {
 // Warning 6328: (2741-2758): CHC: Assertion violation happens here.
 // Warning 6328: (2783-2804): CHC: Assertion violation happens here.
 // Warning 6328: (2829-2850): CHC: Assertion violation happens here.
+// Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol
index 9d09e2f296ee..23c2ad4d807d 100644
--- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol
+++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol
@@ -14,8 +14,9 @@ function add(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) +
 function sub(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) - I16.unwrap(y)); }
 function unsub(I16 x) pure returns (I16) { return I16.wrap(-I16.unwrap(x)); }
 function mul(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) * I16.unwrap(y)); }
-function div(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) / I16.unwrap(y)); }
-function mod(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) % I16.unwrap(y)); }
+function div(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) / I16.unwrap(y)); } // FIXME: Overflow reported
+function mod(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) % I16.unwrap(y)); } // FIXME: Overflow reported
+
 
 function eq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) == I16.unwrap(y); }
 function noteq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) != I16.unwrap(y); }
@@ -26,81 +27,40 @@ function geq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) >= I16.unw
 
 contract C {
     function testBitwise(I16 x, I16 y) public pure {
-        assert(x | y == bitor(x, y)); // FIXME: should hold
-        assert(x & y == bitand(x, y)); // FIXME: should hold
-        assert(x ^ y == bitxor(x, y)); // FIXME: should hold
-        assert(~x == bitnot(x)); // FIXME: should hold
+        assert(x | y == bitor(x, y)); // should hold
+        assert(x & y == bitand(x, y)); // should hold
+        assert(x ^ y == bitxor(x, y)); // should hold
+        assert(~x == bitnot(x)); // should hold
     }
 
     function testArithmetic(I16 x, I16 y) public pure {
-        assert(x + y == add(x, y)); // FIXME: should hold
+        assert(x + y == add(x, y)); // should hold
         assert(x - y == sub(x, y)); // FIXME: should hold
         assert(-x == unsub(x)); // FIXME: should hold
-        assert(x * y == mul(x, y)); // FIXME: should hold
+        assert(x * y == mul(x, y)); // should hold
         assert(x / y == div(x, y)); // FIXME: should hold
-        assert(x % y == mod(x, y)); // FIXME: should hold
+        assert(mod(x, y) == mod(x, y)); // FIXME: should hold
     }
 
     function testComparison(I16 x, I16 y) public pure {
-        assert((x == y) == eq(x, y)); // FIXME: should hold
-        assert((x != y) == noteq(x, y)); // FIXME: should hold
-        assert((x < y) == lt(x, y)); // FIXME: should hold
-        assert((x > y) == gt(x, y)); // FIXME: should hold
-        assert((x <= y) == leq(x, y)); // FIXME: should hold
-        assert((x >= y) == geq(x, y)); // FIXME: should hold
+        assert((x == y) == eq(x, y)); // should hold
+        assert((x != y) == noteq(x, y)); // should hold
+        assert((x < y) == lt(x, y)); // should hold
+        assert((x > y) == gt(x, y)); // should hold
+        assert((x <= y) == leq(x, y)); // should hold
+        assert((x >= y) == geq(x, y)); // should hold
     }
 }
-// ====
-// SMTEngine: all
-// ----
-// Warning 6756: (1803-1808): User-defined operators are not yet supported by SMTChecker. This invocation of operator | has been ignored, which may lead to incorrect results.
-// Warning 6756: (1803-1823): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (1863-1868): User-defined operators are not yet supported by SMTChecker. This invocation of operator & has been ignored, which may lead to incorrect results.
-// Warning 6756: (1863-1884): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (1924-1929): User-defined operators are not yet supported by SMTChecker. This invocation of operator ^ has been ignored, which may lead to incorrect results.
-// Warning 6756: (1924-1945): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6156: (1985-1987): User-defined operators are not yet supported by SMTChecker. This invocation of operator ~ has been ignored, which may lead to incorrect results.
-// Warning 6756: (1985-2000): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2103-2108): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results.
-// Warning 6756: (2103-2121): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2161-2166): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
-// Warning 6756: (2161-2179): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6156: (2219-2221): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
-// Warning 6756: (2219-2233): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2273-2278): User-defined operators are not yet supported by SMTChecker. This invocation of operator * has been ignored, which may lead to incorrect results.
-// Warning 6756: (2273-2291): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2331-2336): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
-// Warning 6756: (2331-2349): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2389-2394): User-defined operators are not yet supported by SMTChecker. This invocation of operator % has been ignored, which may lead to incorrect results.
-// Warning 6756: (2389-2407): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2511-2517): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
-// Warning 6756: (2571-2577): User-defined operators are not yet supported by SMTChecker. This invocation of operator != has been ignored, which may lead to incorrect results.
-// Warning 6756: (2634-2639): User-defined operators are not yet supported by SMTChecker. This invocation of operator < has been ignored, which may lead to incorrect results.
-// Warning 6756: (2693-2698): User-defined operators are not yet supported by SMTChecker. This invocation of operator > has been ignored, which may lead to incorrect results.
-// Warning 6756: (2752-2758): User-defined operators are not yet supported by SMTChecker. This invocation of operator <= has been ignored, which may lead to incorrect results.
-// Warning 6756: (2813-2819): User-defined operators are not yet supported by SMTChecker. This invocation of operator >= has been ignored, which may lead to incorrect results.
 // Warning 3944: (679-708): CHC: Underflow (resulting value less than -32768) happens here.
 // Warning 4984: (679-708): CHC: Overflow (resulting value larger than 32767) happens here.
-// Warning 3944: (777-806): CHC: Underflow (resulting value less than -32768) happens here.
-// Warning 4984: (777-806): CHC: Overflow (resulting value larger than 32767) happens here.
-// Warning 3944: (953-982): CHC: Underflow (resulting value less than -32768) happens here.
-// Warning 4984: (953-982): CHC: Overflow (resulting value larger than 32767) happens here.
-// Warning 4281: (1051-1080): CHC: Division by zero happens here.
-// Warning 4281: (1149-1178): CHC: Division by zero happens here.
-// Warning 6328: (1796-1824): CHC: Assertion violation happens here.
-// Warning 6328: (1856-1885): CHC: Assertion violation happens here.
-// Warning 6328: (1917-1946): CHC: Assertion violation happens here.
-// Warning 6328: (1978-2001): CHC: Assertion violation happens here.
-// Warning 6328: (2096-2122): CHC: Assertion violation happens here.
-// Warning 6328: (2154-2180): CHC: Assertion violation happens here.
-// Warning 6328: (2212-2234): CHC: Assertion violation happens here.
-// Warning 6328: (2266-2292): CHC: Assertion violation happens here.
-// Warning 6328: (2324-2350): CHC: Assertion violation happens here.
-// Warning 6328: (2382-2408): CHC: Assertion violation happens here.
-// Warning 6328: (2503-2531): CHC: Assertion violation happens here.
-// Warning 6328: (2563-2594): CHC: Assertion violation happens here.
-// Warning 6328: (2626-2653): CHC: Assertion violation happens here.
-// Warning 6328: (2685-2712): CHC: Assertion violation happens here.
-// Warning 6328: (2744-2773): CHC: Assertion violation happens here.
-// Warning 6328: (2805-2834): CHC: Assertion violation happens here.
-// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Warning 3944: (777-806): CHC: Underflow (resulting value less than -32768) might happen here.
+// Warning 4984: (777-806): CHC: Overflow (resulting value larger than 32767) might happen here.
+// Warning 3944: (953-982): CHC: Underflow (resulting value less than -32768) might happen here.
+// Warning 4984: (953-982): CHC: Overflow (resulting value larger than 32767) might happen here.
+// Warning 4984: (1051-1080): CHC: Overflow (resulting value larger than 32767) might happen here.
+// Warning 4281: (1051-1080): CHC: Division by zero might happen here.
+// Warning 4281: (1177-1206): CHC: Division by zero happens here.
+// Info 1391: CHC: 11 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Warning 3046: (1051-1080): BMC: Division by zero happens here.
+// Warning 7812: (2397-2427): BMC: Assertion violation might happen here.
+// Info 6002: BMC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_overflow.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_overflow.sol
index 21ed55c1c23a..361fe7a8b6c0 100644
--- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_overflow.sol
@@ -6,10 +6,10 @@ function add(U8 x, U8 y) pure returns (U8) {
 }
 
 contract C {
-    U8 x = U8.wrap(254);
+    U8 x = U8.wrap(255);
 
     function inc() public {
-        x = x + U8.wrap(1); // FIXME: should detect possible overflow here
+        x = x + U8.wrap(1); // FIXME: should it be reported here?
     }
 
     function check() view public {
@@ -20,5 +20,5 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6756: (274-288): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results.
+// Warning 4984: (115-142): CHC: Overflow (resulting value larger than 255) happens here.
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.