Review changes.

6 files changed, 27 insertions, 26 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 092ecdb2..fd78e578 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -438,7 +438,7 @@ void SMTChecker::checkCondition(
 
 	switch (result)
 	{
-	case smt::CheckResult::SAT:
+	case smt::CheckResult::SATISFIABLE:
 	{
 		std::ostringstream message;
 		message << _description << " happens here";
@@ -464,7 +464,7 @@ void SMTChecker::checkCondition(
 		m_errorReporter.warning(_location, message.str());
 		break;
 	}
-	case smt::CheckResult::UNSAT:
+	case smt::CheckResult::UNSATISFIABLE:
 		break;
 	case smt::CheckResult::UNKNOWN:
 		m_errorReporter.warning(_location, _description + " might happen here.");
@@ -484,10 +484,10 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo
 	{
 		solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
 		solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, "");
-		solAssert(m_z3Variables.count(&_varDecl) == 0, "");
+		solAssert(m_Variables.count(&_varDecl) == 0, "");
 		m_currentSequenceCounter[&_varDecl] = 0;
 		m_nextFreeSequenceCounter[&_varDecl] = 1;
-		m_z3Variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
+		m_Variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
 		setValue(_varDecl, _setToZero);
 	}
 	else
@@ -556,7 +556,7 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t)
 
 smt::Expression SMTChecker::expr(Expression const& _e)
 {
-	if (!m_z3Expressions.count(&_e))
+	if (!m_Expressions.count(&_e))
 	{
 		solAssert(_e.annotation().type, "");
 		switch (_e.annotation().type->category())
@@ -565,24 +565,24 @@ smt::Expression SMTChecker::expr(Expression const& _e)
 		{
 			if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
 				solAssert(!rational->isFractional(), "");
-			m_z3Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
+			m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
 			break;
 		}
 		case Type::Category::Integer:
-			m_z3Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
+			m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
 			break;
 		case Type::Category::Bool:
-			m_z3Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
+			m_Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
 			break;
 		default:
 			solAssert(false, "Type not implemented.");
 		}
 	}
-	return m_z3Expressions.at(&_e);
+	return m_Expressions.at(&_e);
 }
 
 smt::Expression SMTChecker::var(Declaration const& _decl)
 {
-	solAssert(m_z3Variables.count(&_decl), "");
-	return m_z3Variables.at(&_decl);
+	solAssert(m_Variables.count(&_decl), "");
+	return m_Variables.at(&_decl);
 }
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index d4935116..d23fd201 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -71,8 +71,8 @@ private:
 
 	void createVariable(VariableDeclaration const& _varDecl, bool _setToZero);
 
-	std::string uniqueSymbol(Declaration const& _decl);
-	std::string uniqueSymbol(Expression const& _expr);
+	static std::string uniqueSymbol(Declaration const& _decl);
+	static std::string uniqueSymbol(Expression const& _expr);
 
 	/// @returns true if _delc is a variable that is known at the current point, i.e.
 	/// has a valid sequence number
@@ -90,8 +90,8 @@ private:
 	/// Sets the value of the declaration either to zero or to its intrinsic range.
 	void setValue(Declaration const& _decl, bool _setToZero);
 
-	smt::Expression minValue(IntegerType const& _t);
-	smt::Expression maxValue(IntegerType const& _t);
+	static smt::Expression minValue(IntegerType const& _t);
+	static smt::Expression maxValue(IntegerType const& _t);
 
 	/// Returns the expression corresponding to the AST node. Creates a new expression
 	/// if it does not exist yet.
@@ -103,8 +103,8 @@ private:
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::map<Declaration const*, int> m_currentSequenceCounter;
 	std::map<Declaration const*, int> m_nextFreeSequenceCounter;
-	std::map<Expression const*, smt::Expression> m_z3Expressions;
-	std::map<Declaration const*, smt::Expression> m_z3Variables;
+	std::map<Expression const*, smt::Expression> m_Expressions;
+	std::map<Declaration const*, smt::Expression> m_Variables;
 	ErrorReporter& m_errorReporter;
 
 	FunctionDefinition const* m_currentFunction = nullptr;
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index e7a9ef8c..cbd766fb 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -103,16 +103,16 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con
 	CheckResult result;
 	// TODO proper parsing
 	if (boost::starts_with(response, "sat\n"))
-		result = CheckResult::SAT;
+		result = CheckResult::SATISFIABLE;
 	else if (boost::starts_with(response, "unsat\n"))
-		result = CheckResult::UNSAT;
+		result = CheckResult::UNSATISFIABLE;
 	else if (boost::starts_with(response, "unknown\n"))
 		result = CheckResult::UNKNOWN;
 	else
 		result = CheckResult::ERROR;
 
 	vector<string> values;
-	if (result != CheckResult::UNSAT && result != CheckResult::ERROR)
+	if (result != CheckResult::UNSATISFIABLE && result != CheckResult::ERROR)
 		values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend());
 	return make_pair(result, values);
 }
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 8423c4a7..32d92a2a 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -39,7 +39,7 @@ namespace smt
 
 enum class CheckResult
 {
-	SAT, UNSAT, UNKNOWN, ERROR
+	SATISFIABLE, UNSATISFIABLE, UNKNOWN, ERROR
 };
 
 enum class Sort
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index bb0d6f6f..522928f0 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -78,11 +78,11 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
 	switch (m_solver.check())
 	{
 	case z3::check_result::sat:
-		result = CheckResult::SAT;
+		result = CheckResult::SATISFIABLE;
 		cout << "sat" << endl;
 		break;
 	case z3::check_result::unsat:
-		result = CheckResult::UNSAT;
+		result = CheckResult::UNSATISFIABLE;
 		cout << "unsat" << endl;
 		break;
 	case z3::check_result::unknown:
@@ -96,7 +96,7 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
 
 
 	vector<string> values;
-	if (result != CheckResult::UNSAT)
+	if (result != CheckResult::UNSATISFIABLE)
 	{
 		z3::model m = m_solver.get_model();
 		for (Expression const& e: _expressionsToEvaluate)
diff --git a/scripts/install_deps.sh b/scripts/install_deps.sh
index 760e4b80..3a1abe10 100755
--- a/scripts/install_deps.sh
+++ b/scripts/install_deps.sh
@@ -212,7 +212,7 @@ case $(uname -s) in
                     git \
                     libboost-all-dev \
                     unzip \
-		    "$install_z3"
+                    "$install_z3"
 
 
                 ;;
@@ -317,7 +317,8 @@ case $(uname -s) in
                     build-essential \
                     cmake \
                     git \
-                    libboost-all-dev "$install_z3"
+                    libboost-all-dev \
+                    "$install_z3"
                 if [ "$CI" = true ]; then
                     # Install 'eth', for use in the Solidity Tests-over-IPC.
                     # We will not use this 'eth', but its dependencies