refactor solver and independence solver to use laser.smt.model

pull/902/head
Joran Honig 6 years ago
parent f380f87ae5
commit 3ce434329f
  1. 3
      mythril/laser/smt/independence_solver.py
  2. 4
      mythril/laser/smt/solver.py

@ -1,5 +1,6 @@
import z3 import z3
from mythril.laser.smt import Model
def get_expr_variables(expression: z3.ExprRef): def get_expr_variables(expression: z3.ExprRef):
""" """
@ -124,7 +125,7 @@ class IndependenceSolver:
:return: :return:
""" """
return self.models return Model(self.models)
def reset(self) -> None: def reset(self) -> None:
"""Reset this solver.""" """Reset this solver."""

@ -2,7 +2,7 @@
import z3 import z3
from mythril.laser.smt.expression import Expression from mythril.laser.smt.expression import Expression
from mythril.laser.smt.model import Model
class Solver: class Solver:
"""An SMT solver object.""" """An SMT solver object."""
@ -55,7 +55,7 @@ class Solver:
:return: :return:
""" """
return self.raw.model() return Model([self.raw.model()])
def reset(self) -> None: def reset(self) -> None:
"""Reset this solver.""" """Reset this solver."""

Loading…
Cancel
Save