Merge pull request #5416 from ethereum/develop

Merge develop into release for 0.5.0

25 files changed, 1265 insertions, 712 deletions

diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
index dba5823a..6cb91483 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -37,6 +37,7 @@ void CVC4Interface::reset()
 	m_functions.clear();
 	m_solver.reset();
 	m_solver.setOption("produce-models", true);
+	m_solver.setTimeLimit(queryTimeout);
 }
 
 void CVC4Interface::push()
@@ -49,23 +50,25 @@ void CVC4Interface::pop()
 	m_solver.pop();
 }
 
-Expression CVC4Interface::newFunction(string _name, Sort _domain, Sort _codomain)
+void CVC4Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
 {
-	CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain));
-	m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)});
-	return SolverInterface::newFunction(move(_name), _domain, _codomain);
+	if (!m_functions.count(_name))
+	{
+		CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain));
+		m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)});
+	}
 }
 
-Expression CVC4Interface::newInteger(string _name)
+void CVC4Interface::declareInteger(string _name)
 {
-	m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())});
-	return SolverInterface::newInteger(move(_name));
+	if (!m_constants.count(_name))
+		m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())});
 }
 
-Expression CVC4Interface::newBool(string _name)
+void CVC4Interface::declareBool(string _name)
 {
-	m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())});
-	return SolverInterface::newBool(std::move(_name));
+	if (!m_constants.count(_name))
+		m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())});
 }
 
 void CVC4Interface::addAssertion(Expression const& _expr)
@@ -109,13 +112,13 @@ pair<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> const&
 			solAssert(false, "");
 		}
 
-		if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty())
+		if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty())
 		{
 			for (Expression const& e: _expressionsToEvaluate)
 				values.push_back(toString(m_solver.getValue(toCVC4Expr(e))));
 		}
 	}
-	catch (CVC4::Exception & e)
+	catch (CVC4::Exception const&)
 	{
 		result = CheckResult::ERROR;
 		values.clear();
diff --git a/libsolidity/formal/CVC4Interface.h b/libsolidity/formal/CVC4Interface.h
index cfaeb412..cd6d761d 100644
--- a/libsolidity/formal/CVC4Interface.h
+++ b/libsolidity/formal/CVC4Interface.h
@@ -21,8 +21,19 @@
 
 #include <boost/noncopyable.hpp>
 
+#if defined(__GLIBC__)
+// The CVC4 headers includes the deprecated system headers <ext/hash_map>
+// and <ext/hash_set>. These headers cause a warning that will break the
+// build, unless _GLIBCXX_PERMIT_BACKWARD_HASH is set.
+#define _GLIBCXX_PERMIT_BACKWARD_HASH
+#endif
+
 #include <cvc4/cvc4.h>
 
+#if defined(__GLIBC__)
+#undef _GLIBCXX_PERMIT_BACKWARD_HASH
+#endif
+
 namespace dev
 {
 namespace solidity
@@ -40,9 +51,9 @@ public:
 	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 declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+	void declareInteger(std::string _name) override;
+	void declareBool(std::string _name) override;
 
 	void addAssertion(Expression const& _expr) override;
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 425c5c1e..cc580021 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -17,17 +17,10 @@
 
 #include <libsolidity/formal/SMTChecker.h>
 
-#ifdef HAVE_Z3
-#include <libsolidity/formal/Z3Interface.h>
-#elif HAVE_CVC4
-#include <libsolidity/formal/CVC4Interface.h>
-#else
-#include <libsolidity/formal/SMTLib2Interface.h>
-#endif
-
-#include <libsolidity/formal/SSAVariable.h>
-#include <libsolidity/formal/SymbolicIntVariable.h>
+#include <libsolidity/formal/SMTPortfolio.h>
+
 #include <libsolidity/formal/VariableUsage.h>
+#include <libsolidity/formal/SymbolicTypes.h>
 
 #include <libsolidity/interface/ErrorReporter.h>
 
@@ -39,21 +32,15 @@ using namespace dev;
 using namespace dev::solidity;
 
 SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
-#ifdef HAVE_Z3
-	m_interface(make_shared<smt::Z3Interface>()),
-#elif HAVE_CVC4
-	m_interface(make_shared<smt::CVC4Interface>()),
-#else
-	m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)),
-#endif
+	m_interface(make_shared<smt::SMTPortfolio>(_readFileCallback)),
 	m_errorReporter(_errorReporter)
 {
-	(void)_readFileCallback;
 }
 
-void SMTChecker::analyze(SourceUnit const& _source)
+void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
 {
 	m_variableUsage = make_shared<VariableUsage>(_source);
+	m_scanner = _scanner;
 	if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		_source.accept(*this);
 }
@@ -68,7 +55,7 @@ bool SMTChecker::visit(ContractDefinition const& _contract)
 
 void SMTChecker::endVisit(ContractDefinition const&)
 {
-	m_stateVariables.clear();
+	m_variables.clear();
 }
 
 void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
@@ -84,45 +71,54 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 			_function.location(),
 			"Assertion checker does not yet support constructors and functions with modifiers."
 		);
-	m_currentFunction = &_function;
-	m_interface->reset();
-	m_variables.clear();
-	m_variables.insert(m_stateVariables.begin(), m_stateVariables.end());
-	m_pathConditions.clear();
+	m_functionPath.push_back(&_function);
+	// Not visited by a function call
+	if (isRootFunction())
+	{
+		m_interface->reset();
+		m_pathConditions.clear();
+		m_expressions.clear();
+		resetStateVariables();
+		initializeLocalVariables(_function);
+	}
+
 	m_loopExecutionHappened = false;
-	initializeLocalVariables(_function);
-	resetStateVariables();
 	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 at the beginning of the function.
-	// If we add storage variables, those should be cleared differently.
-	m_currentFunction = nullptr;
+	// If _function was visited from a function call we don't remove
+	// the local variables just yet, since we might need them for
+	// future calls.
+	// Otherwise we remove any local variables from the context and
+	// keep the state variables.
+	if (isRootFunction())
+		removeLocalVariables();
+	m_functionPath.pop_back();
 }
 
 bool SMTChecker::visit(IfStatement const& _node)
 {
 	_node.condition().accept(*this);
 
-	checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
+	// We ignore called functions here because they have
+	// specific input values.
+	if (isRootFunction())
+		checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
 
-	auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
-	vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
-	decltype(countersEndTrue) countersEndFalse;
+	auto indicesEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
+	vector<VariableDeclaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
+	decltype(indicesEndTrue) indicesEndFalse;
 	if (_node.falseStatement())
 	{
-		countersEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition()));
+		indicesEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition()));
 		touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
 	}
 	else
-	{
-		countersEndFalse = m_variables;
-	}
+		indicesEndFalse = copyVariableIndices();
 
-	mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse);
+	mergeVariables(touchedVariables, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
 
 	return false;
 }
@@ -136,12 +132,14 @@ bool SMTChecker::visit(WhileStatement const& _node)
 		visitBranch(_node.body());
 		// TODO the assertions generated in the body should still be active in the condition
 		_node.condition().accept(*this);
-		checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE.");
+		if (isRootFunction())
+			checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE.");
 	}
 	else
 	{
 		_node.condition().accept(*this);
-		checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
+		if (isRootFunction())
+			checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
 
 		visitBranch(_node.body(), expr(_node.condition()));
 	}
@@ -172,10 +170,10 @@ bool SMTChecker::visit(ForStatement const& _node)
 	if (_node.condition())
 	{
 		_node.condition()->accept(*this);
-		checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
+		if (isRootFunction())
+			checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
 	}
 
-	VariableSequenceCounters sequenceCountersStart = m_variables;
 	m_interface->push();
 	if (_node.condition())
 		m_interface->addAssertion(expr(*_node.condition()));
@@ -186,7 +184,6 @@ bool SMTChecker::visit(ForStatement const& _node)
 	m_interface->pop();
 
 	m_loopExecutionHappened = true;
-	std::swap(sequenceCountersStart, m_variables);
 
 	resetVariables(touchedVariables);
 
@@ -212,28 +209,24 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
 		);
 }
 
-void SMTChecker::endVisit(ExpressionStatement const&)
-{
-}
-
 void SMTChecker::endVisit(Assignment const& _assignment)
 {
-	if (_assignment.assignmentOperator() != Token::Value::Assign)
+	if (_assignment.assignmentOperator() != Token::Assign)
 		m_errorReporter.warning(
 			_assignment.location(),
 			"Assertion checker does not yet implement compound assignment."
 		);
-	else if (!SSAVariable::isSupportedType(_assignment.annotation().type->category()))
+	else if (!isSupportedType(_assignment.annotation().type->category()))
 		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))
+		VariableDeclaration const& decl = dynamic_cast<VariableDeclaration const&>(*identifier->annotation().referencedDeclaration);
+		if (knownVariable(decl))
 		{
-			assignment(*decl, _assignment.rightHandSide(), _assignment.location());
+			assignment(decl, _assignment.rightHandSide(), _assignment.location());
 			defineExpr(_assignment, expr(_assignment.rightHandSide()));
 		}
 		else
@@ -254,7 +247,7 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
 	if (_tuple.isInlineArray() || _tuple.components().size() != 1)
 		m_errorReporter.warning(
 			_tuple.location(),
-			"Assertion checker does not yet implement tules and inline arrays."
+			"Assertion checker does not yet implement tuples and inline arrays."
 		);
 	else
 		defineExpr(_tuple, expr(*_tuple.components()[0]));
