Merge pull request #5189 from ethereum/smt_function_call

[SMTChecker] Inline calls to internal functions

25 files changed, 534 insertions, 75 deletions

diff --git a/Changelog.md b/Changelog.md
index 05636a30..01599026 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -102,6 +102,7 @@ Compiler Features:
  * Removed ``pragma experimental "v0.5.0";``.
  * Syntax Checker: Improved error message for lookup in function types.
  * Name Resolver: Updated name suggestion look up function to take into account length of the identifier: 1: no search, 2-3: at most one change, 4-: at most two changes
+ * SMTChecker: Support calls to internal functions that return none or a single value.
 
 Bugfixes:
  * Build System: Support versions of CVC4 linked against CLN instead of GMP. In case of compilation issues due to the experimental SMT solver support, the solvers can be disabled when configuring the project with CMake using ``-DUSE_CVC4=OFF`` or ``-DUSE_Z3=OFF``.
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index a7973852..1e27dc33 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -71,29 +71,41 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 			_function.location(),
 			"Assertion checker does not yet support constructors and functions with modifiers."
 		);
-	m_currentFunction = &_function;
-	m_interface->reset();
-	m_pathConditions.clear();
+	m_functionPath.push_back(&_function);
+	// Not visited by a function call
+	if (isRootFunction())
+	{
+		m_interface->reset();
+		m_pathConditions.clear();
+		m_expressions.clear();
+		resetStateVariables();
+		initializeLocalVariables(_function);
+	}
+
 	m_loopExecutionHappened = false;
-	resetStateVariables();
-	initializeLocalVariables(_function);
 	return true;
 }
 
 void SMTChecker::endVisit(FunctionDefinition const&)
 {
-	// TODO we could check for "reachability", i.e. satisfiability here.
-	// We only handle local variables, so we clear at the beginning of the function.
-	// If we add storage variables, those should be cleared differently.
-	removeLocalVariables();
-	m_currentFunction = nullptr;
+	// If _function was visited from a function call we don't remove
+	// the local variables just yet, since we might need them for
+	// future calls.
+	// Otherwise we remove any local variables from the context and
+	// keep the state variables.
+	if (isRootFunction())
+		removeLocalVariables();
+	m_functionPath.pop_back();
 }
 
 bool SMTChecker::visit(IfStatement const& _node)
 {
 	_node.condition().accept(*this);
 
-	checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
+	// We ignore called functions here because they have
+	// specific input values.
+	if (isRootFunction())
+		checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
 
 	auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
 	vector<VariableDeclaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
@@ -122,12 +134,14 @@ bool SMTChecker::visit(WhileStatement const& _node)
 		visitBranch(_node.body());
 		// TODO the assertions generated in the body should still be active in the condition
 		_node.condition().accept(*this);
-		checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE.");
+		if (isRootFunction())
+			checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE.");
 	}
 	else
 	{
 		_node.condition().accept(*this);
-		checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
+		if (isRootFunction())
+			checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
 
 		visitBranch(_node.body(), expr(_node.condition()));
 	}
@@ -158,7 +172,8 @@ bool SMTChecker::visit(ForStatement const& _node)
 	if (_node.condition())
 	{
 		_node.condition()->accept(*this);
-		checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
+		if (isRootFunction())
+			checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
 	}
 
 	VariableSequenceCounters sequenceCountersStart = m_variables;
@@ -198,10 +213,6 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
 		);
 }
 
