Cleanup.

8 files changed, 685 insertions, 715 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 0e559fae..b9e0e8f3 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -17,7 +17,6 @@
 
 #include <libsolidity/formal/SMTChecker.h>
 
-#include <libsolidity/formal/SMTCheckerImpl.h>
 
 #include <libsolidity/interface/ErrorReporter.h>
 
@@ -25,12 +24,452 @@ using namespace std;
 using namespace dev;
 using namespace dev::solidity;
 
-SMTChecker::SMTChecker(ErrorReporter& _errorReporter):
-	m_impl(make_shared<SMTCheckerImpl>(_errorReporter))
+SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadFile::Callback const& _readFileCallback):
+	m_interface(_readFileCallback),
+	m_errorReporter(_errorReporter)
 {
 }
 
 void SMTChecker::analyze(SourceUnit const& _source)
 {
-	m_impl->analyze(_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_interface.reset();
+		m_currentSequenceCounter.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.
+	m_interface.pop();
+	m_currentFunction = nullptr;
+}
+
+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]) && _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 " + intType.minValue().str() + ")",
+			"value",
+			&value
+		);
+		checkCondition(
+			value > maxValue(intType),
+			_op.location(),
+			"Overflow (resulting value larger than " + intType.maxValue().str() + ")",
+			"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;
+	if (m_currentFunction)
+	{
+		if (_additionalValue)
+			expressionsToEvaluate.emplace_back(*_additionalValue);
+		for (auto const& param: m_currentFunction->parameters())
+			if (knownVariable(*param))
+				expressionsToEvaluate.emplace_back(currentValue(*param));
+		for (auto const& var: m_currentFunction->localVariables())
+			if (knownVariable(*var))
+				expressionsToEvaluate.emplace_back(currentValue(*var));
+	}
+	smt::CheckResult result;
+	vector<string> values;
+	tie(result, values) = m_interface.check(expressionsToEvaluate);
+	switch (result)
+	{
+	case smt::CheckResult::SAT:
+	{
+		std::ostringstream message;
+		message << _description << " happens here";
+		size_t i = 0;
+		if (m_currentFunction)
+		{
+			message << " for:\n";
+			if (_additionalValue)
+				message << "  " << _additionalValueName << " = " << values.at(i++) << "\n";
+			for (auto const& param: m_currentFunction->parameters())
+				if (knownVariable(*param))
+					message << "  " << param->name() << " = " << values.at(i++) << "\n";
+			for (auto const& var: m_currentFunction->localVariables())
+				if (knownVariable(*var))
+					message << "  " << var->name() << " = " << values.at(i++) << "\n";
+		}
+		else
+			message << ".";
+		m_errorReporter.warning(_location, message.str());
+		break;
+	}
+	case smt::CheckResult::UNSAT:
+		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 (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_interface.newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
+		if (_setToZero)
+			m_interface.addAssertion(currentValue(_varDecl) == 0);
+		else
+		{
+			m_interface.addAssertion(currentValue(_varDecl) >= minValue(*intType));
+			m_interface.addAssertion(currentValue(_varDecl) <= maxValue(*intType));
+		}
+	}
+	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 var(_decl)(m_currentSequenceCounter.at(&_decl));
+}
+
+smt::Expression SMTChecker::newValue(const Declaration& _decl)
+{
+	solAssert(m_currentSequenceCounter.count(&_decl), "");
+	m_currentSequenceCounter[&_decl]++;
+	return currentValue(_decl);
+}
+
+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_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_interface.newInteger(uniqueSymbol(_e)));
+			break;
+		}
+		case Type::Category::Integer:
+			m_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e)));
+			break;
+		case Type::Category::Bool:
+			m_z3Expressions.emplace(&_e, m_interface.newBool(uniqueSymbol(_e)));
+			break;
+		default:
+			solAssert(false, "Type not implemented.");
+		}
+	}
+	return m_z3Expressions.at(&_e);
+}
+
+smt::Expression SMTChecker::var(Declaration const& _decl)
+{
+	solAssert(m_z3Variables.count(&_decl), "");
+	return m_z3Variables.at(&_decl);
 }
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 7e7ee3d9..8c6a2327 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -17,9 +17,12 @@
 
 #pragma once
 
