z3 conditions

10 files changed, 648 insertions, 2 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index da14ddb7..29ca63fe 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -16,6 +16,7 @@ option(SOLC_LINK_STATIC "Link solc executable statically on supported platforms"
 # Let's find our dependencies
 include(EthDependencies)
 include(deps/jsoncpp.cmake)
+include(deps/z3.cmake)
 
 find_package(Threads)
 
diff --git a/cmake/UseSolidity.cmake b/cmake/UseSolidity.cmake
index 5080f71b..9e2dea3e 100644
--- a/cmake/UseSolidity.cmake
+++ b/cmake/UseSolidity.cmake
@@ -25,7 +25,7 @@ function(eth_apply TARGET REQUIRED SUBMODULE)
 
 	if (${SUBMODULE} STREQUAL "solidity" OR ${SUBMODULE} STREQUAL "")
 		eth_use(${TARGET} ${REQUIRED} Dev::soldevcore Solidity::solevmasm)
-		target_link_libraries(${TARGET} ${Solidity_SOLIDITY_LIBRARIES})
+		target_link_libraries(${TARGET} ${Solidity_SOLIDITY_LIBRARIES} z3)
 	endif()
 
 	target_compile_definitions(${TARGET} PUBLIC ETH_SOLIDITY)
diff --git a/deps b/deps
-Subproject e5c8316db8d3daa0abc3b5af8545ce330057608
+Subproject cd9c6ff69134e8f53bde70d92cce12ad294752d
diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt
index 11fd6fe2..a88d16b8 100644
--- a/libsolidity/CMakeLists.txt
+++ b/libsolidity/CMakeLists.txt
@@ -3,4 +3,4 @@ file(GLOB_RECURSE sources "*.cpp" "../libjulia/*.cpp")
 file(GLOB_RECURSE headers "*.h" "../libjulia/*.h")
 
 add_library(solidity ${sources} ${headers})
-target_link_libraries(solidity PUBLIC evmasm devcore)
+target_link_libraries(solidity PUBLIC evmasm devcore z3)
diff --git a/libsolidity/ast/AST.cpp b/libsolidity/ast/AST.cpp
index 605daf55..7f4dea0e 100644
--- a/libsolidity/ast/AST.cpp
+++ b/libsolidity/ast/AST.cpp
@@ -22,6 +22,7 @@
 
 #include <libsolidity/ast/AST.h>
 #include <libsolidity/ast/ASTVisitor.h>
+#include <libsolidity/interface/Exceptions.h>
 #include <libsolidity/ast/AST_accept.h>
 
 #include <libdevcore/SHA3.h>
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
new file mode 100644
index 00000000..0e559fae
--- /dev/null
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -0,0 +1,36 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/formal/SMTChecker.h>
+
+#include <libsolidity/formal/SMTCheckerImpl.h>
+
+#include <libsolidity/interface/ErrorReporter.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+SMTChecker::SMTChecker(ErrorReporter& _errorReporter):
+	m_impl(make_shared<SMTCheckerImpl>(_errorReporter))
+{
+}
+
+void SMTChecker::analyze(SourceUnit const& _source)
+{
+	m_impl->analyze(_source);
+}
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
new file mode 100644
index 00000000..7e7ee3d9
--- /dev/null
+++ b/libsolidity/formal/SMTChecker.h
@@ -0,0 +1,45 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <map>
+#include <string>
+#include <memory>
+
+namespace dev
+{
+namespace solidity
+{
+
+class ErrorReporter;
+class SourceUnit;
+class SMTCheckerImpl;
+
+class SMTChecker
+{
+public:
+	SMTChecker(ErrorReporter& _errorReporter);
+
+	void analyze(SourceUnit const& _sources);
+
+private:
+	std::shared_ptr<SMTCheckerImpl> m_impl;
+};
+
+}
+}
diff --git a/libsolidity/formal/SMTCheckerImpl.cpp b/libsolidity/formal/SMTCheckerImpl.cpp
new file mode 100644
index 00000000..0a9ad66e
--- /dev/null
+++ b/libsolidity/formal/SMTCheckerImpl.cpp
@@ -0,0 +1,456 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/formal/SMTCheckerImpl.h>
+
+
+#include <libsolidity/interface/ErrorReporter.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+SMTCheckerImpl::SMTCheckerImpl(ErrorReporter& _errorReporter):
+	m_solver(m_context),
+	m_errorReporter(_errorReporter)
+{
+}
+
+void SMTCheckerImpl::analyze(SourceUnit const& _source)
+{
+	bool pragmaFound = false;
+	for (auto const& node: _source.nodes())
+		if (auto const* pragma = dynamic_cast<PragmaDirective const*>(node.get()))
+			if (pragma->literals()[0] == "checkAssertionsZ3")
+				pragmaFound = true;
+	if (pragmaFound)
+	{
+		m_solver.reset();
+		m_currentSequenceCounter.clear();
+		_source.accept(*this);
+	}
+}
+
+void SMTCheckerImpl::endVisit(VariableDeclaration const& _varDecl)
+{
+	if (_varDecl.value())
+	{
+		m_errorReporter.warning(
+			_varDecl.location(),
+			"Assertion checker does not yet support this."
+		);
+	}
+	else if (_varDecl.isLocalOrReturn())
+		createVariable(_varDecl, true);
+	else if (_varDecl.isCallableParameter())
+		createVariable(_varDecl, false);
+}
+
+bool SMTCheckerImpl::visit(FunctionDefinition const& _function)
+{
+	if (!_function.modifiers().empty() || _function.isConstructor())
+		m_errorReporter.warning(
+			_function.location(),
+			"Assertion checker does not yet support constructors and functions with modifiers."
+		);
+	// TODO actually we probably also have to reset all local variables and similar things.
+	m_currentFunction = &_function;
+	m_solver.push();
+	return true;
+}
+
+void SMTCheckerImpl::endVisit(FunctionDefinition const&)
+{
+	// TOOD we could check for "reachability", i.e. satisfiability here.
+	m_solver.pop();
+	m_currentFunction = nullptr;
+}
+
+void SMTCheckerImpl::endVisit(VariableDeclarationStatement const& _varDecl)
+{
+	if (_varDecl.declarations().size() != 1)
+		m_errorReporter.warning(
+			_varDecl.location(),
+			"Assertion checker does not yet support such variable declarations."
+		);
+	else if (knownVariable(*_varDecl.declarations()[0]) && _varDecl.initialValue())
+		// TODO more checks?
+		// TODO add restrictions about type (might be assignment from smaller type)
+		m_solver.add(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue()));
+	else
+		m_errorReporter.warning(
+			_varDecl.location(),
+			"Assertion checker does not yet implement such variable declarations."
+		);
+}
+
+void SMTCheckerImpl::endVisit(ExpressionStatement const&)
+{
+}
+
+void SMTCheckerImpl::endVisit(Assignment const& _assignment)
+{
+	if (_assignment.assignmentOperator() != Token::Value::Assign)
+		m_errorReporter.warning(
+			_assignment.location(),
+			"Assertion checker does not yet implement compound assignment."
+		);
+	else if (_assignment.annotation().type->category() != Type::Category::Integer)
+		m_errorReporter.warning(
+			_assignment.location(),
+			"Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
+		);
+	else if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_assignment.leftHandSide()))
+	{
+		Declaration const* decl = identifier->annotation().referencedDeclaration;
+		if (knownVariable(*decl))
+			// TODO more checks?
+			// TODO add restrictions about type (might be assignment from smaller type)
+			m_solver.add(newValue(*decl) == expr(_assignment.rightHandSide()));
+		else
+			m_errorReporter.warning(
+				_assignment.location(),
+				"Assertion checker does not yet implement such assignments."
+			);
+	}
+	else
+		m_errorReporter.warning(
+			_assignment.location(),
+			"Assertion checker does not yet implement such assignments."
+		);
+}
+
+void SMTCheckerImpl::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."
+		);
+	else
+		m_solver.add(expr(_tuple) == expr(*_tuple.components()[0]));
+}
+
+void SMTCheckerImpl::endVisit(BinaryOperation const& _op)
+{
+	if (Token::isArithmeticOp(_op.getOperator()))
+		arithmeticOperation(_op);
+	else if (Token::isCompareOp(_op.getOperator()))
+		compareOperation(_op);
+	else if (Token::isBooleanOp(_op.getOperator()))
+		booleanOperation(_op);
+	else
+		m_errorReporter.warning(
+			_op.location(),
+			"Assertion checker does not yet implement this operator."
+		);
+}
+
+void SMTCheckerImpl::endVisit(FunctionCall const& _funCall)
+{
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+
+	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");
+		m_solver.add(expr(*args[0]));
+	}
+	else if (funType.kind() == FunctionType::Kind::Require)
+	{
+		solAssert(args.size() == 1, "");
+		solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
+		m_solver.add(expr(*args[0]));
+		checkCondition(!(expr(*args[0])), _funCall.location(), "Unreachable code");
+		// TODO is there something meaningful we can check here?
+		// We can check whether the condition is always fulfilled or never fulfilled.
+	}
+}
+
+void SMTCheckerImpl::endVisit(Identifier const& _identifier)
+{
+	Declaration const* decl = _identifier.annotation().referencedDeclaration;
+	solAssert(decl, "");
+	if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
+	{
+		m_solver.add(expr(_identifier) == currentValue(*decl));
+		return;
+	}
+	else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
+	{
+		if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
+			return;
+		// TODO for others, clear our knowledge about storage and memory
+	}
+	m_errorReporter.warning(
+		_identifier.location(),
+		"Assertion checker does not yet support the type of this expression (" +
+		_identifier.annotation().type->toString() +
+		")."
+	);
+}
+
+void SMTCheckerImpl::endVisit(Literal const& _literal)
+{
+	Type const& type = *_literal.annotation().type;
+	if (type.category() == Type::Category::Integer || type.category() == Type::Category::RationalNumber)
+	{
+		if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type))
+			solAssert(!rational->isFractional(), "");
+
+		m_solver.add(expr(_literal) == m_context.int_val(type.literalValue(&_literal).str().c_str()));
+	}
+	else
+		m_errorReporter.warning(
+			_literal.location(),
+			"Assertion checker does not yet support the type of this expression (" +
+			_literal.annotation().type->toString() +
+			")."
+		);
+}
+
+void SMTCheckerImpl::arithmeticOperation(BinaryOperation const& _op)
+{
+	switch (_op.getOperator())
+	{
+	case Token::Add:
+	case Token::Sub:
+	case Token::Mul:
+	{
+		solAssert(_op.annotation().commonType, "");
+		solAssert(_op.annotation().commonType->category() == Type::Category::Integer, "");
+		z3::expr left(expr(_op.leftExpression()));
+		z3::expr right(expr(_op.rightExpression()));
+		Token::Value op = _op.getOperator();
+		z3::expr value(
+			op == Token::Add ? left + right :
+			op == Token::Sub ? left - right :
+			/*op == Token::Mul*/ left * right
+		);
+
+		// Overflow check
+		auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType);
+		checkCondition(
+			value < minValue(intType),
+			_op.location(),
+			"Underflow (resulting value less than " + intType.minValue().str() + ")",
+			"value",
+			&value
+		);
+		checkCondition(
+			value > maxValue(intType),
+			_op.location(),
+			"Overflow (resulting value larger than " + intType.maxValue().str() + ")",
+			"value",
+			&value
+		);
+
+		m_solver.add(expr(_op) == value);
+		break;
+	}
+	default:
+		m_errorReporter.warning(
+			_op.location(),
+			"Assertion checker does not yet implement this operator."
+		);
+	}
+}
+
+void SMTCheckerImpl::compareOperation(BinaryOperation const& _op)
+{
+	solAssert(_op.annotation().commonType, "");
+	if (_op.annotation().commonType->category() == Type::Category::Integer)
+	{
+		z3::expr left(expr(_op.leftExpression()));
+		z3::expr right(expr(_op.rightExpression()));
+		Token::Value op = _op.getOperator();
+		z3::expr value = (
+			op == Token::Equal ? (left == right) :
+			op == Token::NotEqual ? (left != right) :
+			op == Token::LessThan ? (left < right) :
+			op == Token::LessThanOrEqual ? (left <= right) :
+			op == Token::GreaterThan ? (left > right) :
+			/*op == Token::GreaterThanOrEqual*/ (left >= right)
+		);
+		// TODO: check that other values for op are not possible.
+		m_solver.add(expr(_op) == value);
+	}
+	else
+		m_errorReporter.warning(
+			_op.location(),
+			"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for comparisons"
+		);
+}
+
+void SMTCheckerImpl::booleanOperation(BinaryOperation const& _op)
+{
+	solAssert(_op.getOperator() == Token::And || _op.getOperator() == Token::Or, "");
+	solAssert(_op.annotation().commonType, "");
+	if (_op.annotation().commonType->category() == Type::Category::Bool)
+	{
+		if (_op.getOperator() == Token::And)
+			m_solver.add(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression()));
+		else
+			m_solver.add(expr(_op) == expr(_op.leftExpression()) || expr(_op.rightExpression()));
+	}
+	else
+		m_errorReporter.warning(
+			_op.location(),
+			"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for boolean operations"
+		);
+}
+
+void SMTCheckerImpl::checkCondition(
+	z3::expr _condition,
+	SourceLocation const& _location,
+	string const& _description,
+	string const& _additionalValueName,
+	z3::expr* _additionalValue
+)
+{
+	m_solver.push();
+	m_solver.add(_condition);
+	switch (m_solver.check())
+	{
+	case z3::check_result::sat:
+	{
+		std::ostringstream message;
+		message << _description << " happens here";
+		if (m_currentFunction)
+		{
+			message << " for:\n";
+			z3::model m = m_solver.get_model();
+			if (_additionalValue)
+				message << "  " << _additionalValueName << " = " << m.eval(*_additionalValue) << "\n";
+			for (auto const& param: m_currentFunction->parameters())
+				if (knownVariable(*param))
+					message << "  " << param->name() << " = " << m.eval(currentValue(*param)) << "\n";
+			for (auto const& var: m_currentFunction->localVariables())
+				if (knownVariable(*var))
+					message << "  " << var->name() << " = " << m.eval(currentValue(*var)) << "\n";
+//			message << m << endl;
+//			message << m_solver << endl;
+		}
+		else
+			message << ".";
+		m_errorReporter.warning(_location, message.str());
+		break;
+	}
+	case z3::check_result::unsat:
+		break;
+	case z3::check_result::unknown:
+		m_errorReporter.warning(_location, _description + " might happen here.");
+		break;
+	}
+	m_solver.pop();
+}
+
+void SMTCheckerImpl::createVariable(VariableDeclaration const& _varDecl, bool _setToZero)
+{
+	if (auto intType = dynamic_cast<IntegerType const*>(_varDecl.type().get()))
+	{
+		solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
+		solAssert(m_z3Variables.count(&_varDecl) == 0, "");
+		m_currentSequenceCounter[&_varDecl] = 0;
+		m_z3Variables.emplace(&_varDecl, m_context.function(uniqueSymbol(_varDecl).c_str(), m_context.int_sort(), m_context.int_sort()));
+		if (_setToZero)
+			m_solver.add(currentValue(_varDecl) == 0);
+		else
+		{
+			m_solver.add(currentValue(_varDecl) >= minValue(*intType));
+			m_solver.add(currentValue(_varDecl) <= maxValue(*intType));
+		}
+	}
+	else
+		m_errorReporter.warning(
+			_varDecl.location(),
+			"Assertion checker does not yet support the type of this variable."
+		);
+}
+
+string SMTCheckerImpl::uniqueSymbol(Declaration const& _decl)
+{
+	return _decl.name() + "_" + to_string(_decl.id());
+}
+
+string SMTCheckerImpl::uniqueSymbol(Expression const& _expr)
+{
+	return "expr_" + to_string(_expr.id());
+}
+
+bool SMTCheckerImpl::knownVariable(Declaration const& _decl)
+{
+	return m_currentSequenceCounter.count(&_decl);
+}
+
+z3::expr SMTCheckerImpl::currentValue(Declaration const& _decl)
+{
+	solAssert(m_currentSequenceCounter.count(&_decl), "");
+	return var(_decl)(m_currentSequenceCounter.at(&_decl));
+}
+
+z3::expr SMTCheckerImpl::newValue(const Declaration& _decl)
+{
+	solAssert(m_currentSequenceCounter.count(&_decl), "");
+	m_currentSequenceCounter[&_decl]++;
+	return currentValue(_decl);
+}
+
+z3::expr SMTCheckerImpl::minValue(IntegerType const& _t)
+{
+	return m_context.int_val(_t.minValue().str().c_str());
+}
+
+z3::expr SMTCheckerImpl::maxValue(IntegerType const& _t)
+{
+	return m_context.int_val(_t.maxValue().str().c_str());
+}
+
+z3::expr SMTCheckerImpl::expr(Expression const& _e)
+{
+	if (!m_z3Expressions.count(&_e))
+	{
+		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_z3Expressions.emplace(&_e, m_context.int_const(uniqueSymbol(_e).c_str()));
+			break;
+		}
+		case Type::Category::Integer:
+			m_z3Expressions.emplace(&_e, m_context.int_const(uniqueSymbol(_e).c_str()));
+			break;
+		case Type::Category::Bool:
+			m_z3Expressions.emplace(&_e, m_context.bool_const(uniqueSymbol(_e).c_str()));
+			break;
+		default:
+			solAssert(false, "Type not implemented.");
+		}
+	}
+	return m_z3Expressions.at(&_e);
+}
+
+z3::func_decl SMTCheckerImpl::var(Declaration const& _decl)
+{
+	solAssert(m_z3Variables.count(&_decl), "");
+	return m_z3Variables.at(&_decl);
+}
diff --git a/libsolidity/formal/SMTCheckerImpl.h b/libsolidity/formal/SMTCheckerImpl.h
new file mode 100644
index 00000000..a82ec92a
--- /dev/null
+++ b/libsolidity/formal/SMTCheckerImpl.h
@@ -0,0 +1,99 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <libsolidity/ast/ASTVisitor.h>
+
+#include <z3++.h>
+
+#include <map>
+#include <string>
+
+namespace dev
+{
+namespace solidity
+{
+
+class ErrorReporter;
+
+class SMTCheckerImpl: private ASTConstVisitor
+{
+public:
+	SMTCheckerImpl(ErrorReporter& _errorReporter);
+
+	void analyze(SourceUnit const& _sources);
+
+private:
+	// TODO: Check that we do not have concurrent reads and writes to a variable,
+	// because the order of expression evaluation is undefined
+	// TODO: or just force a certain order, but people might have a different idea about that.
+
+	virtual void endVisit(VariableDeclaration const& _node) override;
+	virtual bool visit(FunctionDefinition const& _node) override;
+	virtual void endVisit(FunctionDefinition 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(BinaryOperation const& _node) override;
+	virtual void endVisit(FunctionCall const& _node) override;
+	virtual void endVisit(Identifier const& _node) override;
+	virtual void endVisit(Literal const& _node) override;
+
+	void arithmeticOperation(BinaryOperation const& _op);
+	void compareOperation(BinaryOperation const& _op);
+	void booleanOperation(BinaryOperation const& _op);
+
+	void checkCondition(
+		z3::expr _condition,
+		SourceLocation const& _location,
+		std::string const& _description,
+		std::string const& _additionalValueName = "",
+		z3::expr* _additionalValue = nullptr
+	);
+
+	void createVariable(VariableDeclaration const& _varDecl, bool _setToZero);
+
+	std::string uniqueSymbol(Declaration const& _decl);
+	std::string uniqueSymbol(Expression const& _expr);
+	bool knownVariable(Declaration const& _decl);
+	z3::expr currentValue(Declaration const& _decl);
+	z3::expr newValue(Declaration const& _decl);
+
+	z3::expr minValue(IntegerType const& _t);
+	z3::expr maxValue(IntegerType const& _t);
+
+	/// Returns the z3 expression corresponding to the AST node. Creates a new expression
+	/// if it does not exist yet.
+	z3::expr expr(Expression const& _e);
+	/// Returns the z3 function declaration corresponding to the given variable.
+	/// The function takes one argument which is the "sequence number".
+	z3::func_decl var(Declaration const& _decl);
+
+	z3::context m_context;
+	z3::solver m_solver;
+	std::map<Declaration const*, int> m_currentSequenceCounter;
+	std::map<Expression const*, z3::expr> m_z3Expressions;
+	std::map<Declaration const*, z3::func_decl> m_z3Variables;
+	ErrorReporter& m_errorReporter;
+
+	FunctionDefinition const* m_currentFunction = nullptr;
+};
+
+}
+}
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index 412d2fd3..4283cd99 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -37,6 +37,7 @@
 #include <libsolidity/analysis/PostTypeChecker.h>
 #include <libsolidity/analysis/SyntaxChecker.h>
 #include <libsolidity/codegen/Compiler.h>
+#include <libsolidity/formal/SMTChecker.h>
 #include <libsolidity/interface/ABI.h>
 #include <libsolidity/interface/Natspec.h>
 #include <libsolidity/interface/GasEstimator.h>
@@ -238,6 +239,13 @@ bool CompilerStack::analyze()
 
 	if (noErrors)
 	{
+		SMTChecker smtChecker(m_errorReporter);
+		for (Source const* source: m_sourceOrder)
+			smtChecker.analyze(*source->ast);
+	}
+
+	if (noErrors)
+	{
 		m_stackState = AnalysisSuccessful;
 		return true;
 	}