-void SMTChecker::endVisit(ExpressionStatement const&)
-{
-}
-
 void SMTChecker::endVisit(Assignment const& _assignment)
 {
 	if (_assignment.assignmentOperator() != Token::Value::Assign)
@@ -240,7 +251,7 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
 	if (_tuple.isInlineArray() || _tuple.components().size() != 1)
 		m_errorReporter.warning(
 			_tuple.location(),
-			"Assertion checker does not yet implement tules and inline arrays."
+			"Assertion checker does not yet implement tuples and inline arrays."
 		);
 	else
 		defineExpr(_tuple, expr(*_tuple.components()[0]));
@@ -352,18 +363,95 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 
 	std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
 	if (funType.kind() == FunctionType::Kind::Assert)
-	{
-		solAssert(args.size() == 1, "");
-		solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
-		checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
-		addPathImpliedExpression(expr(*args[0]));
-	}
+		visitAssert(_funCall);
 	else if (funType.kind() == FunctionType::Kind::Require)
+		visitRequire(_funCall);
+	else if (funType.kind() == FunctionType::Kind::Internal)
+		inlineFunctionCall(_funCall);
+	else
 	{
-		solAssert(args.size() == 1, "");
-		solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
+		m_errorReporter.warning(
+			_funCall.location(),
+			"Assertion checker does not yet implement this type of function call."
+		);
+	}
+}
+
+void SMTChecker::visitAssert(FunctionCall const& _funCall)
+{
+	auto const& args = _funCall.arguments();
+	solAssert(args.size() == 1, "");
+	solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
+	checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
+	addPathImpliedExpression(expr(*args[0]));
+}
+
+void SMTChecker::visitRequire(FunctionCall const& _funCall)
+{
+	auto const& args = _funCall.arguments();
+	solAssert(args.size() == 1, "");
+	solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
+	if (isRootFunction())
 		checkBooleanNotConstant(*args[0], "Condition is always $VALUE.");
-		addPathImpliedExpression(expr(*args[0]));
+	addPathImpliedExpression(expr(*args[0]));
+}
+
+void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
+{
+	FunctionDefinition const* _funDef = nullptr;
+	Expression const* _calledExpr = &_funCall.expression();
+
+	if (TupleExpression const* _fun = dynamic_cast<TupleExpression const*>(&_funCall.expression()))
+	{
+		solAssert(_fun->components().size() == 1, "");
+		_calledExpr = _fun->components().at(0).get();
+	}
+
+	if (Identifier const* _fun = dynamic_cast<Identifier const*>(_calledExpr))
+		_funDef = dynamic_cast<FunctionDefinition const*>(_fun->annotation().referencedDeclaration);
+	else if (MemberAccess const* _fun = dynamic_cast<MemberAccess const*>(_calledExpr))
+		_funDef = dynamic_cast<FunctionDefinition const*>(_fun->annotation().referencedDeclaration);
+	else
+	{
+		m_errorReporter.warning(
+			_funCall.location(),
+			"Assertion checker does not yet implement this type of function call."
+		);
+		return;
+	}
+	solAssert(_funDef, "");
+
+	if (visitedFunction(_funDef))
+		m_errorReporter.warning(
+			_funCall.location(),
+			"Assertion checker does not support recursive function calls.",
+			SecondarySourceLocation().append("Starting from function:", _funDef->location())
+		);
+	else if (_funDef && _funDef->isImplemented())
+	{
+		vector<smt::Expression> funArgs;
+		for (auto arg: _funCall.arguments())
+			funArgs.push_back(expr(*arg));
+		initializeFunctionCallParameters(*_funDef, funArgs);
+		_funDef->accept(*this);
+		auto const& returnParams = _funDef->returnParameters();
+		if (_funDef->returnParameters().size())
+		{
+			if (returnParams.size() > 1)
+				m_errorReporter.warning(
+					_funCall.location(),
+					"Assertion checker does not yet support calls to functions that return more than one value."
+				);
+			else
+				defineExpr(_funCall, currentValue(*returnParams[0]));
+		}
+	}
+	else
+	{
+		m_errorReporter.warning(
+			_funCall.location(),
+			"Assertion checker does not support calls to functions without implementation."
+		);
 	}
 }
 
@@ -388,6 +476,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 	{
 		if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
 			return;
+		createExpr(_identifier);
 	}
 }
 
@@ -412,6 +501,21 @@ void SMTChecker::endVisit(Literal const& _literal)
 		);
 }
 