+#include <libsolidity/ast/ASTVisitor.h>
+#include <libsolidity/formal/SMTLib2Interface.h>
+#include <libsolidity/interface/ReadFile.h>
+
 #include <map>
 #include <string>
-#include <memory>
 
 namespace dev
 {
@@ -27,18 +30,68 @@ namespace solidity
 {
 
 class ErrorReporter;
-class SourceUnit;
-class SMTCheckerImpl;
 
-class SMTChecker
+class SMTChecker: private ASTConstVisitor
 {
 public:
-	SMTChecker(ErrorReporter& _errorReporter);
+	SMTChecker(ErrorReporter& _errorReporter, ReadFile::Callback const& _readCallback);
 
 	void analyze(SourceUnit const& _sources);
 
 private:
-	std::shared_ptr<SMTCheckerImpl> m_impl;
+	// 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(
+		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);
+
+	std::string uniqueSymbol(Declaration const& _decl);
+	std::string uniqueSymbol(Expression const& _expr);
+	bool knownVariable(Declaration const& _decl);
+	smt::Expression currentValue(Declaration const& _decl);
+	smt::Expression newValue(Declaration const& _decl);
+
+	smt::Expression minValue(IntegerType const& _t);
+	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);
+
+	smt::SMTLib2Interface m_interface;
+	std::map<Declaration const*, int> m_currentSequenceCounter;
+	std::map<Expression const*, smt::Expression> m_z3Expressions;
+	std::map<Declaration const*, smt::Expression> m_z3Variables;
+	ErrorReporter& m_errorReporter;
+
+	FunctionDefinition const* m_currentFunction = nullptr;
 };
 
 }
