Merge pull request #3099 from ethereum/develop

Merge develop into release for 0.4.18.

1 files changed, 29 insertions, 28 deletions

diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 522928f0..ab28baa3 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -72,36 +72,38 @@ void Z3Interface::addAssertion(Expression const& _expr)
 
 pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate)
 {
-//	cout << "---------------------------------" << endl;
-//	cout << m_solver << endl;
 	CheckResult result;
-	switch (m_solver.check())
+	vector<string> values;
+	try
 	{
-	case z3::check_result::sat:
-		result = CheckResult::SATISFIABLE;
-		cout << "sat" << endl;
-		break;
-	case z3::check_result::unsat:
-		result = CheckResult::UNSATISFIABLE;
-		cout << "unsat" << endl;
-		break;
-	case z3::check_result::unknown:
-		result = CheckResult::UNKNOWN;
-		cout << "unknown" << endl;
-		break;
-	default:
-		solAssert(false, "");
+		switch (m_solver.check())
+		{
+		case z3::check_result::sat:
+			result = CheckResult::SATISFIABLE;
+			break;
+		case z3::check_result::unsat:
+			result = CheckResult::UNSATISFIABLE;
+			break;
+		case z3::check_result::unknown:
+			result = CheckResult::UNKNOWN;
+			break;
+		default:
+			solAssert(false, "");
+		}
+
+		if (result != CheckResult::UNSATISFIABLE)
+		{
+			z3::model m = m_solver.get_model();
+			for (Expression const& e: _expressionsToEvaluate)
+				values.push_back(toString(m.eval(toZ3Expr(e))));
+		}
 	}
-//	cout << "---------------------------------" << endl;
-
-
-	vector<string> values;
-	if (result != CheckResult::UNSATISFIABLE)
+	catch (z3::exception const& _e)
 	{
-		z3::model m = m_solver.get_model();
-		for (Expression const& e: _expressionsToEvaluate)
-			values.push_back(toString(m.eval(toZ3Expr(e))));
+		result = CheckResult::ERROR;
+		values.clear();
 	}
+
 	return make_pair(result, values);
 }
 
@@ -125,8 +127,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 		{">=", 2},
 		{"+", 2},
 		{"-", 2},
-		{"*", 2},
-		{">=", 2}
+		{"*", 2}
 	};
 	string const& n = _expr.name;
 	if (m_functions.count(n))
@@ -142,7 +143,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 		return m_context.int_val(n.c_str());
 	}
 
-	assert(arity.count(n) && arity.at(n) == arguments.size());
+	solAssert(arity.count(n) && arity.at(n) == arguments.size(), "");
 	if (n == "ite")
 		return z3::ite(arguments[0], arguments[1], arguments[2]);
 	else if (n == "not")