+void SMTChecker::endVisit(Return const& _return)
+{
+	if (hasExpr(*_return.expression()))
+	{
+		auto returnParams = m_functionPath.back()->returnParameters();
+		if (returnParams.size() > 1)
+			m_errorReporter.warning(
+				_return.location(),
+				"Assertion checker does not yet support more than one return value."
+			);
+		else if (returnParams.size() == 1)
+			m_interface->addAssertion(expr(*_return.expression()) == newValue(*returnParams[0]));
+	}
+}
+
 void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 {
 	switch (_op.getOperator())
@@ -578,7 +682,7 @@ void SMTChecker::checkCondition(
 
 	vector<smt::Expression> expressionsToEvaluate;
 	vector<string> expressionNames;
-	if (m_currentFunction)
+	if (m_functionPath.size())
 	{
 		if (_additionalValue)
 		{
@@ -607,7 +711,7 @@ void SMTChecker::checkCondition(
 	{
 		std::ostringstream message;
 		message << _description << " happens here";
-		if (m_currentFunction)
+		if (m_functionPath.size())
 		{
 			std::ostringstream modelMessage;
 			modelMessage << "  for:\n";
@@ -723,6 +827,30 @@ smt::CheckResult SMTChecker::checkSatisfiable()
 	return checkSatisfiableAndGenerateModel({}).first;
 }
 
+void SMTChecker::initializeFunctionCallParameters(FunctionDefinition const& _function, vector<smt::Expression> const& _callArgs)
+{
+	auto const& funParams = _function.parameters();
+	solAssert(funParams.size() == _callArgs.size(), "");
+	for (unsigned i = 0; i < funParams.size(); ++i)
+		if (createVariable(*funParams[i]))
+			m_interface->addAssertion(_callArgs[i] == newValue(*funParams[i]));
+
+	for (auto const& variable: _function.localVariables())
+		if (createVariable(*variable))
+		{
+			newValue(*variable);
+			setZeroValue(*variable);
+		}
+
+	if (_function.returnParameterList())
+		for (auto const& retParam: _function.returnParameters())
+			if (createVariable(*retParam))
+			{
+				newValue(*retParam);
+				setZeroValue(*retParam);
+			}
+}
+
 void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
 {
 	for (auto const& variable: _function.localVariables())
@@ -739,6 +867,17 @@ void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
 				setZeroValue(*retParam);
 }
 
+void SMTChecker::removeLocalVariables()
+{
+	for (auto it = m_variables.begin(); it != m_variables.end(); )
+	{
+		if (it->first->isLocalVariable())
+			it = m_variables.erase(it);
+		else
+			++it;
+	}
+}
+
 void SMTChecker::resetStateVariables()
 {
 	for (auto const& variable: m_variables)
@@ -779,7 +918,10 @@ void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _varia
 
 bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 {
-	if (SSAVariable::isSupportedType(_varDecl.type()->category()))
+	// This might be the case for multiple calls to the same function.
+	if (hasVariable(_varDecl))
+		return true;
+	else if (SSAVariable::isSupportedType(_varDecl.type()->category()))
 	{
 		solAssert(m_variables.count(&_varDecl) == 0, "");
 		m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));
@@ -838,40 +980,54 @@ void SMTChecker::setUnknownValue(VariableDeclaration const& _decl)
 
 smt::Expression SMTChecker::expr(Expression const& _e)
 {
-	if (!m_expressions.count(&_e))
+	if (!hasExpr(_e))
 	{
 		m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." );
 		createExpr(_e);
 	}
-	return m_expressions.at(&_e);
+	return prev(m_expressions.upper_bound(&_e))->second;
+}
+
+bool SMTChecker::hasExpr(Expression const& _e) const
+{
+	return m_expressions.count(&_e);
+}
+
+bool SMTChecker::hasVariable(VariableDeclaration const& _var) const
+{
+	return m_variables.count(&_var);
 }
 
 void SMTChecker::createExpr(Expression const& _e)
 {
-	if (m_expressions.count(&_e))
-		m_errorReporter.warning(_e.location(), "Internal error: Expression created twice in SMT solver." );
-	else
+	solAssert(_e.annotation().type, "");
+	string exprSymbol = uniqueSymbol(_e) + "_" + to_string(m_expressions.count(&_e));
+	switch (_e.annotation().type->category())
 	{
-		solAssert(_e.annotation().type, "");
-		switch (_e.annotation().type->category())
-		{
-		case Type::Category::RationalNumber:
-		{
-			if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
-				solAssert(!rational->isFractional(), "");
-			m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
-			break;
-		}
-		case Type::Category::Address:
-		case Type::Category::Integer:
-			m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
-			break;
-		case Type::Category::Bool:
-			m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
-			break;
-		default:
-			solUnimplementedAssert(false, "Type not implemented.");
-		}
+	case Type::Category::RationalNumber:
+	{
+		if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
+			solAssert(!rational->isFractional(), "");
+		m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
+		break;
+	}
+	case Type::Category::Address:
+	case Type::Category::Integer:
+		m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
+		break;
+	case Type::Category::Bool:
+		m_expressions.emplace(&_e, m_interface->newBool(exprSymbol));
+		break;
+	case Type::Category::Function:
+		// This should be replaced by a `non-deterministic` type in the future.
+		m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
+		break;
+	default:
+		m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
+		m_errorReporter.warning(
+			_e.location(),
+			"Assertion checker does not yet implement this type."
+		);
 	}
 }
 
@@ -909,13 +1065,12 @@ void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
 	m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e));
 }
 
-void SMTChecker::removeLocalVariables()
+bool SMTChecker::isRootFunction()
 {
-	for (auto it = m_variables.begin(); it != m_variables.end(); )
-	{
-		if (it->first->isLocalVariable())
-			it = m_variables.erase(it);
-		else
-			++it;
-	}
+	return m_functionPath.size() == 1;
+}
+
+bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef)
+{
+	return contains(m_functionPath, _funDef);
 }
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 6cf4e48a..bef6ea0c 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -59,7 +59,6 @@ private:
 	virtual bool visit(WhileStatement const& _node) override;
 	virtual bool visit(ForStatement const& _node) override;
 	virtual void endVisit(VariableDeclarationStatement const& _node) override;
-	virtual void endVisit(ExpressionStatement const& _node) override;
 	virtual void endVisit(Assignment const& _node) override;
 	virtual void endVisit(TupleExpression const& _node) override;
 	virtual void endVisit(UnaryOperation const& _node) override;
@@ -67,11 +66,18 @@ private:
 	virtual void endVisit(FunctionCall const& _node) override;
 	virtual void endVisit(Identifier const& _node) override;
 	virtual void endVisit(Literal const& _node) override;
+	virtual void endVisit(Return const& _node) override;
 
 	void arithmeticOperation(BinaryOperation const& _op);
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 
+	void visitAssert(FunctionCall const&);
+	void visitRequire(FunctionCall const&);
+	/// Visits the FunctionDefinition of the called function
+	/// if available and inlines the return value.
+	void inlineFunctionCall(FunctionCall const&);
+
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
 	smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
@@ -113,6 +119,7 @@ private:
 	smt::CheckResult checkSatisfiable();
 
 	void initializeLocalVariables(FunctionDefinition const& _function);
+	void initializeFunctionCallParameters(FunctionDefinition const& _function, std::vector<smt::Expression> const& _callArgs);
 	void resetStateVariables();
 	void resetVariables(std::vector<VariableDeclaration const*> _variables);
 	/// Given two different branches and the touched variables,
@@ -147,6 +154,8 @@ private:
 	smt::Expression expr(Expression const& _e);
 	/// Creates the expression (value can be arbitrary)
 	void createExpr(Expression const& _e);
+	/// Checks if expression was created
+	bool hasExpr(Expression const& _e) const;
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smt::Expression _value);
 
@@ -161,18 +170,29 @@ private:
 	/// Add to the solver: the given expression implied by the current path conditions
 	void addPathImpliedExpression(smt::Expression const& _e);
 
-	/// Removes the local variables of a function.
+	/// Removes local variables from the context.
 	void removeLocalVariables();
 
+	/// Checks if VariableDeclaration was seen.
+	bool hasVariable(VariableDeclaration const& _e) const;
+
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::shared_ptr<VariableUsage> m_variableUsage;
 	bool m_loopExecutionHappened = false;
-	std::map<Expression const*, smt::Expression> m_expressions;
+	/// An Expression may have multiple smt::Expression due to
+	/// repeated calls to the same function.
+	std::multimap<Expression const*, smt::Expression> m_expressions;
 	std::map<VariableDeclaration const*, SSAVariable> m_variables;
 	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;
 
-	FunctionDefinition const* m_currentFunction = nullptr;
+	/// Stores the current path of function calls.
+	std::vector<FunctionDefinition const*> m_functionPath;
+	/// Returns true if the current function was not visited by
+	/// a function call.
+	bool isRootFunction();
+	/// Returns true if _funDef was already visited.
+	bool visitedFunction(FunctionDefinition const* _funDef);
 };
 
 }
