From e1552435e80737f5d592f676126522ba314fe444 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Tue, 10 Jul 2018 17:42:27 +0200
Subject: [PATCH] Add timeout logging to solver

---
 mythril/analysis/solver.py | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 9e59f831..0f6703e6 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -1,6 +1,6 @@
-from z3 import Solver, simplify, sat
+from z3 import Solver, simplify, sat, unknown
 from mythril.exceptions import UnsatError
-
+import logging
 
 def get_model(constraints):
     s = Solver()
@@ -8,13 +8,12 @@ def get_model(constraints):
 
     for constraint in constraints:
         s.add(constraint)
-
-    if (s.check() == sat):
-
+    result = s.check()
+    if result == sat:
         return s.model()
-
-    else:
-        raise UnsatError
+    elif result == unknown:
+        logging.info("Timeout encountered while solving expression using z3")
+    raise UnsatError
 
 
 def pretty_print_model(model):