@@ -263,17 +256,17 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
 void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location)
 {
 	checkCondition(
-		_value < SymbolicIntVariable::minValue(_type),
+		_value < minValue(_type),
 		_location,
 		"Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
-		"value",
+		"<result>",
 		&_value
 	);
 	checkCondition(
-		_value > SymbolicIntVariable::maxValue(_type),
+		_value > maxValue(_type),
 		_location,
 		"Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
-		"value",
+		"<result>",
 		&_value
 	);
 }
@@ -284,7 +277,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
 	{
 	case Token::Not: // !
 	{
-		solAssert(SSAVariable::isBool(_op.annotation().type->category()), "");
+		solAssert(isBool(_op.annotation().type->category()), "");
 		defineExpr(_op, !expr(_op.subExpression()));
 		break;
 	}
@@ -292,16 +285,16 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
 	case Token::Dec: // -- (pre- or postfix)
 	{
 
-		solAssert(SSAVariable::isInteger(_op.annotation().type->category()), "");
+		solAssert(isInteger(_op.annotation().type->category()), "");
 		solAssert(_op.subExpression().annotation().lValueRequested, "");
 		if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
 		{
-			Declaration const* decl = identifier->annotation().referencedDeclaration;
-			if (knownVariable(*decl))
+			VariableDeclaration const& decl = dynamic_cast<VariableDeclaration const&>(*identifier->annotation().referencedDeclaration);
+			if (knownVariable(decl))
 			{
-				auto innerValue = currentValue(*decl);
+				auto innerValue = currentValue(decl);
 				auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
-				assignment(*decl, newValue, _op.location());
+				assignment(decl, newValue, _op.location());
 				defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
 			}
 			else
@@ -337,11 +330,11 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
 
 void SMTChecker::endVisit(BinaryOperation const& _op)
 {
-	if (Token::isArithmeticOp(_op.getOperator()))
+	if (TokenTraits::isArithmeticOp(_op.getOperator()))
 		arithmeticOperation(_op);
-	else if (Token::isCompareOp(_op.getOperator()))
+	else if (TokenTraits::isCompareOp(_op.getOperator()))
 		compareOperation(_op);
-	else if (Token::isBooleanOp(_op.getOperator()))
+	else if (TokenTraits::isBooleanOp(_op.getOperator()))
 		booleanOperation(_op);
 	else
 		m_errorReporter.warning(
@@ -366,49 +359,162 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 
 	std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
 	if (funType.kind() == FunctionType::Kind::Assert)
-	{
-		solAssert(args.size() == 1, "");
-		solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
-		checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
-		addPathImpliedExpression(expr(*args[0]));
-	}
+		visitAssert(_funCall);
 	else if (funType.kind() == FunctionType::Kind::Require)
+		visitRequire(_funCall);
+	else if (funType.kind() == FunctionType::Kind::GasLeft)
+		visitGasLeft(_funCall);
+	else if (funType.kind() == FunctionType::Kind::BlockHash)
+		visitBlockHash(_funCall);
+	else if (funType.kind() == FunctionType::Kind::Internal)
+		inlineFunctionCall(_funCall);
+	else
 	{
-		solAssert(args.size() == 1, "");
-		solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
+		m_errorReporter.warning(
+			_funCall.location(),
+			"Assertion checker does not yet implement this type of function call."
+		);
+	}
+}
+
+void SMTChecker::visitAssert(FunctionCall const& _funCall)
+{
+	auto const& args = _funCall.arguments();
+	solAssert(args.size() == 1, "");
+	solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
+	checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
+	addPathImpliedExpression(expr(*args[0]));
+}
+
+void SMTChecker::visitRequire(FunctionCall const& _funCall)
+{
+	auto const& args = _funCall.arguments();
+	solAssert(args.size() == 1, "");
+	solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
+	if (isRootFunction())
 		checkBooleanNotConstant(*args[0], "Condition is always $VALUE.");
-		addPathImpliedExpression(expr(*args[0]));
+	addPathImpliedExpression(expr(*args[0]));
+}
+
+void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
+{
+	string gasLeft = "gasleft()";
+	// We increase the variable index since gasleft changes
+	// inside a tx.
+	defineSpecialVariable(gasLeft, _funCall, true);
+	auto const& symbolicVar = m_specialVariables.at(gasLeft);
+	unsigned index = symbolicVar->index();
+	// We set the current value to unknown anyway to add type constraints.
+	symbolicVar->setUnknownValue();
+	if (index > 0)
+		m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
+}
+
+void SMTChecker::visitBlockHash(FunctionCall const& _funCall)
+{
+	string blockHash = "blockhash()";
+	// TODO Define blockhash as an uninterpreted function
+	defineSpecialVariable(blockHash, _funCall);
+}
+
+void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
+{
+	FunctionDefinition const* _funDef = nullptr;
+	Expression const* _calledExpr = &_funCall.expression();
+
+	if (TupleExpression const* _fun = dynamic_cast<TupleExpression const*>(&_funCall.expression()))
+	{
+		solAssert(_fun->components().size() == 1, "");
+		_calledExpr = _fun->components().at(0).get();
+	}
+
+	if (Identifier const* _fun = dynamic_cast<Identifier const*>(_calledExpr))
+		_funDef = dynamic_cast<FunctionDefinition const*>(_fun->annotation().referencedDeclaration);
+	else if (MemberAccess const* _fun = dynamic_cast<MemberAccess const*>(_calledExpr))
+		_funDef = dynamic_cast<FunctionDefinition const*>(_fun->annotation().referencedDeclaration);
+	else
+	{
+		m_errorReporter.warning(
+			_funCall.location(),
+			"Assertion checker does not yet implement this type of function call."
+		);
+		return;
+	}
+	solAssert(_funDef, "");
+
+	if (visitedFunction(_funDef))
+		m_errorReporter.warning(
+			_funCall.location(),
+			"Assertion checker does not support recursive function calls.",
+			SecondarySourceLocation().append("Starting from function:", _funDef->location())
+		);
+	else if (_funDef && _funDef->isImplemented())
+	{
+		vector<smt::Expression> funArgs;
+		for (auto arg: _funCall.arguments())
+			funArgs.push_back(expr(*arg));
+		initializeFunctionCallParameters(*_funDef, funArgs);
+		_funDef->accept(*this);
+		auto const& returnParams = _funDef->returnParameters();
+		if (_funDef->returnParameters().size())
+		{
+			if (returnParams.size() > 1)
+				m_errorReporter.warning(
+					_funCall.location(),
+					"Assertion checker does not yet support calls to functions that return more than one value."
+				);
+			else
+				defineExpr(_funCall, currentValue(*returnParams[0]));
+		}
+	}
+	else
+	{
+		m_errorReporter.warning(
+			_funCall.location(),
+			"Assertion checker does not support calls to functions without implementation."
+		);
 	}
 }
 
 void SMTChecker::endVisit(Identifier const& _identifier)
 {
-	Declaration const* decl = _identifier.annotation().referencedDeclaration;
-	solAssert(decl, "");
 	if (_identifier.annotation().lValueRequested)
 	{
 		// Will be translated as part of the node that requested the lvalue.
 	}
-	else if (SSAVariable::isSupportedType(_identifier.annotation().type->category()))
-		defineExpr(_identifier, currentValue(*decl));
 	else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
 	{
-		if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
+		if (
+			fun->kind() == FunctionType::Kind::Assert ||
+			fun->kind() == FunctionType::Kind::Require ||
+			fun->kind() == FunctionType::Kind::GasLeft ||
+			fun->kind() == FunctionType::Kind::BlockHash
+		)
 			return;
+		createExpr(_identifier);
+	}
+	else if (isSupportedType(_identifier.annotation().type->category()))
+	{
+		if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
+			defineExpr(_identifier, currentValue(*decl));
+		else if (_identifier.name() == "now")
+			defineSpecialVariable(_identifier.name(), _identifier);
+		else
+			// TODO: handle MagicVariableDeclaration here
+			m_errorReporter.warning(
+				_identifier.location(),
+				"Assertion checker does not yet support the type of this variable."
+			);
 	}
 }
 
 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(), "");
+	if (isNumber(type.category()))
 
 		defineExpr(_literal, smt::Expression(type.literalValue(&_literal)));
-	}
-	else if (type.category() == Type::Category::Bool)
+	else if (isBool(type.category()))
 		defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
 	else
 		m_errorReporter.warning(
@@ -419,6 +525,69 @@ void SMTChecker::endVisit(Literal const& _literal)
 		);
 }
 
+void SMTChecker::endVisit(Return const& _return)
+{
+	if (knownExpr(*_return.expression()))
+	{
+		auto returnParams = m_functionPath.back()->returnParameters();
+		if (returnParams.size() > 1)
+			m_errorReporter.warning(
+				_return.location(),
+				"Assertion checker does not yet support more than one return value."
+			);
+		else if (returnParams.size() == 1)
+			m_interface->addAssertion(expr(*_return.expression()) == newValue(*returnParams[0]));
+	}
+}
+
+bool SMTChecker::visit(MemberAccess const& _memberAccess)
+{
+	auto const& exprType = _memberAccess.expression().annotation().type;
+	solAssert(exprType, "");
+	if (exprType->category() == Type::Category::Magic)
+	{
+		auto identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression());
+		string accessedName;
+		if (identifier)
+			accessedName = identifier->name();
+		else
+			m_errorReporter.warning(
+				_memberAccess.location(),
+				"Assertion checker does not yet support this expression."
+			);
+		defineSpecialVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
+		return false;
+	}
+	else
+		m_errorReporter.warning(
+			_memberAccess.location(),
+			"Assertion checker does not yet support this expression."
+		);
+
+	return true;
+}
+
+void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
+{
+	if (!knownSpecialVariable(_name))
+	{
+		auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
+		m_specialVariables.emplace(_name, result.second);
+		result.second->setUnknownValue();
+		if (result.first)
+			m_errorReporter.warning(
+				_expr.location(),
+				"Assertion checker does not yet support this special variable."
+			);
+	}
+	else if (_increaseIndex)
+		m_specialVariables.at(_name)->increaseIndex();
+	// The default behavior is not to increase the index since
+	// most of the special values stay the same throughout a tx.
+	defineExpr(_expr, m_specialVariables.at(_name)->currentValue());
+}
+
+
 void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 {
 	switch (_op.getOperator())
@@ -429,11 +598,18 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 	case Token::Div:
 	{
 		solAssert(_op.annotation().commonType, "");
-		solAssert(_op.annotation().commonType->category() == Type::Category::Integer, "");
+		if (_op.annotation().commonType->category() != Type::Category::Integer)
+		{
+			m_errorReporter.warning(
+				_op.location(),
+				"Assertion checker does not yet implement this operator on non-integer types."
+			);
+			break;
+		}
 		auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType);
 		smt::Expression left(expr(_op.leftExpression()));
 		smt::Expression right(expr(_op.rightExpression()));
-		Token::Value op = _op.getOperator();
+		Token op = _op.getOperator();
 		smt::Expression value(
 			op == Token::Add ? left + right :
 			op == Token::Sub ? left - right :
@@ -443,7 +619,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 
 		if (_op.getOperator() == Token::Div)
 		{
-			checkCondition(right == 0, _op.location(), "Division by zero", "value", &right);
+			checkCondition(right == 0, _op.location(), "Division by zero", "<result>", &right);
 			m_interface->addAssertion(right != 0);
 		}
 
@@ -463,13 +639,13 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 void SMTChecker::compareOperation(BinaryOperation const& _op)
 {
 	solAssert(_op.annotation().commonType, "");
-	if (SSAVariable::isSupportedType(_op.annotation().commonType->category()))
+	if (isSupportedType(_op.annotation().commonType->category()))
 	{
 		smt::Expression left(expr(_op.leftExpression()));
 		smt::Expression right(expr(_op.rightExpression()));
-		Token::Value op = _op.getOperator();
+		Token op = _op.getOperator();
 		shared_ptr<smt::Expression> value;
-		if (SSAVariable::isInteger(_op.annotation().commonType->category()))
+		if (isNumber(_op.annotation().commonType->category()))
 		{
 			value = make_shared<smt::Expression>(
 				op == Token::Equal ? (left == right) :
@@ -482,14 +658,10 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
 		}
 		else // Bool
 		{
-			solUnimplementedAssert(SSAVariable::isBool(_op.annotation().commonType->category()), "Operation not yet supported");
+			solUnimplementedAssert(isBool(_op.annotation().commonType->category()), "Operation not yet supported");
 			value = make_shared<smt::Expression>(
 				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)
+				/*op == Token::NotEqual*/ (left != right)
 			);
 		}
 		// TODO: check that other values for op are not possible.
@@ -534,37 +706,37 @@ smt::Expression SMTChecker::division(smt::Expression _left, smt::Expression _rig
 		return _left / _right;
 }
 
-void SMTChecker::assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location)
+void SMTChecker::assignment(VariableDeclaration const& _variable, Expression const& _value, SourceLocation const& _location)
 {
 	assignment(_variable, expr(_value), _location);
 }
 
-void SMTChecker::assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location)
+void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location)
 {
 	TypePointer type = _variable.type();
 	if (auto const* intType = dynamic_cast<IntegerType const*>(type.get()))
 		checkUnderOverflow(_value, *intType, _location);
+	else if (dynamic_cast<AddressType const*>(type.get()))
+		checkUnderOverflow(_value, IntegerType(160), _location);
 	m_interface->addAssertion(newValue(_variable) == _value);
 }
 
-SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
+SMTChecker::VariableIndices SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
 {
 	return visitBranch(_statement, &_condition);
 }
 
-SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
+SMTChecker::VariableIndices SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
 {
-	VariableSequenceCounters beforeVars = m_variables;
-
+	auto indicesBeforeBranch = copyVariableIndices();
 	if (_condition)
 		pushPathCondition(*_condition);
 	_statement.accept(*this);
 	if (_condition)
 		popPathCondition();
-
-	std::swap(m_variables, beforeVars);
-
-	return beforeVars;
+	auto indicesAfterBranch = copyVariableIndices();
+	resetVariableIndices(indicesBeforeBranch);
+	return indicesAfterBranch;
 }
 
 void SMTChecker::checkCondition(
@@ -580,31 +752,24 @@ void SMTChecker::checkCondition(
 
 	vector<smt::Expression> expressionsToEvaluate;
 	vector<string> expressionNames;
-	if (m_currentFunction)
+	if (m_functionPath.size())
 	{
+		solAssert(m_scanner, "");
 		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());
-			}
-		for (auto const& var: m_stateVariables)
-			if (knownVariable(*var.first))
-			{
-				expressionsToEvaluate.emplace_back(currentValue(*var.first));
-				expressionNames.push_back(var.first->name());
-			}
+		for (auto const& var: m_variables)
+		{
+			expressionsToEvaluate.emplace_back(currentValue(*var.first));
+			expressionNames.push_back(var.first->name());
+		}
+		for (auto const& var: m_specialVariables)
+		{
+			expressionsToEvaluate.emplace_back(var.second->currentValue());
+			expressionNames.push_back(var.first);
+		}
 	}
 	smt::CheckResult result;
 	vector<string> values;
@@ -621,17 +786,25 @@ void SMTChecker::checkCondition(
 	{
 		std::ostringstream message;
 		message << _description << " happens here";
-		if (m_currentFunction)
+		if (m_functionPath.size())
 		{
-			message << " for:\n";
+			std::ostringstream modelMessage;
+			modelMessage << "  for:\n";
 			solAssert(values.size() == expressionNames.size(), "");
+			map<string, string> sortedModel;
 			for (size_t i = 0; i < values.size(); ++i)
 				if (expressionsToEvaluate.at(i).name != values.at(i))
-					message << "  " << expressionNames.at(i) << " = " << values.at(i) << "\n";
+					sortedModel[expressionNames.at(i)] = values.at(i);
+
+			for (auto const& eval: sortedModel)
+				modelMessage << "  " << eval.first << " = " << eval.second << "\n";
+			m_errorReporter.warning(_location, message.str() + loopComment, SecondarySourceLocation().append(modelMessage.str(), SourceLocation()));
 		}
 		else
+		{
 			message << ".";
-		m_errorReporter.warning(_location, message.str() + loopComment);
+			m_errorReporter.warning(_location, message.str() + loopComment);
+		}
 		break;
 	}
 	case smt::CheckResult::UNSATISFIABLE:
@@ -639,11 +812,12 @@ void SMTChecker::checkCondition(
 	case smt::CheckResult::UNKNOWN:
 		m_errorReporter.warning(_location, _description + " might happen here." + loopComment);
 		break;
+	case smt::CheckResult::CONFLICTING:
+		m_errorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
+		break;
 	case smt::CheckResult::ERROR:
 		m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
 		break;
-	default:
-		solAssert(false, "");
 	}
 	m_interface->pop();
 }
@@ -666,6 +840,8 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
 
 	if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
 		m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver.");
+	else if (positiveResult == smt::CheckResult::CONFLICTING || negatedResult == smt::CheckResult::CONFLICTING)
+		m_errorReporter.warning(_condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound.");
 	else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE)
 	{
 		// everything fine.
@@ -726,6 +902,30 @@ smt::CheckResult SMTChecker::checkSatisfiable()
 	return checkSatisfiableAndGenerateModel({}).first;
 }
 
+void SMTChecker::initializeFunctionCallParameters(FunctionDefinition const& _function, vector<smt::Expression> const& _callArgs)
+{
+	auto const& funParams = _function.parameters();
+	solAssert(funParams.size() == _callArgs.size(), "");
+	for (unsigned i = 0; i < funParams.size(); ++i)
+		if (createVariable(*funParams[i]))
+			m_interface->addAssertion(_callArgs[i] == newValue(*funParams[i]));
+
+	for (auto const& variable: _function.localVariables())
+		if (createVariable(*variable))
+		{
+			newValue(*variable);
+			setZeroValue(*variable);
+		}
+
+	if (_function.returnParameterList())
+		for (auto const& retParam: _function.returnParameters())
+			if (createVariable(*retParam))
+			{
+				newValue(*retParam);
+				setZeroValue(*retParam);
+			}
+}
+
 void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
 {
 	for (auto const& variable: _function.localVariables())
@@ -742,16 +942,30 @@ void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
 				setZeroValue(*retParam);
 }
 
+void SMTChecker::removeLocalVariables()
+{
+	for (auto it = m_variables.begin(); it != m_variables.end(); )
+	{
+		if (it->first->isLocalVariable())
+			it = m_variables.erase(it);
+		else
+			++it;
+	}
+}
+
 void SMTChecker::resetStateVariables()
 {
-	for (auto const& variable: m_stateVariables)
+	for (auto const& variable: m_variables)
 	{
-		newValue(*variable.first);
-		setUnknownValue(*variable.first);
+		if (variable.first->isStateVariable())
+		{
+			newValue(*variable.first);
+			setUnknownValue(*variable.first);
+		}
 	}
 }
 
-void SMTChecker::resetVariables(vector<Declaration const*> _variables)
+void SMTChecker::resetVariables(vector<VariableDeclaration const*> _variables)
 {
 	for (auto const* decl: _variables)
 	{
@@ -760,38 +974,33 @@ void SMTChecker::resetVariables(vector<Declaration const*> _variables)
 	}
 }
 
-void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse)
+void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
 {
-	set<Declaration const*> uniqueVars(_variables.begin(), _variables.end());
+	set<VariableDeclaration const*> uniqueVars(_variables.begin(), _variables.end());
 	for (auto const* decl: uniqueVars)
 	{
-		int trueCounter = _countersEndTrue.at(decl).index();
-		int falseCounter = _countersEndFalse.at(decl).index();
-		solAssert(trueCounter != falseCounter, "");
+		solAssert(_indicesEndTrue.count(decl) && _indicesEndFalse.count(decl), "");
+		int trueIndex = _indicesEndTrue.at(decl);
+		int falseIndex = _indicesEndFalse.at(decl);
+		solAssert(trueIndex != falseIndex, "");
 		m_interface->addAssertion(newValue(*decl) == smt::Expression::ite(
 			_condition,
-			valueAtSequence(*decl, trueCounter),
-			valueAtSequence(*decl, falseCounter))
+			valueAtIndex(*decl, trueIndex),
+			valueAtIndex(*decl, falseIndex))
 		);
 	}
 }
 
 bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 {
-	if (SSAVariable::isSupportedType(_varDecl.type()->category()))
-	{
-		solAssert(m_variables.count(&_varDecl) == 0, "");
-		solAssert(m_stateVariables.count(&_varDecl) == 0, "");
-		if (_varDecl.isLocalVariable())
-			m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));
-		else
-		{
-			solAssert(_varDecl.isStateVariable(), "");
-			m_stateVariables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));
-		}
+	// This might be the case for multiple calls to the same function.
+	if (knownVariable(_varDecl))
 		return true;