diff --git a/test/boostTest.cpp b/test/boostTest.cpp
index d27ba1f6..34eeaec9 100644
--- a/test/boostTest.cpp
+++ b/test/boostTest.cpp
@@ -145,6 +145,13 @@ test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] )
 		"yulOptimizerTests",
 		dev::yul::test::YulOptimizerTest::create
 	) > 0, "no Yul Optimizer tests found");
+	if (!dev::test::Options::get().disableSMT)
+		solAssert(registerTests(
+			master,
+			dev::test::Options::get().testPath / "libsolidity",
+			"smtCheckerTests",
+			SyntaxTest::create
+		) > 0, "no SMT checker tests found");
 	if (dev::test::Options::get().disableIPC)
 	{
 		for (auto suite: {
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 1f6f765f..c7e60256 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -137,16 +137,17 @@ BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars)
 {
 	string text = R"(
 		contract C {
-			function f() public {
+			function g() public pure {}
+			function f() public view {
 				uint a = 3;
-				this.f();
+				this.g();
 				assert(a == 3);
-				f();
+				g();
 				assert(a == 3);
 			}
 		}
 	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
+	CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call");
 }
 
 BOOST_AUTO_TEST_CASE(branches_merge_variables)
@@ -569,7 +570,10 @@ BOOST_AUTO_TEST_CASE(constant_condition)
 			}
 		}
 	)";