diff --git a/libsolidity/formal/SMTCheckerImpl.cpp b/libsolidity/formal/SMTCheckerImpl.cpp
deleted file mode 100644
index b86a0279..00000000
--- a/libsolidity/formal/SMTCheckerImpl.cpp
+++ /dev/null
@@ -1,469 +0,0 @@
-/*
-	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_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_interface.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_interface.push();
-	return true;
-}
-
-void SMTCheckerImpl::endVisit(FunctionDefinition const&)
-{
-	// TOOD we could check for "reachability", i.e. satisfiability here.
-	m_interface.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_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 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_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 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_interface.addAssertion(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_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 SMTCheckerImpl::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 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_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 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, "");
-		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 " + intType.minValue().str() + ")",
-			"value",
-			&value
-		);
-		checkCondition(
-			value > maxValue(intType),
-			_op.location(),
-			"Overflow (resulting value larger than " + intType.maxValue().str() + ")",
-			"value",
-			&value
-		);
-
-		m_interface.addAssertion(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)
-	{
-		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 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_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 SMTCheckerImpl::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;
-	if (m_currentFunction)
-	{
-		if (_additionalValue)
-			expressionsToEvaluate.emplace_back(*_additionalValue);
-		for (auto const& param: m_currentFunction->parameters())
-			if (knownVariable(*param))
-				expressionsToEvaluate.emplace_back(currentValue(*param));
-		for (auto const& var: m_currentFunction->localVariables())
-			if (knownVariable(*var))
-				expressionsToEvaluate.emplace_back(currentValue(*var));
-	}
-	smt::CheckResult result;
-	vector<string> values;
-	tie(result, values) = m_interface.check(expressionsToEvaluate);
-	switch (result)
-	{
-	case smt::CheckResult::SAT:
-	{
-		std::ostringstream message;
-		message << _description << " happens here";
-		size_t i = 0;
-		if (m_currentFunction)
-		{
-			message << " for:\n";
-			if (_additionalValue)
-				message << "  " << _additionalValueName << " = " << values.at(i++) << "\n";
-			for (auto const& param: m_currentFunction->parameters())
-				if (knownVariable(*param))
-					message << "  " << param->name() << " = " << values.at(i++) << "\n";
-			for (auto const& var: m_currentFunction->localVariables())
-				if (knownVariable(*var))
-					message << "  " << var->name() << " = " << values.at(i++) << "\n";
-		}
-		else
-			message << ".";
-		m_errorReporter.warning(_location, message.str());
-		break;
-	}
-	case smt::CheckResult::UNSAT:
-		break;
-	case smt::CheckResult::UNKNOWN:
-		m_errorReporter.warning(_location, _description + " might happen here.");
-		break;
-	}
-	m_interface.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_interface.newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
-		if (_setToZero)
-			m_interface.addAssertion(currentValue(_varDecl) == 0);
-		else
-		{
-			m_interface.addAssertion(currentValue(_varDecl) >= minValue(*intType));
-			m_interface.addAssertion(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);
-}
-
-smt::Expression SMTCheckerImpl::currentValue(Declaration const& _decl)
-{
-	solAssert(m_currentSequenceCounter.count(&_decl), "");
-	return var(_decl)(m_currentSequenceCounter.at(&_decl));
-}
-
-smt::Expression SMTCheckerImpl::newValue(const Declaration& _decl)
-{
-	solAssert(m_currentSequenceCounter.count(&_decl), "");
-	m_currentSequenceCounter[&_decl]++;
-	return currentValue(_decl);
-}
-
-smt::Expression SMTCheckerImpl::minValue(IntegerType const& _t)
-{
-	return smt::Expression(_t.minValue());
-}
-
-smt::Expression SMTCheckerImpl::maxValue(IntegerType const& _t)
-{
-	return smt::Expression(_t.maxValue());
-}
-
-smt::Expression 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_interface.newInteger(uniqueSymbol(_e)));
-			break;
-		}
-		case Type::Category::Integer:
-			m_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e)));
-			break;
-		case Type::Category::Bool:
-			m_z3Expressions.emplace(&_e, m_interface.newBool(uniqueSymbol(_e)));
-			break;
-		default:
-			solAssert(false, "Type not implemented.");
-		}
-	}
-	return m_z3Expressions.at(&_e);
-}
-
-smt::Expression 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
deleted file mode 100644
index e5179440..00000000
--- a/libsolidity/formal/SMTCheckerImpl.h
+++ /dev/null
@@ -1,97 +0,0 @@
-/*
-	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/SMTLib2Interface.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(
-		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);
-
-	std::string uniqueSymbol(Declaration const& _decl);
-	std::string uniqueSymbol(Expression const& _expr);
-	bool knownVariable(Declaration const& _decl);
-	smt::Expression currentValue(Declaration const& _decl);
-	smt::Expression newValue(Declaration const& _decl);
-
-	smt::Expression minValue(IntegerType const& _t);
-	smt::Expression maxValue(IntegerType const& _t);
-
-	/// Returns the z3 expression corresponding to the AST node. Creates a new expression
-	/// if it does not exist yet.
-	smt::Expression expr(Expression const& _e);
-	/// Returns the z3 function declaration corresponding to the given variable.
-	/// The function takes one argument which is the "sequence number".
-	smt::Expression var(Declaration const& _decl);
-
-	smt::SMTLib2Interface m_interface;
-	std::map<Declaration const*, int> m_currentSequenceCounter;
-	std::map<Expression const*, smt::Expression> m_z3Expressions;
-	std::map<Declaration const*, smt::Expression> m_z3Variables;
-	ErrorReporter& m_errorReporter;
-
-	FunctionDefinition const* m_currentFunction = nullptr;
-};
-
-}
-}
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 8d40c354..63ab1679 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -21,6 +21,7 @@
 
 #include <boost/algorithm/string/predicate.hpp>
 #include <boost/algorithm/string/join.hpp>
+#include <boost/filesystem/operations.hpp>
 
 #include <cstdio>
 #include <fstream>
@@ -30,99 +31,31 @@
 #include <string>
 #include <array>
 
-#include <sys/types.h>
-#include <unistd.h>
-#include <stdio.h>
-#include <stdlib.h>
-
 using namespace std;
 using namespace dev;
 using namespace dev::solidity::smt;
 
-
-//namespace
-//{
-
-//void createSubprocess(FILE*& _readPipe, FILE*& _writePipe)
-//{
-//	int pipe_in[2];   /* This is the pipe with wich we write to the child process. */
-//	int pipe_out[2];  /* This is the pipe with wich we read from the child process. */
-
-//	solAssert(!pipe(pipe_in) && !pipe(pipe_out), "");
-
-//	/* Attempt to fork and check for errors */
-//	pid_t pid = fork();
-//	solAssert(pid != -1, "");
-
-//	if (pid)
-//	{
-//		/* The parent has the non-zero PID. */
-//		_readPipe = fdopen(pipe_out[0], "r");
-//		_writePipe = fdopen(pipe_in[1], "w");
-//		close(pipe_out[1]);
-//		close(pipe_in[0]);
-//	}
-//	else
-//	{
-//		/* The child has the zero pid returned by fork*/
-//		cout << "child" << endl;
-//		solAssert(dup2(pipe_out[1], 1) != -1, "");
-//		solAssert(dup2(pipe_in[0], 0) != -1, "");
-//		solAssert(close(pipe_out[0]) == 0, "");
-//		solAssert(close(pipe_out[1]) == 0, "");
-//		solAssert(close(pipe_in[0]) == 0, "");
-//		solAssert(close(pipe_in[1]) == 0, "");
-//		execl("/usr/bin/z3", "z3", "-smt2", "-in", NULL);
-//		exit(1); /* Only reached if execl() failed */
-//	}
-//}
-
-//}
-
-SMTLib2Interface::SMTLib2Interface()
+SMTLib2Interface::SMTLib2Interface(ReadFile::Callback const& _readFileCallback):
+	m_communicator(_readFileCallback)
 {
-	// TODO using pipes did not really work, so trying it the hard way for now.
-//	createSubprocess(m_solverWrite, m_solverRead);
-//	solAssert(m_solverWrite, "Unable to start Z3");
-//	solAssert(m_solverRead, "Unable to start Z3");
-//	write("(set-option :produce-models true)\n(set-logic QF_LIA)\n");
 	reset();
 }
 
