From 06dbcb3afea63a935afc492b926f6b434bb78fa4 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Fri, 27 Jul 2018 14:13:22 +0200
Subject: Only ask for a model if it's SAT

---
 libsolidity/formal/Z3Interface.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'libsolidity/formal/Z3Interface.cpp')

diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 41943c92..7e0788b3 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -92,7 +92,7 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
 			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)
-- 
cgit