Catch exception in Z3.

Note: This exception might not be the result of resource limitation,
it might also hint towards usage error.

1 files changed, 27 insertions, 18 deletions

diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 9eb79d29..ab28baa3 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -73,28 +73,37 @@ void Z3Interface::addAssertion(Expression const& _expr)
 pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate)
 {
 	CheckResult result;
-	switch (m_solver.check())
+	vector<string> values;
+	try
 	{
-	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, "");
+		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))));
+		}
 	}
-
-	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);
 }