-SMTLib2Interface::~SMTLib2Interface()
-{
-//	if (m_solverWrite)
-//	{
-//		write("(exit)\n");
-//		fflush(m_solverWrite);
-//		fclose(m_solverWrite);
-//		m_solverWrite = nullptr;
-//	}
-//	if (m_solverRead)
-//	{
-//		fclose(m_solverRead);
-//		m_solverRead = nullptr;
-//	}
-}
-
 void SMTLib2Interface::reset()
 {
-//	write("(reset)\n");
-//	write("(set-option :produce-models true)\n");
 	m_accumulatedOutput.clear();
 	m_accumulatedOutput.emplace_back();
-	write("(set-option :produce-models true)\n(set-logic QF_UFLIA)\n");
+	write("(set-option :produce-models true)");
+	write("(set-logic QF_UFLIA)");
 }
 
 void SMTLib2Interface::push()
 {
 	m_accumulatedOutput.emplace_back();
-	//write("(push)\n");
 }
 
 void SMTLib2Interface::pop()
 {
-	//write("(pop)\n");
 	solAssert(!m_accumulatedOutput.empty(), "");
 	m_accumulatedOutput.pop_back();
 }
@@ -136,50 +69,34 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom
 		(_domain == Sort::Int ? "Int" : "Bool") +
 		") " +
 		(_codomain == Sort::Int ? "Int" : "Bool") +
-		")\n"
+		")"
 	);
-	return Expression(_name, {});
+	return Expression(std::move(_name), {});
 }
 
 Expression SMTLib2Interface::newInteger(string _name)
 {
-	write("(declare-const |" + _name + "| Int)\n");
-	return Expression(_name, {});
+	write("(declare-const |" + _name + "| Int)");
+	return Expression(std::move(_name), {});
 }
 
 Expression SMTLib2Interface::newBool(string _name)
 {
-	write("(declare-const |" + _name + "| Bool)\n");
-	return Expression(_name, {});
+	write("(declare-const |" + _name + "| Bool)");
+	return Expression(std::move(_name), {});
 }
 