-	CHECK_WARNING(text, "Condition is always true");
+	CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{
+		"Condition is always true",
+		"Assertion checker does not yet implement this type of function call"
+	}));
 	text = R"(
 		contract C {
 			function f(uint x) public pure {
@@ -577,7 +581,10 @@ BOOST_AUTO_TEST_CASE(constant_condition)
 			}
 		}
 	)";
-	CHECK_WARNING(text, "Condition is always false");
+	CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{
+		"Condition is always false",
+		"Assertion checker does not yet implement this type of function call"
+	}));
 	// a plain literal constant is fine
 	text = R"(
 		contract C {
@@ -586,7 +593,7 @@ BOOST_AUTO_TEST_CASE(constant_condition)
 			}
 		}
 	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
+	CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call");
 }
 
 
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol
new file mode 100644
index 00000000..25a42db6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(42);
+		assert(x > 0);
+	}
+}
+
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol
new file mode 100644
index 00000000..a70aaf61
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(0);
+		assert(x > 0);
+	}
+}
+
+// ----
+// Warning: (161-174): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol
new file mode 100644
index 00000000..aff24b03
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return k(x);
+	}
+
+	function k(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(2);
+		assert(x > 0);
+	}
+}
+
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol
new file mode 100644
index 00000000..9baeb935
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return k(x);
+	}
+
+	function k(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(0);
+		assert(x > 0);
+	}
+}
+
+// ----
+// Warning: (229-242): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol
new file mode 100644
index 00000000..3793f411
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = (h)(42);
+		assert(x > 0);
+	}
+}
+
+// ----
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol
new file mode 100644
index 00000000..e3c80594
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = (h)(0);
+		assert(x > 0);
+	}
+}
+
+// ----
+// Warning: (163-176): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol
new file mode 100644
index 00000000..d2f8ab1d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function g() public {
+		if (a > 0)
+		{
+			a = a - 1;
+			g();
+		}
+		else
+			assert(a == 0);
+	}
+}
+
+// ----
+// Warning: (111-114): Assertion checker does not support recursive function calls.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol
new file mode 100644
index 00000000..d5b83f00
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol
@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f() public {
+		if (a > 0)
+		{
+			a = a - 1;
+			g();
+		}
+		else
+			assert(a == 0);
+	}
+	function g() public {
+		if (a > 0)
+		{
+			a = a - 1;
+			f();
+		}
+		else
+			assert(a == 0);
+	}
+}
+// ----
+// Warning: (206-209): Assertion checker does not support recursive function calls.
+// Warning: (111-114): Assertion checker does not support recursive function calls.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol
new file mode 100644
index 00000000..2f7563dd
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(1);
+		assert(a > 0);
+	}
+}
+
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol
new file mode 100644
index 00000000..ad735768
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol
@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(0);
+		assert(a > 0);
+	}
+}
+
+// ----
+// Warning: (144-157): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol
new file mode 100644
index 00000000..2f95d8af
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(1);
+		f(42);
+		assert(a > 1);
+	}
+}
+
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol
new file mode 100644
index 00000000..5d972f96
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(1);
+		f(0);
+		assert(a > 0);
+	}
+}
+
+// ----
+// Warning: (152-165): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol
new file mode 100644
index 00000000..7693ad81
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { require(x); for (;x;) {} }
+}
+// ----
+// Warning: (98-99): For loop condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol
new file mode 100644
index 00000000..ed1ad73a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { for (;x;) {} }
+	function g() public pure { f(true); }
+}
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol
new file mode 100644
index 00000000..364fe8d1
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function f(bool x) public pure { require(x); if (x) {} }
+}
+// ----
+// Warning: (95-96): Condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol
new file mode 100644
index 00000000..e76badf2
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { x = true; require(x); }
+}
+// ----
+// Warning: (98-99): Condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol
new file mode 100644
index 00000000..5cae940b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { require(x); }
+	function g() public pure { f(true); }
+}
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol
new file mode 100644
index 00000000..66396dd8
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { require(x); while (x) {} }
+}
+// ----
+// Warning: (99-100): While loop condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol
new file mode 100644
index 00000000..5000eeb6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { while (x) {} }
+	function g() public pure { f(true); }
+}
diff --git a/test/tools/isoltest.cpp b/test/tools/isoltest.cpp
index bdc89fb3..1b6fd54a 100644
--- a/test/tools/isoltest.cpp
+++ b/test/tools/isoltest.cpp
@@ -328,6 +328,7 @@ int main(int argc, char *argv[])
 		TestTool::editor = "/usr/bin/editor";
 
 	fs::path testPath;
