Merge pull request #2538 from ethereum/z3Conditions

z3 conditions

21 files changed, 1503 insertions, 52 deletions

diff --git a/Changelog.md b/Changelog.md
index efcea03f..ed004d8c 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -2,6 +2,7 @@
 
 Features:
  * ABI JSON: Include new field ``statemutability`` with values ``view``, ``nonpayable`` and ``payable``.
+ * Analyzer: Experimental partial support for Z3 SMT checker.
  * Parser: Display previous visibility specifier in error if multiple are found.
  * Parser: Introduce ``view`` keyword on functions (``constant`` remains an alias for ``view``).
  * Syntax Checker: Support ``pragma experimental <feature>;`` to turn on experimental features.
diff --git a/cmake/FindZ3.cmake b/cmake/FindZ3.cmake
new file mode 100644
index 00000000..8f3f9ee1
--- /dev/null
+++ b/cmake/FindZ3.cmake
@@ -0,0 +1,9 @@
+find_path(Z3_INCLUDE_DIR z3++.h)
+find_library(Z3_LIBRARY NAMES z3 )
+include(${CMAKE_CURRENT_LIST_DIR}/FindPackageHandleStandardArgs.cmake)
+FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3 DEFAULT_MSG Z3_LIBRARY Z3_INCLUDE_DIR)
+
+if(Z3_FOUND)
+  set(Z3_LIBRARIES ${Z3_LIBRARY})
+endif()
+
diff --git a/libdevcore/CommonData.h b/libdevcore/CommonData.h
index 0321011e..5df8986a 100644
--- a/libdevcore/CommonData.h
+++ b/libdevcore/CommonData.h
@@ -145,6 +145,17 @@ inline std::string toHex(u256 val, HexPrefix prefix = HexPrefix::DontAdd)
 	return (prefix == HexPrefix::Add) ? "0x" + str : str;
 }
 
