Merge pull request #917 from ConsenSys/bugfix/916

Redirect stdout to null when executing self.raw.check()

mythril/laser/smt/solver.py

@@ -1,4 +1,6 @@
 """This module contains an abstract SMT representation of an SMT solver."""
+import os
+import sys
 import z3
 from typing import Union, cast, TypeVar, Generic, List, Sequence
 
@@ -44,10 +46,14 @@ class BaseSolver(Generic[T]):
 
     def check(self) -> z3.CheckSatResult:
         """Returns z3 smt check result.
-
-        :return:
+        Also suppresses the stdout when running z3 library's check() to avoid unnecessary output
+        :return: The evaluated result which is either of sat, unsat or unknown
         """
-        return self.raw.check()
+        old_stdout = sys.stdout
+        sys.stdout = open(os.devnull, "w")
+        evaluate = self.raw.check()
+        sys.stdout = old_stdout
+        return evaluate
 
     def model(self) -> Model:
         """Returns z3 model for a solution.