+	bool disableSMT = false;
 	bool formatted = true;
 	po::options_description options(
 		R"(isoltest, tool for interactively managing test contracts.
@@ -340,6 +341,7 @@ Allowed options)",
 	options.add_options()
 		("help", "Show this help screen.")
 		("testpath", po::value<fs::path>(&testPath), "path to test files")
+		("no-smt", "disable SMT checker")
 		("no-color", "don't use colors")
 		("editor", po::value<string>(&TestTool::editor), "editor for opening contracts");
 
@@ -360,6 +362,9 @@ Allowed options)",
 			formatted = false;
 
 		po::notify(arguments);
+
+		if (arguments.count("no-smt"))
+			disableSMT = true;
 	}
 	catch (std::exception const& _exception)
 	{
@@ -395,6 +400,20 @@ Allowed options)",
 	else
 		return 1;
 
+	if (!disableSMT)
+	{
+		if (auto stats = runTestSuite(
+			"SMT Checker",
+			testPath / "libsolidity",
+			"smtCheckerTests",
+			SyntaxTest::create,
+			formatted
+		))
+			global_stats += *stats;
+		else
+			return 1;
+	}
+
 	cout << endl << "Summary: ";
 	FormattedScope(cout, formatted, {BOLD, global_stats ? GREEN : RED}) <<
 		 global_stats.successCount << "/" << global_stats.testCount;