-void SMTLib2Interface::addAssertion(Expression _expr)
+void SMTLib2Interface::addAssertion(Expression const& _expr)
 {
-	write("(assert " + _expr.toSExpr() + ")\n");
+	write("(assert " + _expr.toSExpr() + ")");
 }
 
 pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate)
 {
-	string checks;
-	if (_expressionsToEvaluate.empty())
-		checks = "(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...
-			checks += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n";
-			checks += "(assert (= |EVALEXPR_" + to_string(i) + "| " + e.toSExpr() + "))\n";
-		}
-		checks += "(check-sat)\n";
-		checks += "(get-value (";
-		for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
-			checks += "|EVALEXPR_" + to_string(i) + "| ";
-		checks += "))\n";
-	}
-	string response = communicate(boost::algorithm::join(m_accumulatedOutput, "\n") + checks);
+	string response = m_communicator.communicate(
+		boost::algorithm::join(m_accumulatedOutput, "\n") +
+		checkSatAndGetValuesCommand(_expressionsToEvaluate)
+	);
 	CheckResult result;
 	// TODO proper parsing
 	if (boost::starts_with(response, "sat\n"))
@@ -189,44 +106,43 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con
 	else if (boost::starts_with(response, "unknown\n"))
 		result = CheckResult::UNKNOWN;
 	else
-		solAssert(false, "Invalid response to check-sat: " + response);
+		result = CheckResult::ERROR;
 
 	vector<string> values;
-	if (result != CheckResult::UNSAT)
+	if (result != CheckResult::UNSAT && result != CheckResult::ERROR)
 		values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend());
 	return make_pair(result, values);
 }
 
-//string SMTLib2Interface::eval(Expression _expr)
-//{
-//	write("(get-value (" + _expr.toSExpr() + ")\n");
-//	std::string reply = communicate();
-//	cout << "<-- Z3: " << reply << endl;
-//	// TODO parse
-//	return reply;
-//}
-
 void SMTLib2Interface::write(string _data)
 {
-//	cout << " --> Z3: " << _data << endl;
-//	solAssert(m_solverWrite, "");
-//	solAssert(fputs(_data.c_str(), m_solverWrite) >= 0 || true, "EOF while communicating with Z3.");
-//	solAssert(fflush(m_solverWrite) == 0 || true, "");
 	solAssert(!m_accumulatedOutput.empty(), "");
-	m_accumulatedOutput.back() += move(_data);
+	m_accumulatedOutput.back() += move(_data) + "\n";
 }
 
-string SMTLib2Interface::communicate(std::string const& _input)
+string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _expressionsToEvaluate)
 {
-	ofstream("/tmp/z3exchange.smt2") << _input << "(exit)" << endl;
-	FILE* solverOutput = popen("z3 -smt2 /tmp/z3exchange.smt2", "r");
-	string result;
-	array<char, 128> buffer;
-	while (!feof(solverOutput))
-		if (fgets(buffer.data(), 127, solverOutput) != nullptr)
-			result += buffer.data();
-	fclose(solverOutput);
-	return result;
+	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) + "| " + e.toSExpr() + "))\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)
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index b7bab043..d8c11df9 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -17,10 +17,15 @@
 
 #pragma once
 
+#include <libsolidity/formal/SMTSolverCommunicator.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>
@@ -35,7 +40,7 @@ namespace smt
 
 enum class CheckResult
 {
-	SAT, UNSAT, UNKNOWN
+	SAT, UNSAT, UNKNOWN, ERROR
 };
 
 enum class Sort
@@ -43,6 +48,7 @@ enum class Sort
 	Int, Bool
 };
 