-	}
-	else
+	auto const& type = _varDecl.type();
+	solAssert(m_variables.count(&_varDecl) == 0, "");
+	auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface);
+	m_variables.emplace(&_varDecl, result.second);
+	if (result.first)
 	{
 		m_errorReporter.warning(
 			_varDecl.location(),
@@ -799,84 +1008,78 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 		);
 		return false;
 	}
+	return true;
 }
 
-string SMTChecker::uniqueSymbol(Expression const& _expr)
-{
-	return "expr_" + to_string(_expr.id());
-}
-
-bool SMTChecker::knownVariable(Declaration const& _decl)
+bool SMTChecker::knownVariable(VariableDeclaration const& _decl)
 {
 	return m_variables.count(&_decl);
 }
 
-smt::Expression SMTChecker::currentValue(Declaration const& _decl)
+smt::Expression SMTChecker::currentValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	return m_variables.at(&_decl)();
+	return m_variables.at(&_decl)->currentValue();
 }
 
-smt::Expression SMTChecker::valueAtSequence(Declaration const& _decl, int _sequence)
+smt::Expression SMTChecker::valueAtIndex(VariableDeclaration const& _decl, int _index)
 {
 	solAssert(knownVariable(_decl), "");
-	return m_variables.at(&_decl)(_sequence);
+	return m_variables.at(&_decl)->valueAtIndex(_index);
 }
 
