From 3d012818e939028042bb0dbfb47fee33c9d8d469 Mon Sep 17 00:00:00 2001
From: Iaroslav Zeigerman <zeigerman.ia@gmail.com>
Date: Wed, 29 Dec 2021 17:31:54 -0800
Subject: [PATCH] Fix the leaking file descriptor when returning a z3 smt check
 result (#1574)

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

diff --git a/mythril/laser/smt/solver/solver.py b/mythril/laser/smt/solver/solver.py
index 70cd3c0e..1bf00a81 100644
--- a/mythril/laser/smt/solver/solver.py
+++ b/mythril/laser/smt/solver/solver.py
@@ -54,13 +54,14 @@ class BaseSolver(Generic[T]):
         :return: The evaluated result which is either of sat, unsat or unknown
         """
         old_stdout = sys.stdout
-        sys.stdout = open(os.devnull, "w")
-        try:
-            evaluate = self.raw.check(args)
-        except z3.z3types.Z3Exception as e:
-            # Some requests crash the solver
-            evaluate = z3.unknown
-            log.info(f"Encountered Z3 exception when checking the constraints: {e}")
+        with open(os.devnull, "w") as dev_null_fd:
+            sys.stdout = dev_null_fd
+            try:
+                evaluate = self.raw.check(args)
+            except z3.z3types.Z3Exception as e:
+                # Some requests crash the solver
+                evaluate = z3.unknown
+                log.info(f"Encountered Z3 exception when checking the constraints: {e}")
         sys.stdout = old_stdout
         return evaluate