1 files changed, 34 insertions, 10 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 7e75df87..5b7807f7 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -32,10 +32,19 @@ using namespace dev;
 using namespace langutil;
 using namespace dev::solidity;
 
-SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
-	m_interface(make_shared<smt::SMTPortfolio>(_readFileCallback)),
+SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
+	m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)),
 	m_errorReporter(_errorReporter)
 {
+#if defined (HAVE_Z3) || defined (HAVE_CVC4)
+	if (!_smtlib2Responses.empty())
+		m_errorReporter.warning(
+			"SMT-LIB2 query responses were given in the auxiliary input, "
+			"but this Solidity binary uses an SMT solver (Z3/CVC4) directly."
+			"These responses will be ignored."
+			"Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses."
+		);
+#endif
 }
 
 void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
@@ -409,7 +418,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 	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();
+	setUnknownValue(*symbolicVar);
 	if (index > 0)
 		m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
@@ -417,10 +426,15 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 void SMTChecker::visitBlockHash(FunctionCall const& _funCall)
 {
 	string blockHash = "blockhash";
-	defineUninterpretedFunction(blockHash, {make_shared<smt::Sort>(smt::Kind::Int)}, smt::Kind::Int);
 	auto const& arguments = _funCall.arguments();
 	solAssert(arguments.size() == 1, "");
-	defineExpr(_funCall, m_uninterpretedFunctions.at(blockHash)({expr(*arguments[0])}));
+	smt::SortPointer paramSort = smtSort(*arguments.at(0)->annotation().type);
+	smt::SortPointer returnSort = smtSort(*_funCall.annotation().type);
+	defineUninterpretedFunction(
+		blockHash,
+		make_shared<smt::FunctionSort>(vector<smt::SortPointer>{paramSort}, returnSort)
+	);
+	defineExpr(_funCall, m_uninterpretedFunctions.at(blockHash)({expr(*arguments.at(0))}));
 	m_uninterpretedTerms.push_back(&_funCall);
 }
 
@@ -592,7 +606,7 @@ void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _e
 	{
 		auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
 		m_specialVariables.emplace(_name, result.second);
-		result.second->setUnknownValue();
+		setUnknownValue(*result.second);
 		if (result.first)
 			m_errorReporter.warning(
 				_expr.location(),
@@ -606,10 +620,10 @@ void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _e
 	defineExpr(_expr, m_specialVariables.at(_name)->currentValue());
 }
 
-void SMTChecker::defineUninterpretedFunction(string const& _name, vector<smt::SortPointer> const& _domain, smt::Sort const& _codomain)
+void SMTChecker::defineUninterpretedFunction(string const& _name, smt::SortPointer _sort)
 {
 	if (!m_uninterpretedFunctions.count(_name))
-		m_uninterpretedFunctions.emplace(_name, m_interface->newFunction(_name, _domain, _codomain));
+		m_uninterpretedFunctions.emplace(_name, m_interface->newVariable(_name, _sort));
 }
 
 void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
@@ -1066,13 +1080,23 @@ smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl)
 void SMTChecker::setZeroValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	m_variables.at(&_decl)->setZeroValue();
+	setZeroValue(*m_variables.at(&_decl));
+}
+
+void SMTChecker::setZeroValue(SymbolicVariable& _variable)
+{
+	smt::setSymbolicZeroValue(_variable, *m_interface);
 }
 
 void SMTChecker::setUnknownValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	m_variables.at(&_decl)->setUnknownValue();
+	setUnknownValue(*m_variables.at(&_decl));
+}
+
+void SMTChecker::setUnknownValue(SymbolicVariable& _variable)
+{
+	smt::setSymbolicUnknownValue(_variable, *m_interface);
 }
 
 smt::Expression SMTChecker::expr(Expression const& _e)