From 3ce434329f938124cdb0164093f1ea2c7cbf8af8 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 28 Jan 2019 15:25:47 +0100 Subject: [PATCH] refactor solver and independence solver to use laser.smt.model --- mythril/laser/smt/independence_solver.py | 3 ++- mythril/laser/smt/solver.py | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py index 75512539..4b41ad54 100644 --- a/mythril/laser/smt/independence_solver.py +++ b/mythril/laser/smt/independence_solver.py @@ -1,5 +1,6 @@ import z3 +from mythril.laser.smt import Model def get_expr_variables(expression: z3.ExprRef): """ @@ -124,7 +125,7 @@ class IndependenceSolver: :return: """ - return self.models + return Model(self.models) def reset(self) -> None: """Reset this solver.""" diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver.py index 4b973470..d9eb5c13 100644 --- a/mythril/laser/smt/solver.py +++ b/mythril/laser/smt/solver.py @@ -2,7 +2,7 @@ import z3 from mythril.laser.smt.expression import Expression - +from mythril.laser.smt.model import Model class Solver: """An SMT solver object.""" @@ -55,7 +55,7 @@ class Solver: :return: """ - return self.raw.model() + return Model([self.raw.model()]) def reset(self) -> None: """Reset this solver."""