+/// C++ representation of an SMTLIB2 expression.
 class Expression
 {
 	friend class SMTLib2Interface;
@@ -62,23 +68,23 @@ public:
 
 	friend Expression operator!(Expression _a)
 	{
-		return Expression("not", _a);
+		return Expression("not", std::move(_a));
 	}
 	friend Expression operator&&(Expression _a, Expression _b)
 	{
-		return Expression("and", _a, _b);
+		return Expression("and", std::move(_a), std::move(_b));
 	}
 	friend Expression operator||(Expression _a, Expression _b)
 	{
-		return Expression("or", _a, _b);
+		return Expression("or", std::move(_a), std::move(_b));
 	}
 	friend Expression operator==(Expression _a, Expression _b)
 	{
-		return Expression("=", _a, _b);
+		return Expression("=", std::move(_a), std::move(_b));
 	}
 	friend Expression operator!=(Expression _a, Expression _b)
 	{
-		return !(_a == _b);
+		return !(std::move(_a) == std::move(_b));
 	}
 	friend Expression operator<(Expression _a, Expression _b)
 	{
@@ -140,8 +146,7 @@ private:
 class SMTLib2Interface: public boost::noncopyable
 {
 public:
-	SMTLib2Interface();
-	~SMTLib2Interface();
+	SMTLib2Interface(ReadFile::Callback const& _readFileCallback);
 
 	void reset();
 
@@ -152,19 +157,17 @@ public:
 	Expression newInteger(std::string _name);
 	Expression newBool(std::string _name);
 
-	void addAssertion(Expression _expr);
+	void addAssertion(Expression const& _expr);
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate);
-//	std::string eval(Expression _expr);
 
 private:
 	void write(std::string _data);
-	std::string communicate(std::string const& _input);
 
+	std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
 	std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
 
+	SMTSolverCommunicator m_communicator;
 	std::vector<std::string> m_accumulatedOutput;
-//	FILE* m_solverWrite = nullptr;
-//	FILE* m_solverRead = nullptr;
 };
 
 
diff --git a/libsolidity/formal/SMTSolverCommunicator.cpp b/libsolidity/formal/SMTSolverCommunicator.cpp
new file mode 100644
index 00000000..a97e5fcc
--- /dev/null
+++ b/libsolidity/formal/SMTSolverCommunicator.cpp
@@ -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/>.
+*/
+
+#include <libsolidity/formal/SMTSolverCommunicator.h>
+
+#include <libdevcore/Common.h>
+
+#include <boost/filesystem/operations.hpp>
+
+#include <fstream>
+
+#include <stdio.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity::smt;
+
+#ifdef EMSCRIPTEN
+
+string SMTSolverCommunicator::communicate(string const& _input)
+{
+	auto result = m_readFileCallback("SMTLIB2Solver>> " + _input);
+	if (result.success)
+		return result.contentsOrErrorMessage;
+	else
+		return "";
+}
+
+#else
+
+#ifndef _WIN32
+inline FILE* _popen(char const* command, char const* type)
+{
+	return popen(command, type);
+}
+inline int _pclose(FILE* file)
+{
+	return pclose(file);
+}
+#endif
+
+string SMTSolverCommunicator::communicate(string const& _input)
+{
+	namespace fs = boost::filesystem;
+	auto tempPath = fs::unique_path(fs::temp_directory_path() / "%%%%-%%%%-%%%%.smt2");
+	ScopeGuard s1([&]() { fs::remove(tempPath); });
+	ofstream(tempPath.string()) << _input << "(exit)" << endl;
+
+	// TODO Escaping might not be 100% perfect.
+	FILE* solverOutput = _popen(("z3 -smt2 \"" + tempPath.string() + "\"").c_str(), "r");
+	ScopeGuard s2([&]() { _pclose(solverOutput); });
+
+	string result;
+	array<char, 128> buffer;
+	while (!feof(solverOutput))
+		if (fgets(buffer.data(), 127, solverOutput) != nullptr)
+			result += buffer.data();
+	return result;
+}
+
+#endif
diff --git a/libsolidity/formal/SMTSolverCommunicator.h b/libsolidity/formal/SMTSolverCommunicator.h
new file mode 100644
index 00000000..25aeba61
--- /dev/null
+++ b/libsolidity/formal/SMTSolverCommunicator.h
@@ -0,0 +1,50 @@
+/*
+	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/ReadFile.h>
+
+#include <string>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+/// Platform-specific way to access the SMT solver.
+class SMTSolverCommunicator
+{
+public:
+	/// Creates the communicator, the read file callback is used only
+	/// on the emscripten platform.
+	SMTSolverCommunicator(ReadFile::Callback const& _readFileCallback):
+		m_readFileCallback(_readFileCallback)
+	{}
+
+	std::string communicate(std::string const& _input);
+
+private:
+	ReadFile::Callback m_readFileCallback;
+};
+
+
+}
+}
+}