+/// Returns decimal representation for small numbers and hex for large numbers.
+inline std::string formatNumber(bigint const& _value)
+{
+	if (_value < 0)
+		return "-" + formatNumber(-_value);
+	if (_value > 0x1000000)
+		return toHex(toCompactBigEndian(_value), 2, HexPrefix::Add);
+	else
+		return _value.str();
+}
+
 inline std::string toCompactHexWithPrefix(u256 val)
 {
 	std::ostringstream ret;
diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt
index 11fd6fe2..f7c1a390 100644
--- a/libsolidity/CMakeLists.txt
+++ b/libsolidity/CMakeLists.txt
@@ -2,5 +2,19 @@
 file(GLOB_RECURSE sources "*.cpp" "../libjulia/*.cpp")
 file(GLOB_RECURSE headers "*.h" "../libjulia/*.h")
 
+find_package(Z3 QUIET)
+if (${Z3_FOUND})
+  include_directories(${Z3_INCLUDE_DIR})
+  add_definitions(-DHAVE_Z3)
+  message("Z3 SMT solver FOUND.")
+else()
+  message("Z3 SMT solver NOT found.")
+  list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/Z3Interface.cpp")
+endif()
+
 add_library(solidity ${sources} ${headers})
 target_link_libraries(solidity PUBLIC evmasm devcore)
+
+if (${Z3_FOUND})
+  target_link_libraries(solidity PUBLIC ${Z3_LIBRARY})
+endif()
\ No newline at end of file
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/ast/ExperimentalFeatures.h b/libsolidity/ast/ExperimentalFeatures.h
index 0c03ea4a..2c089671 100644
--- a/libsolidity/ast/ExperimentalFeatures.h
+++ b/libsolidity/ast/ExperimentalFeatures.h
@@ -29,6 +29,7 @@ namespace solidity
 
 enum class ExperimentalFeature
 {
+	SMTChecker,
 	ABIEncoderV2, // new ABI encoder that makes use of JULIA
 	Test,
 	TestOnlyAnalysis
@@ -36,11 +37,13 @@ enum class ExperimentalFeature
 
 static const std::map<ExperimentalFeature, bool> ExperimentalFeatureOnlyAnalysis =
 {
+	{ ExperimentalFeature::SMTChecker, true },
 	{ ExperimentalFeature::TestOnlyAnalysis, true },
 };
 
 static const std::map<std::string, ExperimentalFeature> ExperimentalFeatureNames =
 {
+	{ "SMTChecker", ExperimentalFeature::SMTChecker },
 	{ "ABIEncoderV2", ExperimentalFeature::ABIEncoderV2 },
 	{ "__test", ExperimentalFeature::Test },
 	{ "__testOnlyAnalysis", ExperimentalFeature::TestOnlyAnalysis },
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
new file mode 100644
index 00000000..fd78e578
--- /dev/null
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -0,0 +1,588 @@
+/*
+	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>
+
+#ifdef HAVE_Z3
+#include <libsolidity/formal/Z3Interface.h>
+#else
+#include <libsolidity/formal/SMTLib2Interface.h>
+#endif
+
+#include <libsolidity/interface/ErrorReporter.h>
+
+#include <boost/range/adaptor/map.hpp>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
+#ifdef HAVE_Z3
+	m_interface(make_shared<smt::Z3Interface>()),
+#else
+	m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)),
+#endif
+	m_errorReporter(_errorReporter)
+{
+	(void)_readFileCallback;
+}
+
+void SMTChecker::analyze(SourceUnit const& _source)
+{
+	if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
+	{
+		m_interface->reset();
+		m_currentSequenceCounter.clear();
+		m_nextFreeSequenceCounter.clear();
+		_source.accept(*this);
+	}
+}
+
+void SMTChecker::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 SMTChecker::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_interface->push();
+	return true;
+}
+
+void SMTChecker::endVisit(FunctionDefinition const&)
+{
+	// TOOD we could check for "reachability", i.e. satisfiability here.
+	// We only handle local variables, so we clear everything.
+	// If we add storage variables, those should be cleared differently.
+	m_currentSequenceCounter.clear();
+	m_nextFreeSequenceCounter.clear();
+	m_interface->pop();
+	m_currentFunction = nullptr;
+}
+
+bool SMTChecker::visit(IfStatement const& _node)
+{
+	_node.condition().accept(*this);
+
+	// TODO Check if condition is always true
+
+	auto countersAtStart = m_currentSequenceCounter;
+	m_interface->push();
+	m_interface->addAssertion(expr(_node.condition()));
+	_node.trueStatement().accept(*this);
+	auto countersAtEndOfTrue = m_currentSequenceCounter;
+	m_interface->pop();
+
+	decltype(m_currentSequenceCounter) countersAtEndOfFalse;
+	if (_node.falseStatement())
+	{
+		m_currentSequenceCounter = countersAtStart;
+		m_interface->push();
+		m_interface->addAssertion(!expr(_node.condition()));
+		_node.falseStatement()->accept(*this);
+		countersAtEndOfFalse = m_currentSequenceCounter;
+		m_interface->pop();
+	}
+	else
+		countersAtEndOfFalse = countersAtStart;
+
+	// Reset all values that have been touched.
+
+	// TODO this should use a previously generated side-effect structure
+
+	solAssert(countersAtEndOfFalse.size() == countersAtEndOfTrue.size(), "");
+	for (auto const& declCounter: countersAtEndOfTrue)
+	{
+		solAssert(countersAtEndOfFalse.count(declCounter.first), "");
+		auto decl = declCounter.first;
+		int trueCounter = countersAtEndOfTrue.at(decl);
+		int falseCounter = countersAtEndOfFalse.at(decl);
+		if (trueCounter == falseCounter)
+			continue; // Was not modified
+		newValue(*decl);
+		setValue(*decl, 0);
+	}
+	return false;
+}
+
+bool SMTChecker::visit(WhileStatement const& _node)
+{
+	_node.condition().accept(*this);
+
+	//m_interface->push();
+	//m_interface->addAssertion(expr(_node.condition()));
+	// TDOO clear knowledge (increment sequence numbers and add bounds assertions	) apart from assertions
+
+	// TODO combine similar to if
+	return true;
+}
+
+void SMTChecker::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]))
+	{
+		if (_varDecl.initialValue())
+			// TODO more checks?
+			// TODO add restrictions about type (might be assignment from smaller type)
+			m_interface->addAssertion(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue()));
+	}
+	else
+		m_errorReporter.warning(
+			_varDecl.location(),
+			"Assertion checker does not yet implement such variable declarations."
+		);
+}
+
+void SMTChecker::endVisit(ExpressionStatement const&)
+{
+}
+
+void SMTChecker::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_interface->addAssertion(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 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."
+		);
+	else
+		m_interface->addAssertion(expr(_tuple) == expr(*_tuple.components()[0]));
+}
+
+void SMTChecker::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 SMTChecker::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_interface->addAssertion(expr(*args[0]));
+	}
+	else if (funType.kind() == FunctionType::Kind::Require)
+	{
+		solAssert(args.size() == 1, "");
+		solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
+		m_interface->addAssertion(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 SMTChecker::endVisit(Identifier const& _identifier)
+{
+	Declaration const* decl = _identifier.annotation().referencedDeclaration;
+	solAssert(decl, "");
+	if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
+	{
+		m_interface->addAssertion(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 SMTChecker::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_interface->addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal)));
+	}
+	else
+		m_errorReporter.warning(
+			_literal.location(),
+			"Assertion checker does not yet support the type of this expression (" +
+			_literal.annotation().type->toString() +
+			")."
+		);
+}
+
+void SMTChecker::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, "");
+		smt::Expression left(expr(_op.leftExpression()));
+		smt::Expression right(expr(_op.rightExpression()));
+		Token::Value op = _op.getOperator();
+		smt::Expression 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 " + formatNumber(intType.minValue()) + ")",
+			"value",
+			&value
+		);
+		checkCondition(
+			value > maxValue(intType),
+			_op.location(),
+			"Overflow (resulting value larger than " + formatNumber(intType.maxValue()) + ")",
+			"value",
+			&value
+		);
+
+		m_interface->addAssertion(expr(_op) == value);
+		break;
+	}
+	default:
+		m_errorReporter.warning(
+			_op.location(),
+			"Assertion checker does not yet implement this operator."
+		);
+	}
+}
+
+void SMTChecker::compareOperation(BinaryOperation const& _op)
+{
+	solAssert(_op.annotation().commonType, "");
+	if (_op.annotation().commonType->category() == Type::Category::Integer)
+	{
+		smt::Expression left(expr(_op.leftExpression()));
+		smt::Expression right(expr(_op.rightExpression()));
+		Token::Value op = _op.getOperator();
+		smt::Expression 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_interface->addAssertion(expr(_op) == value);
+	}
+	else
+		m_errorReporter.warning(
+			_op.location(),
+			"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for comparisons"
+		);
+}
+
+void SMTChecker::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_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression()));
+		else
+			m_interface->addAssertion(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 SMTChecker::checkCondition(
+	smt::Expression _condition,
+	SourceLocation const& _location,
+	string const& _description,
+	string const& _additionalValueName,
+	smt::Expression* _additionalValue
+)
+{
+	m_interface->push();
+	m_interface->addAssertion(_condition);
+
+	vector<smt::Expression> expressionsToEvaluate;
+	vector<string> expressionNames;
+	if (m_currentFunction)
+	{
+		if (_additionalValue)
+		{
+			expressionsToEvaluate.emplace_back(*_additionalValue);
+			expressionNames.push_back(_additionalValueName);
+		}
+		for (auto const& param: m_currentFunction->parameters())
+			if (knownVariable(*param))
+			{
+				expressionsToEvaluate.emplace_back(currentValue(*param));
+				expressionNames.push_back(param->name());
+			}
+		for (auto const& var: m_currentFunction->localVariables())
+			if (knownVariable(*var))
+			{
+				expressionsToEvaluate.emplace_back(currentValue(*var));
+				expressionNames.push_back(var->name());
+			}
+	}
+	smt::CheckResult result;
+	vector<string> values;
+	try
+	{
+		tie(result, values) = m_interface->check(expressionsToEvaluate);
+	}
+	catch (smt::SolverError const& _e)
+	{
+		string description("Error querying SMT solver");
+		if (_e.comment())
+			description += ": " + *_e.comment();
+		m_errorReporter.warning(_location, description);
+		return;
+	}
+
+	switch (result)
+	{
+	case smt::CheckResult::SATISFIABLE:
+	{
+		std::ostringstream message;
+		message << _description << " happens here";
+		if (m_currentFunction)
+		{
+			message << " for:\n";
+			solAssert(values.size() == expressionNames.size(), "");
+			for (size_t i = 0; i < values.size(); ++i)
+			{
+				string formattedValue = values.at(i);
+				try
+				{
+					// Parse and re-format nicely
+					formattedValue = formatNumber(bigint(formattedValue));
+				}
+				catch (...) { }
+
+				message << "  " << expressionNames.at(i) << " = " << formattedValue << "\n";
+			}
+		}
+		else
+			message << ".";
+		m_errorReporter.warning(_location, message.str());
+		break;
+	}
+	case smt::CheckResult::UNSATISFIABLE:
+		break;
+	case smt::CheckResult::UNKNOWN:
+		m_errorReporter.warning(_location, _description + " might happen here.");
+		break;
+	case smt::CheckResult::ERROR:
+		m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
+		break;
+	default:
+		solAssert(false, "");
+	}
+	m_interface->pop();
+}
+
+void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setToZero)
+{
+	if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
+	{
+		solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
+		solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, "");
+		solAssert(m_Variables.count(&_varDecl) == 0, "");
+		m_currentSequenceCounter[&_varDecl] = 0;
+		m_nextFreeSequenceCounter[&_varDecl] = 1;
+		m_Variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
+		setValue(_varDecl, _setToZero);
+	}
+	else
+		m_errorReporter.warning(
+			_varDecl.location(),
+			"Assertion checker does not yet support the type of this variable."
+		);
+}
+
+string SMTChecker::uniqueSymbol(Declaration const& _decl)
+{
+	return _decl.name() + "_" + to_string(_decl.id());
+}
+
+string SMTChecker::uniqueSymbol(Expression const& _expr)
+{
+	return "expr_" + to_string(_expr.id());
+}
+
+bool SMTChecker::knownVariable(Declaration const& _decl)
+{
+	return m_currentSequenceCounter.count(&_decl);
+}
+
+smt::Expression SMTChecker::currentValue(Declaration const& _decl)
+{
+	solAssert(m_currentSequenceCounter.count(&_decl), "");
+	return valueAtSequence(_decl, m_currentSequenceCounter.at(&_decl));
+}
+
+smt::Expression SMTChecker::valueAtSequence(const Declaration& _decl, int _sequence)
+{
+	return var(_decl)(_sequence);
+}
+
+smt::Expression SMTChecker::newValue(Declaration const& _decl)
+{
+	solAssert(m_currentSequenceCounter.count(&_decl), "");
+	solAssert(m_nextFreeSequenceCounter.count(&_decl), "");
+	m_currentSequenceCounter[&_decl] = m_nextFreeSequenceCounter[&_decl]++;
+	return currentValue(_decl);
+}
+
+void SMTChecker::setValue(Declaration const& _decl, bool _setToZero)
+{
+	auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type());
+
+	if (_setToZero)
+		m_interface->addAssertion(currentValue(_decl) == 0);
+	else
+	{
+		m_interface->addAssertion(currentValue(_decl) >= minValue(intType));
+		m_interface->addAssertion(currentValue(_decl) <= maxValue(intType));
+	}
+}
+
+smt::Expression SMTChecker::minValue(IntegerType const& _t)
+{
+	return smt::Expression(_t.minValue());
+}
+
+smt::Expression SMTChecker::maxValue(IntegerType const& _t)
+{
+	return smt::Expression(_t.maxValue());
+}
+
+smt::Expression SMTChecker::expr(Expression const& _e)
+{
+	if (!m_Expressions.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_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
+			break;
+		}
+		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:
+			solAssert(false, "Type not implemented.");
+		}
+	}
+	return m_Expressions.at(&_e);
+}
+
+smt::Expression SMTChecker::var(Declaration const& _decl)
+{
+	solAssert(m_Variables.count(&_decl), "");
+	return m_Variables.at(&_decl);
+}
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
new file mode 100644
index 00000000..d23fd201
--- /dev/null
+++ b/libsolidity/formal/SMTChecker.h
@@ -0,0 +1,114 @@
+/*
+	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 <libsolidity/formal/SolverInterface.h>
+#include <libsolidity/interface/ReadFile.h>
+
+#include <map>
+#include <string>
+
+namespace dev
+{
+namespace solidity
+{
+
+class ErrorReporter;
+
+class SMTChecker: private ASTConstVisitor
+{
+public:
+	SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback);
+
+	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 bool visit(IfStatement const& _node) override;
+	virtual bool visit(WhileStatement 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(
+		smt::Expression _condition,
+		SourceLocation const& _location,
+		std::string const& _description,
+		std::string const& _additionalValueName = "",
+		smt::Expression* _additionalValue = nullptr
+	);
+
+	void createVariable(VariableDeclaration const& _varDecl, bool _setToZero);
+
+	static std::string uniqueSymbol(Declaration const& _decl);
+	static std::string uniqueSymbol(Expression const& _expr);
+
+	/// @returns true if _delc is a variable that is known at the current point, i.e.
+	/// has a valid sequence number
+	bool knownVariable(Declaration const& _decl);
+	/// @returns an expression denoting the value of the variable declared in @a _decl
+	/// at the current point.
+	smt::Expression currentValue(Declaration const& _decl);
+	/// @returns an expression denoting the value of the variable declared in @a _decl
+	/// at the given sequence point. Does not ensure that this sequence point exists.
+	smt::Expression valueAtSequence(Declaration const& _decl, int _sequence);
+	/// Allocates a new sequence number for the declaration, updates the current
+	/// sequence number to this value and returns the expression.
+	smt::Expression newValue(Declaration const& _decl);
+
+	/// Sets the value of the declaration either to zero or to its intrinsic range.
+	void setValue(Declaration const& _decl, bool _setToZero);
+
+	static smt::Expression minValue(IntegerType const& _t);
+	static smt::Expression maxValue(IntegerType const& _t);
+
+	/// Returns the expression corresponding to the AST node. Creates a new expression
+	/// if it does not exist yet.
+	smt::Expression expr(Expression const& _e);
+	/// Returns the function declaration corresponding to the given variable.
+	/// The function takes one argument which is the "sequence number".
+	smt::Expression var(Declaration const& _decl);
+
+	std::shared_ptr<smt::SolverInterface> m_interface;
+	std::map<Declaration const*, int> m_currentSequenceCounter;
+	std::map<Declaration const*, int> m_nextFreeSequenceCounter;
+	std::map<Expression const*, smt::Expression> m_Expressions;
+	std::map<Declaration const*, smt::Expression> m_Variables;
+	ErrorReporter& m_errorReporter;
+
+	FunctionDefinition const* m_currentFunction = nullptr;
+};
+
+}
+}
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
new file mode 100644
index 00000000..cbd766fb
--- /dev/null
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -0,0 +1,187 @@
+/*
+	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/SMTLib2Interface.h>
+
+#include <libsolidity/interface/Exceptions.h>
+#include <libsolidity/interface/ReadFile.h>
+
+#include <boost/algorithm/string/predicate.hpp>
+#include <boost/algorithm/string/join.hpp>
+#include <boost/filesystem/operations.hpp>
+
+#include <cstdio>
+#include <fstream>
+#include <iostream>
+#include <memory>
+#include <stdexcept>
+#include <string>
+#include <array>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+using namespace dev::solidity::smt;
+
+SMTLib2Interface::SMTLib2Interface(ReadCallback::Callback const& _queryCallback):
+	m_queryCallback(_queryCallback)
+{
+	reset();
+}
+
+void SMTLib2Interface::reset()
+{
+	m_accumulatedOutput.clear();
+	m_accumulatedOutput.emplace_back();
+	write("(set-option :produce-models true)");
+	write("(set-logic QF_UFLIA)");
+}
+
+void SMTLib2Interface::push()
+{
+	m_accumulatedOutput.emplace_back();
+}
+
+void SMTLib2Interface::pop()
+{
+	solAssert(!m_accumulatedOutput.empty(), "");
+	m_accumulatedOutput.pop_back();
+}
+
+Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain)
+{
+	write(
+		"(declare-fun |" +
+		_name +
+		"| (" +
+		(_domain == Sort::Int ? "Int" : "Bool") +
+		") " +
+		(_codomain == Sort::Int ? "Int" : "Bool") +
+		")"
+	);
+	return SolverInterface::newFunction(move(_name), _domain, _codomain);
+}
+
+Expression SMTLib2Interface::newInteger(string _name)
+{
+	write("(declare-const |" + _name + "| Int)");
+	return SolverInterface::newInteger(move(_name));
+}
+
+Expression SMTLib2Interface::newBool(string _name)
+{
+	write("(declare-const |" + _name + "| Bool)");
+	return SolverInterface::newBool(std::move(_name));
+}
+
+void SMTLib2Interface::addAssertion(Expression const& _expr)
+{
+	write("(assert " + toSExpr(_expr) + ")");
+}
+
+pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate)
+{
+	string response = querySolver(
+		boost::algorithm::join(m_accumulatedOutput, "\n") +
+		checkSatAndGetValuesCommand(_expressionsToEvaluate)
+	);
+
+	CheckResult result;
+	// TODO proper parsing
+	if (boost::starts_with(response, "sat\n"))
+		result = CheckResult::SATISFIABLE;
+	else if (boost::starts_with(response, "unsat\n"))
+		result = CheckResult::UNSATISFIABLE;
+	else if (boost::starts_with(response, "unknown\n"))
+		result = CheckResult::UNKNOWN;
+	else
+		result = CheckResult::ERROR;
+
+	vector<string> values;
+	if (result != CheckResult::UNSATISFIABLE && result != CheckResult::ERROR)
+		values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend());
+	return make_pair(result, values);
+}
+
+string SMTLib2Interface::toSExpr(Expression const& _expr)
+{
+	if (_expr.arguments.empty())
+		return _expr.name;
+	std::string sexpr = "(" + _expr.name;
+	for (auto const& arg: _expr.arguments)
+		sexpr += " " + toSExpr(arg);
+	sexpr += ")";
+	return sexpr;
+}
+
+void SMTLib2Interface::write(string _data)
+{
+	solAssert(!m_accumulatedOutput.empty(), "");
+	m_accumulatedOutput.back() += move(_data) + "\n";
+}
+
+string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _expressionsToEvaluate)
+{
+	string command;
+	if (_expressionsToEvaluate.empty())
+		command = "(check-sat)\n";
+	else
+	{
+		// TODO make sure these are unique
+		for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
+		{
+			auto const& e = _expressionsToEvaluate.at(i);
+			// TODO they don't have to be ints...
+			command += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n";
+			command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
+		}
+		command += "(check-sat)\n";
+		command += "(get-value (";
+		for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
+			command += "|EVALEXPR_" + to_string(i) + "| ";
+		command += "))\n";
+	}
+
+	return command;
+}
+
+vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, string::const_iterator _end)
+{
+	vector<string> values;
+	while (_start < _end)
+	{
+		auto valStart = find(_start, _end, ' ');
+		if (valStart < _end)
+			++valStart;
+		auto valEnd = find(valStart, _end, ')');
+		values.emplace_back(valStart, valEnd);
+		_start = find(valEnd, _end, '(');
+	}
+
+	return values;
+}
+
+string SMTLib2Interface::querySolver(string const& _input)
+{
+	if (!m_queryCallback)
+		BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment("No SMT solver available."));
+
+	ReadCallback::Result queryResult = m_queryCallback(_input);
+	if (!queryResult.success)
+		BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment(queryResult.responseOrErrorMessage));
+	return queryResult.responseOrErrorMessage;
+}
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
new file mode 100644
index 00000000..b8dac366
--- /dev/null
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -0,0 +1,75 @@
+/*
+	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/formal/SolverInterface.h>
+
+#include <libsolidity/interface/Exceptions.h>
+#include <libsolidity/interface/ReadFile.h>
+
+#include <libdevcore/Common.h>
+
+#include <boost/noncopyable.hpp>
+
+#include <map>
+#include <string>
+#include <vector>
+#include <cstdio>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+class SMTLib2Interface: public SolverInterface, public boost::noncopyable
+{
+public:
+	SMTLib2Interface(ReadCallback::Callback const& _queryCallback);
+
+	void reset() override;
+
+	void push() override;
+	void pop() override;
+
+	Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override;
+	Expression newInteger(std::string _name) override;
+	Expression newBool(std::string _name) override;
+
+	void addAssertion(Expression const& _expr) override;
+	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
+
+private:
+	std::string toSExpr(Expression const& _expr);
+
+	void write(std::string _data);
+
+	std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
+	std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
+
+	/// Communicates with the solver via the callback. Throws SMTSolverError on error.
+	std::string querySolver(std::string const& _input);
+
+	ReadCallback::Callback m_queryCallback;
+	std::vector<std::string> m_accumulatedOutput;
+};
+
+}
+}
+}
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
new file mode 100644
index 00000000..32d92a2a
--- /dev/null
+++ b/libsolidity/formal/SolverInterface.h
@@ -0,0 +1,178 @@
+/*
+	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/interface/Exceptions.h>
+#include <libsolidity/interface/ReadFile.h>
+
+#include <libdevcore/Common.h>
+#include <libdevcore/Exceptions.h>
+
+#include <boost/noncopyable.hpp>
+
+#include <map>
+#include <string>
+#include <vector>
+#include <cstdio>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+enum class CheckResult
+{
+	SATISFIABLE, UNSATISFIABLE, UNKNOWN, ERROR
+};
+
+enum class Sort
+{
+	Int, Bool
+};
+
+/// C++ representation of an SMTLIB2 expression.
+class Expression
+{
+	friend class SolverInterface;
+public:
+	Expression(size_t _number): name(std::to_string(_number)) {}
+	Expression(u256 const& _number): name(_number.str()) {}
+	Expression(bigint const& _number): name(_number.str()) {}
+
+	Expression(Expression const& _other) = default;
+	Expression(Expression&& _other) = default;
+	Expression& operator=(Expression const& _other) = default;
+	Expression& operator=(Expression&& _other) = default;
+
+	static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
+	{
+		return Expression("ite", std::vector<Expression>{
+			std::move(_condition), std::move(_trueValue), std::move(_falseValue)
+		});
+	}
+
+	friend Expression operator!(Expression _a)
+	{
+		return Expression("not", std::move(_a));
+	}
+	friend Expression operator&&(Expression _a, Expression _b)
+	{
+		return Expression("and", std::move(_a), std::move(_b));
+	}
+	friend Expression operator||(Expression _a, Expression _b)
+	{
+		return Expression("or", std::move(_a), std::move(_b));
+	}
+	friend Expression operator==(Expression _a, Expression _b)
+	{
+		return Expression("=", std::move(_a), std::move(_b));
+	}
+	friend Expression operator!=(Expression _a, Expression _b)
+	{
+		return !(std::move(_a) == std::move(_b));
+	}
+	friend Expression operator<(Expression _a, Expression _b)
+	{
+		return Expression("<", std::move(_a), std::move(_b));
+	}
+	friend Expression operator<=(Expression _a, Expression _b)
+	{
+		return Expression("<=", std::move(_a), std::move(_b));
+	}
+	friend Expression operator>(Expression _a, Expression _b)
+	{
+		return Expression(">", std::move(_a), std::move(_b));
+	}
+	friend Expression operator>=(Expression _a, Expression _b)
+	{
+		return Expression(">=", std::move(_a), std::move(_b));
+	}
+	friend Expression operator+(Expression _a, Expression _b)
+	{
+		return Expression("+", std::move(_a), std::move(_b));
+	}
+	friend Expression operator-(Expression _a, Expression _b)
+	{
+		return Expression("-", std::move(_a), std::move(_b));
+	}
+	friend Expression operator*(Expression _a, Expression _b)
+	{
+		return Expression("*", std::move(_a), std::move(_b));
+	}
+	Expression operator()(Expression _a) const
+	{
+		solAssert(arguments.empty(), "Attempted function application to non-function.");
+		return Expression(name, _a);
+	}
+
+	std::string const name;
+	std::vector<Expression> const arguments;
+
+private:
+	/// Manual constructor, should only be used by SolverInterface and this class itself.
+	Expression(std::string _name, std::vector<Expression> _arguments):
+		name(std::move(_name)), arguments(std::move(_arguments)) {}
+
+	explicit Expression(std::string _name):
+		Expression(std::move(_name), std::vector<Expression>{}) {}
+	Expression(std::string _name, Expression _arg):
+		Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}) {}
+	Expression(std::string _name, Expression _arg1, Expression _arg2):
+		Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}) {}
+};
+
+DEV_SIMPLE_EXCEPTION(SolverError);
+
+class SolverInterface
+{
+public:
+	virtual void reset() = 0;
+
+	virtual void push() = 0;
+	virtual void pop() = 0;
+
+	virtual Expression newFunction(std::string _name, Sort /*_domain*/, Sort /*_codomain*/)
+	{
+		// Subclasses should do something here
+		return Expression(std::move(_name), {});
+	}
+	virtual Expression newInteger(std::string _name)
+	{
+		// Subclasses should do something here
+		return Expression(std::move(_name), {});
+	}
+	virtual Expression newBool(std::string _name)
+	{
+		// Subclasses should do something here
+		return Expression(std::move(_name), {});
+	}
+
+	virtual void addAssertion(Expression const& _expr) = 0;
+
+	/// Checks for satisfiability, evaluates the expressions if a model
+	/// is available. Throws SMTSolverError on error.
+	virtual std::pair<CheckResult, std::vector<std::string>>
+	check(std::vector<Expression> const& _expressionsToEvaluate) = 0;
+};
+
+
+}
+}
+}
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
new file mode 100644
index 00000000..522928f0
--- /dev/null
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -0,0 +1,189 @@
+/*
+	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/Z3Interface.h>
+
+#include <libsolidity/interface/Exceptions.h>
+
+#include <libdevcore/CommonIO.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity::smt;
+
+Z3Interface::Z3Interface():
+	m_solver(m_context)
+{
+}
+
+void Z3Interface::reset()
+{
+	m_constants.clear();
+	m_functions.clear();
+	m_solver.reset();
+}
+
+void Z3Interface::push()
+{
+	m_solver.push();
+}
+
+void Z3Interface::pop()
+{
+	m_solver.pop();
+}
+
+Expression Z3Interface::newFunction(string _name, Sort _domain, Sort _codomain)
+{
+	m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
+	return SolverInterface::newFunction(move(_name), _domain, _codomain);
+}
+
+Expression Z3Interface::newInteger(string _name)
+{
+	m_constants.insert({_name, m_context.int_const(_name.c_str())});
+	return SolverInterface::newInteger(move(_name));
+}
+
+Expression Z3Interface::newBool(string _name)
+{
+	m_constants.insert({_name, m_context.bool_const(_name.c_str())});
+	return SolverInterface::newBool(std::move(_name));
+}
+
+void Z3Interface::addAssertion(Expression const& _expr)
+{
+	m_solver.add(toZ3Expr(_expr));
+}
+
+pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate)
+{
+//	cout << "---------------------------------" << endl;
+//	cout << m_solver << endl;
+	CheckResult result;
+	switch (m_solver.check())
+	{
+	case z3::check_result::sat:
+		result = CheckResult::SATISFIABLE;
+		cout << "sat" << endl;
+		break;
+	case z3::check_result::unsat:
+		result = CheckResult::UNSATISFIABLE;
+		cout << "unsat" << endl;
+		break;
+	case z3::check_result::unknown:
+		result = CheckResult::UNKNOWN;
+		cout << "unknown" << endl;
+		break;
+	default:
+		solAssert(false, "");
+	}
+//	cout << "---------------------------------" << endl;
+
+
+	vector<string> values;
+	if (result != CheckResult::UNSATISFIABLE)
+	{
+		z3::model m = m_solver.get_model();
+		for (Expression const& e: _expressionsToEvaluate)
+			values.push_back(toString(m.eval(toZ3Expr(e))));
+	}
+	return make_pair(result, values);
+}
+
+z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
+{
+	if (_expr.arguments.empty() && m_constants.count(_expr.name))
+		return m_constants.at(_expr.name);
+	z3::expr_vector arguments(m_context);
+	for (auto const& arg: _expr.arguments)
+		arguments.push_back(toZ3Expr(arg));
+
+	static map<string, unsigned> arity{
+		{"ite", 3},
+		{"not", 1},
+		{"and", 2},
+		{"or", 2},
+		{"=", 2},
+		{"<", 2},
+		{"<=", 2},
+		{">", 2},
+		{">=", 2},
+		{"+", 2},
+		{"-", 2},
+		{"*", 2},
+		{">=", 2}
+	};
+	string const& n = _expr.name;
+	if (m_functions.count(n))
+		return m_functions.at(n)(arguments);
+	else if (m_constants.count(n))
+	{
+		solAssert(arguments.empty(), "");
+		return m_constants.at(n);
+	}
+	else if (arguments.empty())
+	{
+		// We assume it is an integer...
+		return m_context.int_val(n.c_str());
+	}
+
+	assert(arity.count(n) && arity.at(n) == arguments.size());
+	if (n == "ite")
+		return z3::ite(arguments[0], arguments[1], arguments[2]);
+	else if (n == "not")
+		return !arguments[0];
+	else if (n == "and")
+		return arguments[0] && arguments[1];
+	else if (n == "or")
+		return arguments[0] || arguments[1];
+	else if (n == "=")
+		return arguments[0] == arguments[1];
+	else if (n == "<")
+		return arguments[0] < arguments[1];
+	else if (n == "<=")
+		return arguments[0] <= arguments[1];
+	else if (n == ">")
+		return arguments[0] > arguments[1];
+	else if (n == ">=")
+		return arguments[0] >= arguments[1];
+	else if (n == "+")
+		return arguments[0] + arguments[1];
+	else if (n == "-")
+		return arguments[0] - arguments[1];
+	else if (n == "*")
+		return arguments[0] * arguments[1];
+	// Cannot reach here.
+	solAssert(false, "");
+	return arguments[0];
+}
+
+z3::sort Z3Interface::z3Sort(Sort _sort)
+{
+	switch (_sort)
+	{
+	case Sort::Bool:
+		return m_context.bool_sort();
+	case Sort::Int:
+		return m_context.int_sort();
+	default:
+		break;
+	}
+	solAssert(false, "");
+	// Cannot be reached.
+	return m_context.int_sort();
+}
diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h
new file mode 100644
index 00000000..44d4bb2f
--- /dev/null
+++ b/libsolidity/formal/Z3Interface.h
@@ -0,0 +1,65 @@
+/*
+	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/formal/SolverInterface.h>
+
+#include <boost/noncopyable.hpp>
+
+#include <z3++.h>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+class Z3Interface: public SolverInterface, public boost::noncopyable
+{
+public:
+	Z3Interface();
+
+	void reset() override;
+
+	void push() override;
+	void pop() override;
+
+	Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override;
+	Expression newInteger(std::string _name) override;
+	Expression newBool(std::string _name) override;
+
+	void addAssertion(Expression const& _expr) override;
+	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
+
+private:
+	z3::expr toZ3Expr(Expression const& _expr);
+	z3::sort z3Sort(smt::Sort _sort);
+
+	std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
+	std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
+
+	z3::context m_context;
+	z3::solver m_solver;
+	std::map<std::string, z3::expr> m_constants;
+	std::map<std::string, z3::func_decl> m_functions;
+};
+
+}
+}
+}
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index 412d2fd3..363f45dd 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, m_smtQuery);
+		for (Source const* source: m_sourceOrder)
+			smtChecker.analyze(*source->ast);
+	}
+
+	if (noErrors)
+	{
 		m_stackState = AnalysisSuccessful;
 		return true;
 	}
@@ -527,17 +535,17 @@ StringMap CompilerStack::loadMissingSources(SourceUnit const& _ast, std::string
 			if (m_sources.count(importPath) || newSources.count(importPath))
 				continue;
 
-			ReadFile::Result result{false, string("File not supplied initially.")};
+			ReadCallback::Result result{false, string("File not supplied initially.")};
 			if (m_readFile)
 				result = m_readFile(importPath);
 
 			if (result.success)
-				newSources[importPath] = result.contentsOrErrorMessage;
+				newSources[importPath] = result.responseOrErrorMessage;
 			else
 			{
 				m_errorReporter.parserError(
 					import->location(),
-					string("Source \"" + importPath + "\" not found: " + result.contentsOrErrorMessage)
+					string("Source \"" + importPath + "\" not found: " + result.responseOrErrorMessage)
 				);
 				continue;
 			}
diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h
index bb0f4126..361b8a45 100644
--- a/libsolidity/interface/CompilerStack.h
+++ b/libsolidity/interface/CompilerStack.h
@@ -82,7 +82,7 @@ public:
 	/// Creates a new compiler stack.
 	/// @param _readFile callback to used to read files for import statements. Must return
 	/// and must not emit exceptions.
-	explicit CompilerStack(ReadFile::Callback const& _readFile = ReadFile::Callback()):
+	explicit CompilerStack(ReadCallback::Callback const& _readFile = ReadCallback::Callback()):
 		m_readFile(_readFile),
 		m_errorList(),
 		m_errorReporter(m_errorList) {}
@@ -287,7 +287,8 @@ private:
 		std::string target;
 	};
 
-	ReadFile::Callback m_readFile;
+	ReadCallback::Callback m_readFile;
+	ReadCallback::Callback m_smtQuery;
 	bool m_optimize = false;
 	unsigned m_optimizeRuns = 200;
 	std::map<std::string, h160> m_libraries;
diff --git a/libsolidity/interface/ReadFile.h b/libsolidity/interface/ReadFile.h
index 2e8a6bd8..7068629d 100644
--- a/libsolidity/interface/ReadFile.h
+++ b/libsolidity/interface/ReadFile.h
@@ -27,17 +27,17 @@ namespace dev
 namespace solidity
 {
 
-class ReadFile: boost::noncopyable
+class ReadCallback: boost::noncopyable
 {
 public:
-	/// File reading result.
+	/// File reading or generic query result.
 	struct Result
 	{
 		bool success;
-		std::string contentsOrErrorMessage;
+		std::string responseOrErrorMessage;
 	};
 
-	/// File reading callback.
+	/// File reading or generic query callback.
 	using Callback = std::function<Result(std::string const&)>;
 };
 
diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
index 7a6f9989..be823743 100644
--- a/libsolidity/interface/StandardCompiler.cpp
+++ b/libsolidity/interface/StandardCompiler.cpp
@@ -203,10 +203,10 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
 
 			for (auto const& url: sources[sourceName]["urls"])
 			{
-				ReadFile::Result result = m_readFile(url.asString());
+				ReadCallback::Result result = m_readFile(url.asString());
 				if (result.success)
 				{
-					if (!hash.empty() && !hashMatchesContent(hash, result.contentsOrErrorMessage))
+					if (!hash.empty() && !hashMatchesContent(hash, result.responseOrErrorMessage))
 						errors.append(formatError(
 							false,
 							"IOError",
@@ -215,13 +215,13 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
 						));
 					else
 					{
-						m_compilerStack.addSource(sourceName, result.contentsOrErrorMessage);
+						m_compilerStack.addSource(sourceName, result.responseOrErrorMessage);
 						found = true;
 						break;
 					}
 				}
 				else
-					failures.push_back("Cannot import url (\"" + url.asString() + "\"): " + result.contentsOrErrorMessage);
+					failures.push_back("Cannot import url (\"" + url.asString() + "\"): " + result.responseOrErrorMessage);
 			}
 
 			for (auto const& failure: failures)
diff --git a/libsolidity/interface/StandardCompiler.h b/libsolidity/interface/StandardCompiler.h
index d9787a40..11a0b4c2 100644
--- a/libsolidity/interface/StandardCompiler.h
+++ b/libsolidity/interface/StandardCompiler.h
@@ -40,7 +40,7 @@ public:
 	/// Creates a new StandardCompiler.
 	/// @param _readFile callback to used to read files for import statements. Must return
 	/// and must not emit exceptions.
-	explicit StandardCompiler(ReadFile::Callback const& _readFile = ReadFile::Callback())
+	explicit StandardCompiler(ReadCallback::Callback const& _readFile = ReadCallback::Callback())
 		: m_compilerStack(_readFile), m_readFile(_readFile)
 	{
 	}
@@ -56,7 +56,7 @@ private:
 	Json::Value compileInternal(Json::Value const& _input);
 
 	CompilerStack m_compilerStack;
-	ReadFile::Callback m_readFile;
+	ReadCallback::Callback m_readFile;
 };
 
 }
diff --git a/scripts/install_deps.sh b/scripts/install_deps.sh
index 24cf49d5..3a1abe10 100755
--- a/scripts/install_deps.sh
+++ b/scripts/install_deps.sh
@@ -115,7 +115,7 @@ case $(uname -s) in
         echo "Installing solidity dependencies on FreeBSD."
         echo "ERROR - 'install_deps.sh' doesn't have FreeBSD support yet."
         echo "Please let us know if you see this error message, and we can work out what is missing."
-        echo "Drop us a message at https://gitter.im/ethereum/solidity."
+        echo "Drop us a message at https://gitter.im/ethereum/solidity-dev."
         exit 1
         ;;
 
@@ -167,6 +167,7 @@ case $(uname -s) in
 
             Debian)
                 #Debian
+                install_z3=""
                 case $(lsb_release -cs) in
                     wheezy)
                         #wheezy
@@ -174,7 +175,7 @@ case $(uname -s) in
                         echo "ERROR - 'install_deps.sh' doesn't have Debian Wheezy support yet."
                         echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions."
                         echo "If you would like to get 'install_deps.sh' working for Debian Wheezy, that would be fantastic."
-                        echo "Drop us a message at https://gitter.im/ethereum/solidity."
+                        echo "Drop us a message at https://gitter.im/ethereum/solidity-dev."
                         echo "See also https://github.com/ethereum/webthree-umbrella/issues/495 where we are working through Alpine support."
                         exit 1
                         ;;
@@ -185,20 +186,19 @@ case $(uname -s) in
                     stretch)
                         #stretch
                         echo "Installing solidity dependencies on Debian Stretch (9.x)."
-                        echo "ERROR - 'install_deps.sh' doesn't have Debian Stretch support yet."
-                        echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions."
-                        echo "If you would like to get 'install_deps.sh' working for Debian Stretch, that would be fantastic."
-                        echo "Drop us a message at https://gitter.im/ethereum/solidity."
-                        exit 1
+                        install_z3="libz3-dev"
+                        ;;
+                    buster)
+                        #buster
+                        echo "Installing solidity dependencies on Debian Buster (10.x)."
+                        install_z3="libz3-dev"
                         ;;
                     *)
                         #other Debian
                         echo "Installing solidity dependencies on unknown Debian version."
-                        echo "ERROR - Debian Jessie is the only Debian version which solidity has been tested on."
-                        echo "If you are using a different release and would like to get 'install_deps.sh'"
-                        echo "working for that release that would be fantastic."
-                        echo "Drop us a message at https://gitter.im/ethereum/solidity."
-                        exit 1
+                        echo "ERROR - This might not work, but we are trying anyway."
+                        echo "Drop us a message at https://gitter.im/ethereum/solidity-dev"
+                        install_z3="libz3-dev"
                         ;;
                 esac
 
@@ -211,7 +211,9 @@ case $(uname -s) in
                     gcc \
                     git \
                     libboost-all-dev \
-                    unzip
+                    unzip \
+                    "$install_z3"
+
 
                 ;;
 
@@ -267,6 +269,7 @@ case $(uname -s) in
 
             Ubuntu)
                 #Ubuntu
+                install_z3=""
                 case $(lsb_release -cs) in
                     trusty)
                         #trusty
@@ -287,22 +290,25 @@ case $(uname -s) in
                     xenial)
                         #xenial
                         echo "Installing solidity dependencies on Ubuntu Xenial Xerus (16.04)."
+                        install_z3="libz3-dev"
                         ;;
                     yakkety)
                         #yakkety
                         echo "Installing solidity dependencies on Ubuntu Yakkety Yak (16.10)."
-                        echo ""
-                        echo "NOTE - You are in unknown territory with this preview OS."
-                        echo "We will need to update the Ethereum PPAs, work through build and runtime breaks, etc."
-                        echo "See https://github.com/ethereum/webthree-umbrella/issues/624."
-                        echo "If you would like to partner with us to work through these, that"
-                        echo "would be fantastic.  Please just comment on that issue.  Thanks!"
+                        install_z3="libz3-dev"
+                        ;;
+                    zesty)
+                        #zesty
+                        echo "Installing solidity dependencies on Ubuntu Zesty (17.04)."
+                        install_z3="libz3-dev"
                         ;;
                     *)
                         #other Ubuntu
                         echo "ERROR - Unknown or unsupported Ubuntu version (" $(lsb_release -cs) ")"
-                        echo "We only support Trusty, Utopic, Vivid, Wily and Xenial, with work-in-progress on Yakkety."
-                        exit 1
+                        echo "ERROR - This might not work, but we are trying anyway."
+                        echo "Please drop us a message at https://gitter.im/ethereum/solidity-dev."
+                        echo "We only support Trusty, Utopic, Vivid, Wily, Xenial and Yakkety."
+                        install_z3="libz3-dev"
                         ;;
                 esac
 
@@ -311,7 +317,8 @@ case $(uname -s) in
                     build-essential \
                     cmake \
                     git \
-                    libboost-all-dev
+                    libboost-all-dev \
+                    "$install_z3"
                 if [ "$CI" = true ]; then
                     # Install 'eth', for use in the Solidity Tests-over-IPC.
                     # We will not use this 'eth', but its dependencies
@@ -375,7 +382,7 @@ case $(uname -s) in
                 echo "ERROR - Unsupported or unidentified Linux distro."
                 echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions."
                 echo "If you would like to get your distro working, that would be fantastic."
-                echo "Drop us a message at https://gitter.im/ethereum/solidity."
+                echo "Drop us a message at https://gitter.im/ethereum/solidity-dev."
                 exit 1
                 ;;
         esac
@@ -392,6 +399,6 @@ case $(uname -s) in
         echo "ERROR - Unsupported or unidentified operating system."
         echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions."
         echo "If you would like to get your operating system working, that would be fantastic."
-        echo "Drop us a message at https://gitter.im/ethereum/solidity."
+        echo "Drop us a message at https://gitter.im/ethereum/solidity-dev."
         ;;
 esac
diff --git a/solc/CommandLineInterface.cpp b/solc/CommandLineInterface.cpp
index bfc53aef..315f951e 100644
--- a/solc/CommandLineInterface.cpp
+++ b/solc/CommandLineInterface.cpp
@@ -663,7 +663,7 @@ Allowed options)",
 
 bool CommandLineInterface::processInput()
 {
-	ReadFile::Callback fileReader = [this](string const& _path)
+	ReadCallback::Callback fileReader = [this](string const& _path)
 	{
 		try
 		{
@@ -683,25 +683,25 @@ bool CommandLineInterface::processInput()
 				}
 			}
 			if (!isAllowed)
-				return ReadFile::Result{false, "File outside of allowed directories."};
+				return ReadCallback::Result{false, "File outside of allowed directories."};
 			else if (!boost::filesystem::exists(path))
-				return ReadFile::Result{false, "File not found."};
+				return ReadCallback::Result{false, "File not found."};
 			else if (!boost::filesystem::is_regular_file(canonicalPath))
-				return ReadFile::Result{false, "Not a valid file."};
+				return ReadCallback::Result{false, "Not a valid file."};
 			else
 			{
 				auto contents = dev::contentsString(canonicalPath.string());
 				m_sourceCodes[path.string()] = contents;
-				return ReadFile::Result{true, contents};
+				return ReadCallback::Result{true, contents};
 			}
 		}
 		catch (Exception const& _exception)
 		{
-			return ReadFile::Result{false, "Exception in read callback: " + boost::diagnostic_information(_exception)};
+			return ReadCallback::Result{false, "Exception in read callback: " + boost::diagnostic_information(_exception)};
 		}
 		catch (...)
 		{
-			return ReadFile::Result{false, "Unknown exception in read callback."};
+			return ReadCallback::Result{false, "Unknown exception in read callback."};
 		}
 	};
 
diff --git a/solc/jsonCompiler.cpp b/solc/jsonCompiler.cpp
index ab928ac0..684d49e4 100644
--- a/solc/jsonCompiler.cpp
+++ b/solc/jsonCompiler.cpp
@@ -41,9 +41,9 @@ typedef void (*CStyleReadFileCallback)(char const* _path, char** o_contents, cha
 namespace
 {
 
-ReadFile::Callback wrapReadCallback(CStyleReadFileCallback _readCallback = nullptr)
+ReadCallback::Callback wrapReadCallback(CStyleReadFileCallback _readCallback = nullptr)
 {
-	ReadFile::Callback readCallback;
+	ReadCallback::Callback readCallback;
 	if (_readCallback)
 	{
 		readCallback = [=](string const& _path)
@@ -51,23 +51,23 @@ ReadFile::Callback wrapReadCallback(CStyleReadFileCallback _readCallback = nullp
 			char* contents_c = nullptr;
 			char* error_c = nullptr;
 			_readCallback(_path.c_str(), &contents_c, &error_c);
-			ReadFile::Result result;
+			ReadCallback::Result result;
 			result.success = true;
 			if (!contents_c && !error_c)
 			{
 				result.success = false;
-				result.contentsOrErrorMessage = "File not found.";
+				result.responseOrErrorMessage = "File not found.";
 			}
 			if (contents_c)
 			{
 				result.success = true;
-				result.contentsOrErrorMessage = string(contents_c);
+				result.responseOrErrorMessage = string(contents_c);
 				free(contents_c);
 			}
 			if (error_c)
 			{
 				result.success = false;
-				result.contentsOrErrorMessage = string(error_c);
+				result.responseOrErrorMessage = string(error_c);
 				free(error_c);
 			}
 			return result;