-smt::Expression SMTChecker::newValue(Declaration const& _decl)
+smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	++m_variables.at(&_decl);
-	return m_variables.at(&_decl)();
+	return m_variables.at(&_decl)->increaseIndex();
 }
 
-void SMTChecker::setZeroValue(Declaration const& _decl)
+void SMTChecker::setZeroValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	m_variables.at(&_decl).setZeroValue();
+	m_variables.at(&_decl)->setZeroValue();
 }
 
-void SMTChecker::setUnknownValue(Declaration const& _decl)
+void SMTChecker::setUnknownValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	m_variables.at(&_decl).setUnknownValue();
+	m_variables.at(&_decl)->setUnknownValue();
 }
 
 smt::Expression SMTChecker::expr(Expression const& _e)
 {
-	if (!m_expressions.count(&_e))
+	if (!knownExpr(_e))
 	{
 		m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." );
 		createExpr(_e);
 	}
-	return m_expressions.at(&_e);
+	return m_expressions.at(&_e)->currentValue();
+}
+
+bool SMTChecker::knownExpr(Expression const& _e) const
+{
+	return m_expressions.count(&_e);
+}
+
+bool SMTChecker::knownSpecialVariable(string const& _var) const
+{
+	return m_specialVariables.count(_var);
 }
 
 void SMTChecker::createExpr(Expression const& _e)
 {
-	if (m_expressions.count(&_e))
-		m_errorReporter.warning(_e.location(), "Internal error: Expression created twice in SMT solver." );
+	solAssert(_e.annotation().type, "");
+	if (knownExpr(_e))
+		m_expressions.at(&_e)->increaseIndex();
 	else
 	{
-		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:
-			solUnimplementedAssert(false, "Type not implemented.");
-		}
+		auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface);
+		m_expressions.emplace(&_e, result.second);
+		if (result.first)
+			m_errorReporter.warning(
+				_e.location(),
+				"Assertion checker does not yet implement this type."
+			);
 	}
 }
 
@@ -899,7 +1102,7 @@ void SMTChecker::pushPathCondition(smt::Expression const& _e)
 
 smt::Expression SMTChecker::currentPathConditions()
 {
-	if (m_pathConditions.size() == 0)
+	if (m_pathConditions.empty())
 		return smt::Expression(true);
 	return m_pathConditions.back();
 }
@@ -913,3 +1116,27 @@ void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
 {
 	m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e));
 }
+
+bool SMTChecker::isRootFunction()
+{
+	return m_functionPath.size() == 1;
+}
+
+bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef)
+{
+	return contains(m_functionPath, _funDef);
+}
+
+SMTChecker::VariableIndices SMTChecker::copyVariableIndices()
+{
+	VariableIndices indices;
+	for (auto const& var: m_variables)
+		indices.emplace(var.first, var.second->index());
+	return indices;
+}
+
+void SMTChecker::resetVariableIndices(VariableIndices const& _indices)
+{
+	for (auto const& var: _indices)
+		m_variables.at(var.first)->index() = var.second;
+}
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 50d40ab9..a7f955dd 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -19,14 +19,15 @@
 
 
 #include <libsolidity/formal/SolverInterface.h>
-
-#include <libsolidity/formal/SSAVariable.h>
+#include <libsolidity/formal/SymbolicVariables.h>
 
 #include <libsolidity/ast/ASTVisitor.h>
 
 #include <libsolidity/interface/ReadFile.h>
 
-#include <map>
+#include <libsolidity/parsing/Scanner.h>
+
+#include <unordered_map>
 #include <string>
 #include <vector>
 
@@ -43,7 +44,7 @@ class SMTChecker: private ASTConstVisitor
 public:
 	SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback);
 
-	void analyze(SourceUnit const& _sources);
+	void analyze(SourceUnit const& _sources, std::shared_ptr<Scanner> const& _scanner);
 
 private:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
@@ -59,7 +60,6 @@ private:
 	virtual bool visit(WhileStatement const& _node) override;
 	virtual bool visit(ForStatement const& _node) override;
 	virtual void endVisit(VariableDeclarationStatement const& _node) override;
-	virtual void endVisit(ExpressionStatement const& _node) override;
 	virtual void endVisit(Assignment const& _node) override;
 	virtual void endVisit(TupleExpression const& _node) override;
 	virtual void endVisit(UnaryOperation const& _node) override;
@@ -67,26 +67,38 @@ private:
 	virtual void endVisit(FunctionCall const& _node) override;
 	virtual void endVisit(Identifier const& _node) override;
 	virtual void endVisit(Literal const& _node) override;
+	virtual void endVisit(Return const& _node) override;
+	virtual bool visit(MemberAccess const& _node) override;
 
 	void arithmeticOperation(BinaryOperation const& _op);
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 
+	void visitAssert(FunctionCall const&);
+	void visitRequire(FunctionCall const&);
+	void visitGasLeft(FunctionCall const&);
+	void visitBlockHash(FunctionCall const&);
+	/// Visits the FunctionDefinition of the called function
+	/// if available and inlines the return value.
+	void inlineFunctionCall(FunctionCall const&);
+
+	void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
+
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
 	smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
 
-	void assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location);
-	void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
+	void assignment(VariableDeclaration const& _variable, Expression const& _value, SourceLocation const& _location);
+	void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
 
 	/// Maps a variable to an SSA index.
-	using VariableSequenceCounters = std::map<Declaration const*, SSAVariable>;
+	using VariableIndices = std::unordered_map<VariableDeclaration const*, int>;
 
 	/// Visits the branch given by the statement, pushes and pops the current path conditions.
 	/// @param _condition if present, asserts that this condition is true within the branch.
-	/// @returns the variable sequence counter after visiting the branch.
-	VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
-	VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression _condition);
+	/// @returns the variable indices after visiting the branch.
+	VariableIndices visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
+	VariableIndices visitBranch(Statement const& _statement, smt::Expression _condition);
 
 	/// Check that a condition can be satisfied.
 	void checkCondition(
@@ -113,43 +125,47 @@ private:
 	smt::CheckResult checkSatisfiable();
 
 	void initializeLocalVariables(FunctionDefinition const& _function);
+	void initializeFunctionCallParameters(FunctionDefinition const& _function, std::vector<smt::Expression> const& _callArgs);
 	void resetStateVariables();
-	void resetVariables(std::vector<Declaration const*> _variables);
+	void resetVariables(std::vector<VariableDeclaration const*> _variables);
 	/// Given two different branches and the touched variables,
 	/// merge the touched variables into after-branch ite variables
 	/// using the branch condition as guard.
-	void mergeVariables(std::vector<Declaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse);
+	void mergeVariables(std::vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse);
 	/// Tries to create an uninitialized variable and returns true on success.
 	/// This fails if the type is not supported.
 	bool createVariable(VariableDeclaration const& _varDecl);
 
-	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);
+	/// has a valid index
+	bool knownVariable(VariableDeclaration 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);
+	smt::Expression currentValue(VariableDeclaration 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);
+	/// at the given index. Does not ensure that this index exists.
+	smt::Expression valueAtIndex(VariableDeclaration const& _decl, int _index);
+	/// Allocates a new index for the declaration, updates the current
+	/// index to this value and returns the expression.
+	smt::Expression newValue(VariableDeclaration const& _decl);
 
 	/// Sets the value of the declaration to zero.
