Fix the leaking file descriptor when returning a z3 smt check result (#1574)

pull/1576/head
Iaroslav Zeigerman 3 years ago committed by GitHub
parent 916a47286c
commit 3d012818e9
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
  1. 15
      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 :return: The evaluated result which is either of sat, unsat or unknown
""" """
old_stdout = sys.stdout old_stdout = sys.stdout
sys.stdout = open(os.devnull, "w") with open(os.devnull, "w") as dev_null_fd:
try: sys.stdout = dev_null_fd
evaluate = self.raw.check(args) try:
except z3.z3types.Z3Exception as e: evaluate = self.raw.check(args)
# Some requests crash the solver except z3.z3types.Z3Exception as e:
evaluate = z3.unknown # Some requests crash the solver
log.info(f"Encountered Z3 exception when checking the constraints: {e}") evaluate = z3.unknown
log.info(f"Encountered Z3 exception when checking the constraints: {e}")
sys.stdout = old_stdout sys.stdout = old_stdout
return evaluate return evaluate

Loading…
Cancel
Save