Merge pull request #5189 from ethereum/smt_function_call

[SMTChecker] Inline calls to internal functions

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``.

libsolidity/formal/SMTChecker.cpp

@@ -71,28 +71,40 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 			_function.location(),
 			"Assertion checker does not yet support constructors and functions with modifiers."
 		);
-	m_currentFunction = &_function;
+	m_functionPath.push_back(&_function);
+	// Not visited by a function call
+	if (isRootFunction())
+	{
 		m_interface->reset();
 		m_pathConditions.clear();
-	m_loopExecutionHappened = false;
+		m_expressions.clear();
 		resetStateVariables();
 		initializeLocalVariables(_function);
+	}
+
+	m_loopExecutionHappened = false;
 	return true;
 }
 
 void SMTChecker::endVisit(FunctionDefinition const&)
 {
-	// TODO we could check for "reachability", i.e. satisfiability here.
+	// If _function was visited from a function call we don't remove
-	// We only handle local variables, so we clear at the beginning of the function.
+	// the local variables just yet, since we might need them for
-	// If we add storage variables, those should be cleared differently.
+	// future calls.
+	// Otherwise we remove any local variables from the context and
+	// keep the state variables.
+	if (isRootFunction())
 		removeLocalVariables();
-	m_currentFunction = nullptr;
+	m_functionPath.pop_back();
 }
 
 bool SMTChecker::visit(IfStatement const& _node)
 {
 	_node.condition().accept(*this);
 
+	// 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()));
@@ -122,11 +134,13 @@ 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);
+		if (isRootFunction())
 			checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE.");
 	}
 	else
 	{
 		_node.condition().accept(*this);
+		if (isRootFunction())
 			checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
 
 		visitBranch(_node.body(), expr(_node.condition()));
@@ -158,6 +172,7 @@ bool SMTChecker::visit(ForStatement const& _node)
 	if (_node.condition())
 	{
 		_node.condition()->accept(*this);
+		if (isRootFunction())
 			checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
 	}
 
@@ -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,19 +363,96 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 
 	std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
 	if (funType.kind() == FunctionType::Kind::Assert)
+		visitAssert(_funCall);
+	else if (funType.kind() == FunctionType::Kind::Require)
+		visitRequire(_funCall);
+	else if (funType.kind() == FunctionType::Kind::Internal)
+		inlineFunctionCall(_funCall);
+	else
 	{
+		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]));
 }
-	else if (funType.kind() == FunctionType::Kind::Require)
+
+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]));
 }
+
+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."
+		);
+	}
 }
 
 void SMTChecker::endVisit(Identifier const& _identifier)
@@ -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())
 	{
 	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)));
+		m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
 		break;
 	}
 	case Type::Category::Address:
 	case Type::Category::Integer:
-			m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
+		m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
 		break;
 	case Type::Category::Bool:
-			m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
+		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:
-			solUnimplementedAssert(false, "Type not implemented.");
+		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(); )
+	return m_functionPath.size() == 1;
+}
+
+bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef)
 {
-		if (it->first->isLocalVariable())
+	return contains(m_functionPath, _funDef);
-			it = m_variables.erase(it);
-		else
-			++it;
-	}
 }

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);
 };
 
 }

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: {

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");
 }
 
 

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);
+	}
+}
+

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

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);
+	}
+}
+

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

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);
+	}
+}
+
+// ----

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

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.

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.

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);
+	}
+}
+

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

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);
+	}
+}
+

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

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.

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); }
+}

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.

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.

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); }
+}

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.

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); }
+}

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;