-	void setZeroValue(Declaration const& _decl);
+	void setZeroValue(VariableDeclaration const& _decl);
 	/// Resets the variable to an unknown value (in its range).
-	void setUnknownValue(Declaration const& decl);
+	void setUnknownValue(VariableDeclaration const& decl);
 
 	/// Returns the expression corresponding to the AST node. Throws if the expression does not exist.
 	smt::Expression expr(Expression const& _e);
 	/// Creates the expression (value can be arbitrary)
 	void createExpr(Expression const& _e);
+	/// Checks if expression was created
+	bool knownExpr(Expression const& _e) const;
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smt::Expression _value);
 
+	/// Checks if special variable was seen.
+	bool knownSpecialVariable(std::string const& _var) const;
+
 	/// Adds a new path condition
 	void pushPathCondition(smt::Expression const& _e);
 	/// Remove the last path condition
@@ -161,16 +177,33 @@ private:
 	/// Add to the solver: the given expression implied by the current path conditions
 	void addPathImpliedExpression(smt::Expression const& _e);
 
+	/// Removes local variables from the context.
+	void removeLocalVariables();
+
+	/// Copy the SSA indices of m_variables.
+	VariableIndices copyVariableIndices();
+	/// Resets the variable indices.
+	void resetVariableIndices(VariableIndices const& _indices);
+
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::shared_ptr<VariableUsage> m_variableUsage;
 	bool m_loopExecutionHappened = false;
-	std::map<Expression const*, smt::Expression> m_expressions;
-	std::map<Declaration const*, SSAVariable> m_variables;
-	std::map<Declaration const*, SSAVariable> m_stateVariables;
+	/// An Expression may have multiple smt::Expression due to
+	/// repeated calls to the same function.
+	std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
+	std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
+	std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_specialVariables;
 	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;
-
-	FunctionDefinition const* m_currentFunction = nullptr;
+	std::shared_ptr<Scanner> m_scanner;
+
+	/// Stores the current path of function calls.
+	std::vector<FunctionDefinition const*> m_functionPath;
+	/// Returns true if the current function was not visited by
+	/// a function call.
+	bool isRootFunction();
+	/// Returns true if _funDef was already visited.
+	bool visitedFunction(FunctionDefinition const* _funDef);
 };
 
 }
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 0e00665a..a6c1f87c 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -47,6 +47,8 @@ void SMTLib2Interface::reset()
 {
 	m_accumulatedOutput.clear();
 	m_accumulatedOutput.emplace_back();
+	m_constants.clear();
+	m_functions.clear();
 	write("(set-option :produce-models true)");
 	write("(set-logic QF_UFLIA)");
 }
@@ -62,30 +64,40 @@ void SMTLib2Interface::pop()
 	m_accumulatedOutput.pop_back();
 }
 
-Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain)
+void SMTLib2Interface::declareFunction(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);
+	// TODO Use domain and codomain as key as well
+	if (!m_functions.count(_name))
+	{
+		m_functions.insert(_name);
+		write(
+			"(declare-fun |" +
+			_name +
+			"| (" +
+			(_domain == Sort::Int ? "Int" : "Bool") +
+			") " +
+			(_codomain == Sort::Int ? "Int" : "Bool") +
+			")"
+		);
+	}
 }
 
-Expression SMTLib2Interface::newInteger(string _name)
+void SMTLib2Interface::declareInteger(string _name)
 {
-	write("(declare-const |" + _name + "| Int)");
-	return SolverInterface::newInteger(move(_name));
+	if (!m_constants.count(_name))
+	{
+		m_constants.insert(_name);
+		write("(declare-const |" + _name + "| Int)");
+	}
 }
 
-Expression SMTLib2Interface::newBool(string _name)
+void SMTLib2Interface::declareBool(string _name)
 {
-	write("(declare-const |" + _name + "| Bool)");
-	return SolverInterface::newBool(std::move(_name));
+	if (!m_constants.count(_name))
+	{
+		m_constants.insert(_name);
+		write("(declare-const |" + _name + "| Bool)");
+	}
 }
 
 void SMTLib2Interface::addAssertion(Expression const& _expr)
@@ -112,7 +124,7 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con
 		result = CheckResult::ERROR;
 
 	vector<string> values;
-	if (result != CheckResult::UNSATISFIABLE && result != CheckResult::ERROR)
+	if (result == CheckResult::SATISFIABLE && result != CheckResult::ERROR)
 		values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend());
 	return make_pair(result, values);
 }
@@ -146,7 +158,7 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _
 		{
 			auto const& e = _expressionsToEvaluate.at(i);
 			solAssert(e.sort == Sort::Int || e.sort == Sort::Bool, "Invalid sort for expression to evaluate.");
-			command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort == Sort::Int ? "Int" : "Bool") + "\n";
+			command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort == Sort::Int ? "Int" : "Bool") + ")\n";
 			command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
 		}
 		command += "(check-sat)\n";
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index 63188acd..eb876a7f 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -30,6 +30,7 @@
 #include <string>
 #include <vector>
 #include <cstdio>
+#include <set>
 
 namespace dev
 {
@@ -48,9 +49,9 @@ public:
 	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 declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+	void declareInteger(std::string _name) override;
+	void declareBool(std::string _name) override;
 
 	void addAssertion(Expression const& _expr) override;
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
@@ -68,6 +69,8 @@ private:
 
 	ReadCallback::Callback m_queryCallback;
 	std::vector<std::string> m_accumulatedOutput;
+	std::set<std::string> m_constants;
+	std::set<std::string> m_functions;
 };
 
 }
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp
new file mode 100644
index 00000000..8b9fe9ce
--- /dev/null
+++ b/libsolidity/formal/SMTPortfolio.cpp
@@ -0,0 +1,152 @@
+/*
+	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/SMTPortfolio.h>
+
+#ifdef HAVE_Z3
+#include <libsolidity/formal/Z3Interface.h>
+#endif
+#ifdef HAVE_CVC4
+#include <libsolidity/formal/CVC4Interface.h>
+#endif
+#if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
+#include <libsolidity/formal/SMTLib2Interface.h>
+#endif
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+using namespace dev::solidity::smt;
+
+SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback)
+{
+#ifdef HAVE_Z3
+	m_solvers.emplace_back(make_shared<smt::Z3Interface>());
+#endif
+#ifdef HAVE_CVC4
+	m_solvers.emplace_back(make_shared<smt::CVC4Interface>());
+#endif
+#if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
+	m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_readCallback)),
+#endif
+	(void)_readCallback;
+}
+
+void SMTPortfolio::reset()
+{
+	for (auto s : m_solvers)
+		s->reset();
+}
+
+void SMTPortfolio::push()
+{
+	for (auto s : m_solvers)
+		s->push();
+}
+
+void SMTPortfolio::pop()
+{
+	for (auto s : m_solvers)
+		s->pop();
+}
+
+void SMTPortfolio::declareFunction(string _name, Sort _domain, Sort _codomain)
+{
+	for (auto s : m_solvers)
+		s->declareFunction(_name, _domain, _codomain);
+}
+
+void SMTPortfolio::declareInteger(string _name)
+{
+	for (auto s : m_solvers)
+		s->declareInteger(_name);
+}
+
+void SMTPortfolio::declareBool(string _name)
+{
+	for (auto s : m_solvers)
+		s->declareBool(_name);
+}
+
+void SMTPortfolio::addAssertion(Expression const& _expr)
+{
+	for (auto s : m_solvers)
+		s->addAssertion(_expr);
+}
+
+/*
+ * Broadcasts the SMT query to all solvers and returns a single result.
+ * This comment explains how this result is decided.
+ *
+ * When a solver is queried, there are four possible answers:
+ *   SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, CONFLICTING, ERROR
+ * We say that a solver _answered_ the query if it returns either:
+ *   SAT or UNSAT
+ * A solver did not answer the query if it returns either:
+ *   UNKNOWN (it tried but couldn't solve it) or ERROR (crash, internal error, API error, etc).
+ *
+ * Ideally all solvers answer the query and agree on what the answer is
+ * (all say SAT or all say UNSAT).
+ *
+ * The actual logic as as follows:
+ * 1) If at least one solver answers the query, all the non-answer results are ignored.
+ *   Here SAT/UNSAT is preferred over UNKNOWN since it's an actual answer, and over ERROR
+ *   because one buggy solver/integration shouldn't break the portfolio.
+ *
+ * 2) If at least one solver answers SAT and at least one answers UNSAT, at least one of them is buggy
+ * and the result is CONFLICTING.
+ *   In the future if we have more than 2 solvers enabled we could go with the majority.
+ *
+ * 3) If NO solver answers the query:
+ *   If at least one solver returned UNKNOWN (where the rest returned ERROR), the result is UNKNOWN.
+ *   This is preferred over ERROR since the SMTChecker might decide to abstract the query
+ *   when it is told that this is a hard query to solve.
+ *
+ *   If all solvers return ERROR, the result is ERROR.
+*/
+pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const& _expressionsToEvaluate)
+{
+	CheckResult lastResult = CheckResult::ERROR;
+	vector<string> finalValues;
+	for (auto s : m_solvers)
+	{
+		CheckResult result;
+		vector<string> values;
+		tie(result, values) = s->check(_expressionsToEvaluate);
+		if (solverAnswered(result))
+		{
+			if (!solverAnswered(lastResult))
+			{
+				lastResult = result;
+				finalValues = std::move(values);
+			}
+			else if (lastResult != result)
+			{
+				lastResult = CheckResult::CONFLICTING;
+				break;
+			}
+		}
+		else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR)
+			lastResult = result;
+	}
+	return make_pair(lastResult, finalValues);
+}
+
+bool SMTPortfolio::solverAnswered(CheckResult result)
+{
+	return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE;
+}
diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h
new file mode 100644
index 00000000..96c7ff57
--- /dev/null
+++ b/libsolidity/formal/SMTPortfolio.h
@@ -0,0 +1,67 @@
+/*
+	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/ReadFile.h>
+
+#include <boost/noncopyable.hpp>
+
+#include <vector>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+/**
+ * The SMTPortfolio wraps all available solvers within a single interface,
+ * propagating the functionalities to all solvers.
+ * It also checks whether different solvers give conflicting answers
+ * to SMT queries.
+ */
+class SMTPortfolio: public SolverInterface, public boost::noncopyable
+{
+public:
+	SMTPortfolio(ReadCallback::Callback const& _readCallback);
+
+	void reset() override;
+
+	void push() override;
+	void pop() override;
+
+	void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+	void declareInteger(std::string _name) override;
+	void declareBool(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:
+	static bool solverAnswered(CheckResult result);
+
+	std::vector<std::shared_ptr<smt::SolverInterface>> m_solvers;
+};
+
+}
+}
+}
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
index f3213e03..36e15508 100644
--- a/libsolidity/formal/SSAVariable.cpp
+++ b/libsolidity/formal/SSAVariable.cpp
@@ -17,70 +17,17 @@
 
 #include <libsolidity/formal/SSAVariable.h>
 
-#include <libsolidity/formal/SymbolicBoolVariable.h>
-#include <libsolidity/formal/SymbolicIntVariable.h>
-
-#include <libsolidity/ast/AST.h>
-
 using namespace std;
-using namespace dev;
 using namespace dev::solidity;
 
-SSAVariable::SSAVariable(
-	Declaration const& _decl,
-	smt::SolverInterface& _interface
-)
+SSAVariable::SSAVariable()
 {
 	resetIndex();
-
-	if (isInteger(_decl.type()->category()))
-		m_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface);
-	else if (isBool(_decl.type()->category()))
-		m_symbolicVar = make_shared<SymbolicBoolVariable>(_decl, _interface);
-	else
-	{
-		solAssert(false, "");
-	}
-}
-
-bool SSAVariable::isSupportedType(Type::Category _category)
-{
-	return isInteger(_category) || isBool(_category);
-}
-
-bool SSAVariable::isInteger(Type::Category _category)
-{
-	return _category == Type::Category::Integer;
-}
-
-bool SSAVariable::isBool(Type::Category _category)
-{
-	return _category == Type::Category::Bool;
 }
 
 void SSAVariable::resetIndex()
 {
-	m_currentSequenceCounter = 0;
-	m_nextFreeSequenceCounter.reset (new int);
-	*m_nextFreeSequenceCounter = 1;
-}
-
-int SSAVariable::index() const
-{
-	return m_currentSequenceCounter;
-}
-
-int SSAVariable::next() const
-{
-	return *m_nextFreeSequenceCounter;
-}
-
-void SSAVariable::setZeroValue()
-{
-	m_symbolicVar->setZeroValue(index());
-}
-
-void SSAVariable::setUnknownValue()
-{
-	m_symbolicVar->setUnknownValue(index());
+	m_currentIndex = 0;
+	m_nextFreeIndex.reset (new unsigned);
+	*m_nextFreeIndex = 1;
 }
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
index bf5dae3b..46935472 100644
--- a/libsolidity/formal/SSAVariable.h
+++ b/libsolidity/formal/SSAVariable.h
@@ -17,8 +17,6 @@
 
 #pragma once
 
-#include <libsolidity/formal/SymbolicVariable.h>
-
 #include <memory>
 
 namespace dev
@@ -26,64 +24,29 @@ namespace dev
 namespace solidity
 {
 
-class Declaration;
-
 /**
  * This class represents the SSA representation of a program variable.
  */
 class SSAVariable
 {
 public:
-	/// @param _decl Used to determine the type and forwarded to the symbolic var.
-	/// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver.
-	SSAVariable(
-		Declaration const& _decl,
-		smt::SolverInterface& _interface
-	);
-
+	SSAVariable();
 	void resetIndex();
 
 	/// This function returns the current index of this SSA variable.
-	int index() const;
-	/// This function returns the next free index of this SSA variable.
-	int next() const;
-
-	int operator++()
-	{
-		return m_currentSequenceCounter = (*m_nextFreeSequenceCounter)++;
-	}
-
-	smt::Expression operator()() const
-	{
-		return valueAtSequence(index());
-	}
+	unsigned index() const { return m_currentIndex; }
+	unsigned& index() { return m_currentIndex; }
 
-	smt::Expression operator()(int _seq) const
+	unsigned operator++()
 	{
-		return valueAtSequence(_seq);
+		return m_currentIndex = (*m_nextFreeIndex)++;
 	}
 
-	/// These two functions forward the call to the symbolic var
-	/// which generates the constraints according to the type.
-	void setZeroValue();
-	void setUnknownValue();
-
-	/// So far Int and Bool are supported.
-	static bool isSupportedType(Type::Category _category);
-	static bool isInteger(Type::Category _category);
-	static bool isBool(Type::Category _category);
-
 private:
-	smt::Expression valueAtSequence(int _seq) const
-	{
-		return (*m_symbolicVar)(_seq);
-	}
-
-	std::shared_ptr<SymbolicVariable> m_symbolicVar = nullptr;
-	int m_currentSequenceCounter;
-	/// The next free sequence counter is a shared pointer because we want
+	unsigned m_currentIndex;
+	/// The next free index is a shared pointer because we want
 	/// the copy and the copied to share it.
-	std::shared_ptr<int> m_nextFreeSequenceCounter;
+	std::shared_ptr<unsigned> m_nextFreeIndex;
 };
 
 }
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 16796684..af1cc8e4 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -39,7 +39,7 @@ namespace smt
 
 enum class CheckResult
 {
-	SATISFIABLE, UNSATISFIABLE, UNKNOWN, ERROR
+	SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR
 };
 
 enum class Sort
@@ -171,8 +171,8 @@ public:
 		}
 	}
 
-	std::string const name;
-	std::vector<Expression> const arguments;
+	std::string name;
+	std::vector<Expression> arguments;
 	Sort sort;
 
 private:
@@ -199,8 +199,10 @@ public:
 	virtual void push() = 0;
 	virtual void pop() = 0;
 
-	virtual Expression newFunction(std::string _name, Sort _domain, Sort _codomain)
+	virtual void declareFunction(std::string _name, Sort _domain, Sort _codomain) = 0;
+	Expression newFunction(std::string _name, Sort _domain, Sort _codomain)
 	{
+		declareFunction(_name, _domain, _codomain);
 		solAssert(_domain == Sort::Int, "Function sort not supported.");
 		// Subclasses should do something here
 		switch (_codomain)
@@ -214,14 +216,18 @@ public:
 			break;
 		}
 	}
-	virtual Expression newInteger(std::string _name)
+	virtual void declareInteger(std::string _name) = 0;
+	Expression newInteger(std::string _name)
 	{
 		// Subclasses should do something here
+		declareInteger(_name);
 		return Expression(std::move(_name), {}, Sort::Int);
 	}
-	virtual Expression newBool(std::string _name)
+	virtual void declareBool(std::string _name) = 0;
+	Expression newBool(std::string _name)
 	{
 		// Subclasses should do something here
+		declareBool(_name);
 		return Expression(std::move(_name), {}, Sort::Bool);
 	}
 
@@ -231,8 +237,11 @@ public:
 	/// is available. Throws SMTSolverError on error.
 	virtual std::pair<CheckResult, std::vector<std::string>>
 	check(std::vector<Expression> const& _expressionsToEvaluate) = 0;
-};
 
+protected:
+	// SMT query timeout in milliseconds.
+	static int const queryTimeout = 10000;
+};
 
 }
 }
diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp
deleted file mode 100644
index 5cf22d7d..00000000
--- a/libsolidity/formal/SymbolicBoolVariable.cpp
+++ /dev/null
@@ -1,47 +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/SymbolicBoolVariable.h>
-
-#include <libsolidity/ast/AST.h>
-
-using namespace std;
-using namespace dev;
-using namespace dev::solidity;
-
-SymbolicBoolVariable::SymbolicBoolVariable(
-	Declaration const& _decl,
-	smt::SolverInterface&_interface
-):
-	SymbolicVariable(_decl, _interface)
-{
-	solAssert(m_declaration.type()->category() == Type::Category::Bool, "");
-}
-
-smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const
-{
-	return m_interface.newBool(uniqueSymbol(_seq));
-}
-
-void SymbolicBoolVariable::setZeroValue(int _seq)
-{
-	m_interface.addAssertion(valueAtSequence(_seq) == smt::Expression(false));
-}
-
-void SymbolicBoolVariable::setUnknownValue(int)
-{
-}
diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h
deleted file mode 100644
index 678f97d9..00000000
--- a/libsolidity/formal/SymbolicBoolVariable.h
+++ /dev/null
@@ -1,50 +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/formal/SymbolicVariable.h>
-
-#include <libsolidity/ast/Types.h>
-
-namespace dev
-{
-namespace solidity
-{
-
-/**
- * Specialization of SymbolicVariable for Bool
- */
-class SymbolicBoolVariable: public SymbolicVariable
-{
-public:
-	SymbolicBoolVariable(
-		Declaration const& _decl,
-		smt::SolverInterface& _interface
-	);
-
-	/// Sets the var to false.
-	void setZeroValue(int _seq);
-	/// Does nothing since the SMT solver already knows the valid values.
-	void setUnknownValue(int _seq);
-
-protected:
-	smt::Expression valueAtSequence(int _seq) const;
-};
-
-}
-}
diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
deleted file mode 100644
index 5e71fdcc..00000000
--- a/libsolidity/formal/SymbolicIntVariable.cpp
+++ /dev/null
@@ -1,60 +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/SymbolicIntVariable.h>
-
-#include <libsolidity/ast/AST.h>
-
-using namespace std;
-using namespace dev;
-using namespace dev::solidity;
-
-SymbolicIntVariable::SymbolicIntVariable(
-	Declaration const& _decl,
-	smt::SolverInterface& _interface
-):
-	SymbolicVariable(_decl, _interface)
-{
-	solAssert(m_declaration.type()->category() == Type::Category::Integer, "");
-}
-
-smt::Expression SymbolicIntVariable::valueAtSequence(int _seq) const
-{
-	return m_interface.newInteger(uniqueSymbol(_seq));
-}
-
-void SymbolicIntVariable::setZeroValue(int _seq)
-{
-	m_interface.addAssertion(valueAtSequence(_seq) == 0);
-}
-
-void SymbolicIntVariable::setUnknownValue(int _seq)
-{
-	auto const& intType = dynamic_cast<IntegerType const&>(*m_declaration.type());
-	m_interface.addAssertion(valueAtSequence(_seq) >= minValue(intType));
-	m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(intType));
-}
-
-smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t)
-{
-	return smt::Expression(_t.minValue());
-}
-
-smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t)
-{
-	return smt::Expression(_t.maxValue());
-}
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h
deleted file mode 100644
index d591e8db..00000000
--- a/libsolidity/formal/SymbolicIntVariable.h
+++ /dev/null
@@ -1,53 +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/formal/SymbolicVariable.h>
-
-#include <libsolidity/ast/Types.h>
-
-namespace dev
-{
-namespace solidity
-{
-
-/**
- * Specialization of SymbolicVariable for Integers
- */
-class SymbolicIntVariable: public SymbolicVariable
-{
-public:
-	SymbolicIntVariable(
-		Declaration const& _decl,
-		smt::SolverInterface& _interface
-	);
-
-	/// Sets the var to 0.
-	void setZeroValue(int _seq);
-	/// Sets the variable to the full valid value range.
-	void setUnknownValue(int _seq);
-
-	static smt::Expression minValue(IntegerType const& _t);
-	static smt::Expression maxValue(IntegerType const& _t);
-
-protected:
-	smt::Expression valueAtSequence(int _seq) const;
-};
-
-}
-}
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
new file mode 100644
index 00000000..3eb1c1ce
--- /dev/null
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -0,0 +1,127 @@
+/*
+	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/SymbolicTypes.h>
+
+#include <libsolidity/ast/Types.h>
+
+#include <memory>
+
+using namespace std;
+using namespace dev::solidity;
+
+bool dev::solidity::isSupportedType(Type::Category _category)
+{
+	return isNumber(_category) ||
+		isBool(_category) ||
+		isFunction(_category);
+}
+
+pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
+	Type const& _type,
+	std::string const& _uniqueName,
+	smt::SolverInterface& _solver
+)
+{
+	bool abstract = false;
+	shared_ptr<SymbolicVariable> var;
+	TypePointer type = _type.shared_from_this();
+	if (!isSupportedType(_type))
+	{
+		abstract = true;
+		var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
+	}
+	else if (isBool(_type.category()))
+		var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _solver);
+	else if (isFunction(_type.category()))
+		var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
+	else if (isInteger(_type.category()))
+		var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
+	else if (isFixedBytes(_type.category()))
+	{
+		auto fixedBytesType = dynamic_cast<FixedBytesType const*>(type.get());
+		solAssert(fixedBytesType, "");
+		var = make_shared<SymbolicFixedBytesVariable>(fixedBytesType->numBytes(), _uniqueName, _solver);
+	}
+	else if (isAddress(_type.category()))
+		var = make_shared<SymbolicAddressVariable>(_uniqueName, _solver);
+	else if (isRational(_type.category()))
+	{
+		auto rational = dynamic_cast<RationalNumberType const*>(&_type);
+		solAssert(rational, "");
+		if (rational->isFractional())
+			var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
+		else
+			var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
+	}
+	else
+		solAssert(false, "");
+	return make_pair(abstract, var);
+}
+
+bool dev::solidity::isSupportedType(Type const& _type)
+{
+	return isSupportedType(_type.category());
+}
+
+bool dev::solidity::isInteger(Type::Category _category)
+{
+	return _category == Type::Category::Integer;
+}
+
+bool dev::solidity::isRational(Type::Category _category)
+{
+	return _category == Type::Category::RationalNumber;
+}
+
+bool dev::solidity::isFixedBytes(Type::Category _category)
+{
+	return _category == Type::Category::FixedBytes;
+}
+
+bool dev::solidity::isAddress(Type::Category _category)
+{
+	return _category == Type::Category::Address;
+}
+
+bool dev::solidity::isNumber(Type::Category _category)
+{
+	return isInteger(_category) ||
+		isRational(_category) ||
+		isFixedBytes(_category) ||
+		isAddress(_category);
+}
+
+bool dev::solidity::isBool(Type::Category _category)
+{
+	return _category == Type::Category::Bool;
+}
+
+bool dev::solidity::isFunction(Type::Category _category)
+{
+	return _category == Type::Category::Function;
+}
+
+smt::Expression dev::solidity::minValue(IntegerType const& _type)
+{
+	return smt::Expression(_type.minValue());
+}
+
+smt::Expression dev::solidity::maxValue(IntegerType const& _type)
+{
+	return smt::Expression(_type.maxValue());
+}
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
new file mode 100644
index 00000000..dcdd9ea4
--- /dev/null
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -0,0 +1,53 @@
+/*
+	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/formal/SymbolicVariables.h>
+
+#include <libsolidity/ast/AST.h>
+#include <libsolidity/ast/Types.h>
+
+namespace dev
+{
+namespace solidity
+{
+
+/// So far int, bool and address are supported.
+/// Returns true if type is supported.
+bool isSupportedType(Type::Category _category);
+bool isSupportedType(Type const& _type);
+
+bool isInteger(Type::Category _category);
+bool isRational(Type::Category _category);
+bool isFixedBytes(Type::Category _category);
+bool isAddress(Type::Category _category);
+bool isNumber(Type::Category _category);
+bool isBool(Type::Category _category);
+bool isFunction(Type::Category _category);
+
+/// Returns a new symbolic variable, according to _type.
+/// Also returns whether the type is abstract or not,
+/// which is true for unsupported types.
+std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver);
+
+smt::Expression minValue(IntegerType const& _type);
+smt::Expression maxValue(IntegerType const& _type);
+
+}
+}
diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp
deleted file mode 100644
index caefa3a3..00000000
--- a/libsolidity/formal/SymbolicVariable.cpp
+++ /dev/null
@@ -1,40 +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/SymbolicVariable.h>
-
-#include <libsolidity/ast/AST.h>
-
-using namespace std;
-using namespace dev;
-using namespace dev::solidity;
-
-SymbolicVariable::SymbolicVariable(
-	Declaration const& _decl,
-	smt::SolverInterface& _interface
-):
-	m_declaration(_decl),
-	m_interface(_interface)
-{
-}
-
-string SymbolicVariable::uniqueSymbol(int _seq) const
-{
-	return m_declaration.name() + "_" + to_string(m_declaration.id()) + "_" + to_string(_seq);
-}
-
-
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h
deleted file mode 100644
index e29ded26..00000000
--- a/libsolidity/formal/SymbolicVariable.h
+++ /dev/null
@@ -1,66 +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/formal/SolverInterface.h>
-
-#include <libsolidity/ast/AST.h>
-
-#include <memory>
-
-namespace dev
-{
-namespace solidity
-{
-
-class Declaration;
-
-/**
- * This class represents the symbolic version of a program variable.
- */
-class SymbolicVariable
-{
-public:
-	SymbolicVariable(
-		Declaration const& _decl,
-		smt::SolverInterface& _interface
-	);
-	virtual ~SymbolicVariable() = default;
-
-	smt::Expression operator()(int _seq) const
-	{
-		return valueAtSequence(_seq);
-	}
-
-	std::string uniqueSymbol(int _seq) const;
-
-	/// Sets the var to the default value of its type.
-	virtual void setZeroValue(int _seq) = 0;
-	/// The unknown value is the full range of valid values,
-	/// and that's sub-type dependent.
-	virtual void setUnknownValue(int _seq) = 0;
-
-protected:
-	virtual smt::Expression valueAtSequence(int _seq) const = 0;
-
-	Declaration const& m_declaration;
-	smt::SolverInterface& m_interface;
-};
-
-}
-}
diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
new file mode 100644
index 00000000..85818ba0
--- /dev/null
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -0,0 +1,112 @@
+/*
+	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/SymbolicVariables.h>
+
+#include <libsolidity/formal/SymbolicTypes.h>
+
+#include <libsolidity/ast/AST.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+SymbolicVariable::SymbolicVariable(
+	TypePointer _type,
+	string const& _uniqueName,
+	smt::SolverInterface& _interface
+):
+	m_type(move(_type)),
+	m_uniqueName(_uniqueName),
+	m_interface(_interface),
+	m_ssa(make_shared<SSAVariable>())
+{
+}
+
+string SymbolicVariable::uniqueSymbol(unsigned _index) const
+{
+	return m_uniqueName + "_" + to_string(_index);
+}
+
+SymbolicBoolVariable::SymbolicBoolVariable(
+	TypePointer _type,
+	string const& _uniqueName,
+	smt::SolverInterface&_interface
+):
+	SymbolicVariable(move(_type), _uniqueName, _interface)
+{
+	solAssert(m_type->category() == Type::Category::Bool, "");
+}
+
+smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
+{
+	return m_interface.newBool(uniqueSymbol(_index));
+}
+
+void SymbolicBoolVariable::setZeroValue()
+{
+	m_interface.addAssertion(currentValue() == smt::Expression(false));
+}
+
+void SymbolicBoolVariable::setUnknownValue()
+{
+}
+
+SymbolicIntVariable::SymbolicIntVariable(
+	TypePointer _type,
+	string const& _uniqueName,
+	smt::SolverInterface& _interface
+):
+	SymbolicVariable(move(_type), _uniqueName, _interface)
+{
+	solAssert(isNumber(m_type->category()), "");
+}
+
+smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
+{
+	return m_interface.newInteger(uniqueSymbol(_index));
+}
+
+void SymbolicIntVariable::setZeroValue()
+{
+	m_interface.addAssertion(currentValue() == 0);
+}
+
+void SymbolicIntVariable::setUnknownValue()
+{
+	auto intType = dynamic_cast<IntegerType const*>(m_type.get());
+	solAssert(intType, "");
+	m_interface.addAssertion(currentValue() >= minValue(*intType));
+	m_interface.addAssertion(currentValue() <= maxValue(*intType));
+}
+
+SymbolicAddressVariable::SymbolicAddressVariable(
+	string const& _uniqueName,
+	smt::SolverInterface& _interface
+):
+	SymbolicIntVariable(make_shared<IntegerType>(160), _uniqueName, _interface)
+{
+}
+
+SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
+	unsigned _numBytes,
+	string const& _uniqueName,
+	smt::SolverInterface& _interface
+):
+	SymbolicIntVariable(make_shared<IntegerType>(_numBytes * 8), _uniqueName, _interface)
+{
+}
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
new file mode 100644
index 00000000..4fd9b245
--- /dev/null
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -0,0 +1,149 @@
+/*
+	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/SSAVariable.h>
+
+#include <libsolidity/formal/SolverInterface.h>
+
+#include <libsolidity/ast/Types.h>
+
+#include <memory>
+
+namespace dev
+{
+namespace solidity
+{
+
+class Type;
+
+/**
+ * This abstract class represents the symbolic version of a program variable.
+ */
+class SymbolicVariable
+{
+public:
+	SymbolicVariable(
+		TypePointer _type,
+		std::string const& _uniqueName,
+		smt::SolverInterface& _interface
+	);
+
+	virtual ~SymbolicVariable() = default;
+
+	smt::Expression currentValue() const
+	{
+		return valueAtIndex(m_ssa->index());
+	}
+
+	virtual smt::Expression valueAtIndex(int _index) const = 0;
+
+	smt::Expression increaseIndex()
+	{
+		++(*m_ssa);
+		return currentValue();
+	}
+
+	unsigned index() const { return m_ssa->index(); }
+	unsigned& index() { return m_ssa->index(); }
+
+	/// Sets the var to the default value of its type.
+	/// Inherited types must implement.
+	virtual void setZeroValue() = 0;
+	/// The unknown value is the full range of valid values.
+	/// It is sub-type dependent, but not mandatory.
+	virtual void setUnknownValue() {}
+
+protected:
+	std::string uniqueSymbol(unsigned _index) const;
+
+	TypePointer m_type = nullptr;
+	std::string m_uniqueName;
+	smt::SolverInterface& m_interface;
+	std::shared_ptr<SSAVariable> m_ssa = nullptr;
+};
+
+/**
+ * Specialization of SymbolicVariable for Bool
+ */
+class SymbolicBoolVariable: public SymbolicVariable
+{
+public:
+	SymbolicBoolVariable(
+		TypePointer _type,
+		std::string const& _uniqueName,
+		smt::SolverInterface& _interface
+	);
+
+	/// Sets the var to false.
+	void setZeroValue();
+	/// Does nothing since the SMT solver already knows the valid values for Bool.
+	void setUnknownValue();
+
+protected:
+	smt::Expression valueAtIndex(int _index) const;
+};
+
+/**
+ * Specialization of SymbolicVariable for Integers
+ */
+class SymbolicIntVariable: public SymbolicVariable
+{
+public:
+	SymbolicIntVariable(
+		TypePointer _type,
+		std::string const& _uniqueName,
+		smt::SolverInterface& _interface
+	);
+
+	/// Sets the var to 0.
+	void setZeroValue();
+	/// Sets the variable to the full valid value range.
+	void setUnknownValue();
+
+protected:
+	smt::Expression valueAtIndex(int _index) const;
+};
+
+/**
+ * Specialization of SymbolicVariable for Address
+ */
+class SymbolicAddressVariable: public SymbolicIntVariable
+{
+public:
+	SymbolicAddressVariable(
+		std::string const& _uniqueName,
+		smt::SolverInterface& _interface
+	);
+};
+
+/**
+ * Specialization of SymbolicVariable for FixedBytes
+ */
+class SymbolicFixedBytesVariable: public SymbolicIntVariable
+{
+public:
+	SymbolicFixedBytesVariable(
+		unsigned _numBytes,
+		std::string const& _uniqueName,
+		smt::SolverInterface& _interface
+	);
+};
+
+}
+}
diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp
index c2dea844..9282a560 100644
--- a/libsolidity/formal/VariableUsage.cpp
+++ b/libsolidity/formal/VariableUsage.cpp
@@ -50,12 +50,12 @@ VariableUsage::VariableUsage(ASTNode const& _node)
 	_node.accept(reducer);
 }
 
-vector<Declaration const*> VariableUsage::touchedVariables(ASTNode const& _node) const
+vector<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node) const
 {
 	if (!m_children.count(&_node) && !m_touchedVariable.count(&_node))
 		return {};
 
-	set<Declaration const*> touched;
+	set<VariableDeclaration const*> touched;
 	vector<ASTNode const*> toVisit;
 	toVisit.push_back(&_node);
 
diff --git a/libsolidity/formal/VariableUsage.h b/libsolidity/formal/VariableUsage.h
index 62561cce..dda13de2 100644
--- a/libsolidity/formal/VariableUsage.h
+++ b/libsolidity/formal/VariableUsage.h
@@ -27,7 +27,7 @@ namespace solidity
 {
 
 class ASTNode;
-class Declaration;
+class VariableDeclaration;
 
 /**
  * This class collects information about which local variables of value type
@@ -38,11 +38,11 @@ class VariableUsage
 public:
 	explicit VariableUsage(ASTNode const& _node);
 
-	std::vector<Declaration const*> touchedVariables(ASTNode const& _node) const;
+	std::vector<VariableDeclaration const*> touchedVariables(ASTNode const& _node) const;
 
 private:
 	// Variable touched by a specific AST node.
-	std::map<ASTNode const*, Declaration const*> m_touchedVariable;
+	std::map<ASTNode const*, VariableDeclaration const*> m_touchedVariable;
 	std::map<ASTNode const*, std::vector<ASTNode const*>> m_children;
 };
 
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 41943c92..9a0ccf48 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -28,7 +28,10 @@ using namespace dev::solidity::smt;
 Z3Interface::Z3Interface():
 	m_solver(m_context)
 {
+	// This needs to be set globally.
 	z3::set_param("rewriter.pull_cheap_ite", true);
+	// This needs to be set in the context.
+	m_context.set("timeout", queryTimeout);
 }
 
 void Z3Interface::reset()
@@ -48,22 +51,22 @@ void Z3Interface::pop()
 	m_solver.pop();
 }
 
-Expression Z3Interface::newFunction(string _name, Sort _domain, Sort _codomain)
+void Z3Interface::declareFunction(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);
+	if (!m_functions.count(_name))
+		m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
 }
 
-Expression Z3Interface::newInteger(string _name)
+void Z3Interface::declareInteger(string _name)
 {
-	m_constants.insert({_name, m_context.int_const(_name.c_str())});
-	return SolverInterface::newInteger(move(_name));
+	if (!m_constants.count(_name))
+		m_constants.insert({_name, m_context.int_const(_name.c_str())});
 }
 
-Expression Z3Interface::newBool(string _name)
+void Z3Interface::declareBool(string _name)
 {
-	m_constants.insert({_name, m_context.bool_const(_name.c_str())});
-	return SolverInterface::newBool(std::move(_name));
+	if (!m_constants.count(_name))
+		m_constants.insert({_name, m_context.bool_const(_name.c_str())});
 }
 
 void Z3Interface::addAssertion(Expression const& _expr)
@@ -88,11 +91,9 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
 		case z3::check_result::unknown:
 			result = CheckResult::UNKNOWN;
 			break;
-		default:
-			solAssert(false, "");
 		}
 
-		if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty())
+		if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty())
 		{
 			z3::model m = m_solver.get_model();
 			for (Expression const& e: _expressionsToEvaluate)
diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h
index 354ded25..84880ff3 100644
--- a/libsolidity/formal/Z3Interface.h
+++ b/libsolidity/formal/Z3Interface.h
@@ -40,9 +40,9 @@ public:
 	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 declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+	void declareInteger(std::string _name) override;
+	void declareBool(std::string _name) override;
 
 	void addAssertion(Expression const& _expr) override;
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;