From a82940de2cf23decd428499794f6442f85e9e356 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 24 Jan 2019 00:09:17 +0100
Subject: [PATCH 01/32] add initial implementation of dependence map

---
 mythril/laser/smt/independence_solver.py | 75 ++++++++++++++++++++++++
 1 file changed, 75 insertions(+)
 create mode 100644 mythril/laser/smt/independence_solver.py

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
new file mode 100644
index 00000000..922c06f3
--- /dev/null
+++ b/mythril/laser/smt/independence_solver.py
@@ -0,0 +1,75 @@
+from z3 import BitVec, AstRef, ExprRef, BitVecVal, BitVecNumRef
+
+a = BitVec('a', 256)
+c = BitVec('c', 256)
+b = c * (a + 1)
+
+e = BitVec('d', 256)
+
+
+def get_expr_variables(expression: ExprRef):
+    """
+    Get's the variables that make up the current expression
+    :param expression:
+    :return:
+    """
+    result = []
+    if not expression.children() and not isinstance(expression, BitVecNumRef):
+        result.append(expression)
+    for child in expression.children():
+        c_children = get_expr_variables(child)
+        result.extend(c_children)
+    return result
+
+
+class DependenceBucket:
+    def __init__(self, variables=None, expressions=None):
+        self.variables = variables or []
+        self.expressions = expressions or []
+
+
+class DependenceMap:
+    def __init__(self):
+        self.buckets = []
+        self.variable_map = {}
+
+    def add_condition(self, condition):
+        variables = get_expr_variables(condition)
+        relevant_buckets = []
+        for variable in variables:
+            try:
+                bucket = self.variable_map[str(variable)]
+                relevant_buckets.append(bucket)
+            except KeyError:
+                continue
+
+        new_bucket = DependenceBucket(variables, [condition])
+        self.buckets.append(new_bucket)
+
+        if relevant_buckets:
+            # Merge buckets, and rewrite variable map accordingly
+            new_bucket = self.merge_buckets(relevant_buckets + [new_bucket])
+
+        for variable in variables:
+            self.variable_map[str(variable)] = new_bucket
+
+    def merge_buckets(self, bucket_list):
+        variables = []
+        expressions = []
+        for bucket in bucket_list:
+            self.buckets.remove(bucket)
+            variables += bucket.variables
+            expressions += bucket.expressions
+
+        new_bucket = DependenceBucket(variables, expressions)
+        self.buckets.append(new_bucket)
+
+        return new_bucket
+
+dmap = DependenceMap()
+
+dmap.add_condition(a)
+dmap.add_condition(b)
+dmap.add_condition(e)
+
+print("yeah")

From 39f7ecf56668632ea7f1049fc249ff73f26922b5 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 24 Jan 2019 00:22:42 +0100
Subject: [PATCH 02/32] add initial independence solver object to smt

---
 mythril/laser/smt/independence_solver.py | 105 ++++++++++++++++++++---
 1 file changed, 91 insertions(+), 14 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index 922c06f3..75512539 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -1,20 +1,14 @@
-from z3 import BitVec, AstRef, ExprRef, BitVecVal, BitVecNumRef
+import z3
 
-a = BitVec('a', 256)
-c = BitVec('c', 256)
-b = c * (a + 1)
 
-e = BitVec('d', 256)
-
-
-def get_expr_variables(expression: ExprRef):
+def get_expr_variables(expression: z3.ExprRef):
     """
     Get's the variables that make up the current expression
     :param expression:
     :return:
     """
     result = []
-    if not expression.children() and not isinstance(expression, BitVecNumRef):
+    if not expression.children() and not isinstance(expression, z3.BitVecNumRef):
         result.append(expression)
     for child in expression.children():
         c_children = get_expr_variables(child)
@@ -66,10 +60,93 @@ class DependenceMap:
 
         return new_bucket
 
-dmap = DependenceMap()
 
-dmap.add_condition(a)
-dmap.add_condition(b)
-dmap.add_condition(e)
+class IndependenceSolver:
+    """An SMT solver object."""
 
-print("yeah")
+    def __init__(self):
+        """"""
+        self.raw = z3.Solver()
+        self.constraints = []
+        self.models = []
+
+    def set_timeout(self, timeout: int) -> None:
+        """Sets the timeout that will be used by this solver, timeout is in
+        milliseconds.
+
+        :param timeout:
+        """
+        self.raw.set(timeout=timeout)
+
+    def add(self, constraints: list) -> None:
+        """Adds the constraints to this solver.
+
+        :param constraints:
+        :return:
+        """
+        constraints = [c.raw for c in constraints]
+        self.constraints.extend(constraints)
+
+    def append(self, constraints: list) -> None:
+        """Adds the constraints to this solver.
+
+        :param constraints:
+        :return:
+        """
+        constraints = [c.raw for c in constraints]
+        self.constraints.extend(constraints)
+
+    def check(self):
+        """Returns z3 smt check result.
+
+        :return:
+        """
+        dependence_map = DependenceMap()
+        for constraint in self.constraints:
+            dependence_map.add_condition(constraint)
+
+        self.models = []
+        for bucket in dependence_map.buckets:
+            self.raw.reset()
+            self.raw.append(*bucket.expressions)
+            check_result = self.raw.check()
+            if check_result == z3.unsat:
+                return z3.unsat
+            elif check_result == z3.unknown:
+                return z3.unknown
+            else:
+                self.models.append(self.raw.model())
+
+        return z3.sat
+
+    def model(self):
+        """Returns z3 model for a solution.
+
+        :return:
+        """
+        return self.models
+
+    def reset(self) -> None:
+        """Reset this solver."""
+        self.constraints = []
+
+    def pop(self, num) -> None:
+        """Pop num constraints from this solver.
+
+        :param num:
+        """
+        self.constraints.pop(num)
+
+
+from mythril.laser.smt import symbol_factory
+a = symbol_factory.BitVecSym('a', 256)
+c = symbol_factory.BitVecSym('c', 256)
+b = c == (a + symbol_factory.BitVecVal(1, 256))
+
+e = symbol_factory.BitVecSym('d', 256) == symbol_factory.BitVecVal(3, 256)
+
+solver = IndependenceSolver()
+solver.add([b, e])
+result = solver.check()
+
+print("hello")

From f380f87ae5abaa14ca3d5f6b0bd4f26897384f5b Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 15:24:22 +0100
Subject: [PATCH 03/32] add model implementation to laser.smt

---
 mythril/laser/smt/__init__.py |  1 +
 mythril/laser/smt/model.py    | 45 +++++++++++++++++++++++++++++++++++
 2 files changed, 46 insertions(+)
 create mode 100644 mythril/laser/smt/model.py

diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py
index 3b41f7d2..e585371b 100644
--- a/mythril/laser/smt/__init__.py
+++ b/mythril/laser/smt/__init__.py
@@ -18,6 +18,7 @@ from mythril.laser.smt.expression import Expression, simplify
 from mythril.laser.smt.bool import Bool, is_true, is_false, Or, Not
 from mythril.laser.smt.array import K, Array, BaseArray
 from mythril.laser.smt.solver import Solver, Optimize
+from mythril.laser.smt.model import Model
 
 import z3
 
diff --git a/mythril/laser/smt/model.py b/mythril/laser/smt/model.py
new file mode 100644
index 00000000..ff3c3756
--- /dev/null
+++ b/mythril/laser/smt/model.py
@@ -0,0 +1,45 @@
+import z3
+
+
+class Model:
+    """ The model class wraps a z3 model
+
+    This implementation allows for multiple internal models, this is required for the use of an independence solver
+    which has models for multiple queries which need an uniform output.
+    """
+    def __init__(self, models=None):
+        """
+        Initialize a model object
+        :param models: the internal z3 models that this model should use
+        """
+        self.raw = models or []
+
+    def decls(self):
+        """Get the declarations for this model"""
+        result = []
+        for internal_model in self.raw:
+            result.extend(internal_model.decls())
+
+    def __getitem__(self, item):
+        """ Get declaration from model
+         If item is an int, then the declaration at offset item is returned
+         If item is a declaration, then the interpretation is returned
+         """
+        for internal_model in self.raw:
+            try:
+                return internal_model[item]
+            except KeyError:
+                continue
+
+    def eval(self, expression: z3.ExprRef, model_completion: bool = False):
+        """ Evaluate the expression using this model
+
+        :param expression: The expression to evaluate
+        :param model_completion: Use the default value if the model has no interpretation of the given expression
+        :return: The evaluated expression
+        """
+        for internal_model in self.raw:
+            is_last_model = self.raw.index(internal_model) == len(self.raw) - 1
+            is_relevant_model = expression.decl() in list(internal_model.decls())
+            if is_relevant_model or is_last_model:
+                return internal_model.eval(expression, model_completion)

From 3ce434329f938124cdb0164093f1ea2c7cbf8af8 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 15:25:47 +0100
Subject: [PATCH 04/32] 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."""

From 5ddc5ec8bf63e08cd84f1ae8bffe65551b862914 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 15:26:14 +0100
Subject: [PATCH 05/32] refactor independence solver to make get_expr_variables
 private

---
 mythril/laser/smt/independence_solver.py | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index 4b41ad54..b236c99b 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -2,7 +2,8 @@ import z3
 
 from mythril.laser.smt import Model
 
-def get_expr_variables(expression: z3.ExprRef):
+
+def _get_expr_variables(expression: z3.ExprRef):
     """
     Get's the variables that make up the current expression
     :param expression:
@@ -12,7 +13,7 @@ def get_expr_variables(expression: z3.ExprRef):
     if not expression.children() and not isinstance(expression, z3.BitVecNumRef):
         result.append(expression)
     for child in expression.children():
-        c_children = get_expr_variables(child)
+        c_children = _get_expr_variables(child)
         result.extend(c_children)
     return result
 
@@ -29,7 +30,7 @@ class DependenceMap:
         self.variable_map = {}
 
     def add_condition(self, condition):
-        variables = get_expr_variables(condition)
+        variables = _get_expr_variables(condition)
         relevant_buckets = []
         for variable in variables:
             try:

From 99329328169ced61384a3eb73f477679973ef3ff Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 15:32:19 +0100
Subject: [PATCH 06/32] add documentation and typehints for independence solver

---
 mythril/laser/smt/independence_solver.py | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index b236c99b..4fab307e 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -1,7 +1,7 @@
 import z3
 
 from mythril.laser.smt import Model
-
+from typing import List
 
 def _get_expr_variables(expression: z3.ExprRef):
     """
@@ -19,17 +19,29 @@ def _get_expr_variables(expression: z3.ExprRef):
 
 
 class DependenceBucket:
-    def __init__(self, variables=None, expressions=None):
+    """ Bucket object to contain a set of conditions that are dependent on each other """
+    def __init__(self, variables=None, condition=None):
+        """
+        Initializes a DependenceBucket object
+        :param variables: Variables contained in the expressions
+        :param expressions: The expressions that are dependent on each other
+        """
         self.variables = variables or []
-        self.expressions = expressions or []
+        self.expressions = condition or []
 
 
 class DependenceMap:
+    """ DependenceMap object that maintains a set of dependence buckets, used to separate independent smt queries """
     def __init__(self):
+        """ Initializes a DependenceMap object """
         self.buckets = []
         self.variable_map = {}
 
-    def add_condition(self, condition):
+    def add_condition(self, condition: z3.BoolRef):
+        """
+        Add condition to the dependence map
+        :param condition: The condition that is to be added to the dependence map
+        """
         variables = _get_expr_variables(condition)
         relevant_buckets = []
         for variable in variables:
@@ -49,7 +61,8 @@ class DependenceMap:
         for variable in variables:
             self.variable_map[str(variable)] = new_bucket
 
-    def merge_buckets(self, bucket_list):
+    def merge_buckets(self, bucket_list: List[DependenceBucket]):
+        """ Merges the buckets in bucket list """
         variables = []
         expressions = []
         for bucket in bucket_list:

From f5e84fcb21ec0c29494cffb03b892d7019456767 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 15:32:38 +0100
Subject: [PATCH 07/32] apply style rules

---
 mythril/laser/smt/independence_solver.py | 10 +++++++---
 mythril/laser/smt/model.py               |  1 +
 mythril/laser/smt/solver.py              |  1 +
 3 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index 4fab307e..01552410 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -3,6 +3,7 @@ import z3
 from mythril.laser.smt import Model
 from typing import List
 
+
 def _get_expr_variables(expression: z3.ExprRef):
     """
     Get's the variables that make up the current expression
@@ -20,6 +21,7 @@ def _get_expr_variables(expression: z3.ExprRef):
 
 class DependenceBucket:
     """ Bucket object to contain a set of conditions that are dependent on each other """
+
     def __init__(self, variables=None, condition=None):
         """
         Initializes a DependenceBucket object
@@ -32,6 +34,7 @@ class DependenceBucket:
 
 class DependenceMap:
     """ DependenceMap object that maintains a set of dependence buckets, used to separate independent smt queries """
+
     def __init__(self):
         """ Initializes a DependenceMap object """
         self.buckets = []
@@ -154,11 +157,12 @@ class IndependenceSolver:
 
 
 from mythril.laser.smt import symbol_factory
-a = symbol_factory.BitVecSym('a', 256)
-c = symbol_factory.BitVecSym('c', 256)
+
+a = symbol_factory.BitVecSym("a", 256)
+c = symbol_factory.BitVecSym("c", 256)
 b = c == (a + symbol_factory.BitVecVal(1, 256))
 
-e = symbol_factory.BitVecSym('d', 256) == symbol_factory.BitVecVal(3, 256)
+e = symbol_factory.BitVecSym("d", 256) == symbol_factory.BitVecVal(3, 256)
 
 solver = IndependenceSolver()
 solver.add([b, e])
diff --git a/mythril/laser/smt/model.py b/mythril/laser/smt/model.py
index ff3c3756..1e758008 100644
--- a/mythril/laser/smt/model.py
+++ b/mythril/laser/smt/model.py
@@ -7,6 +7,7 @@ class Model:
     This implementation allows for multiple internal models, this is required for the use of an independence solver
     which has models for multiple queries which need an uniform output.
     """
+
     def __init__(self, models=None):
         """
         Initialize a model object
diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver.py
index d9eb5c13..3794c613 100644
--- a/mythril/laser/smt/solver.py
+++ b/mythril/laser/smt/solver.py
@@ -4,6 +4,7 @@ import z3
 from mythril.laser.smt.expression import Expression
 from mythril.laser.smt.model import Model
 
+
 class Solver:
     """An SMT solver object."""
 

From a0dd0614249698473edcb1074173964df8155a99 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 15:39:05 +0100
Subject: [PATCH 08/32] add _get_expr_variable tests for independence solver

---
 tests/laser/smt/__init__.py                |  0
 tests/laser/smt/independece_solver_test.py | 32 ++++++++++++++++++++++
 2 files changed, 32 insertions(+)
 create mode 100644 tests/laser/smt/__init__.py
 create mode 100644 tests/laser/smt/independece_solver_test.py

diff --git a/tests/laser/smt/__init__.py b/tests/laser/smt/__init__.py
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/laser/smt/independece_solver_test.py b/tests/laser/smt/independece_solver_test.py
new file mode 100644
index 00000000..0505a431
--- /dev/null
+++ b/tests/laser/smt/independece_solver_test.py
@@ -0,0 +1,32 @@
+from mythril.laser.smt.independence_solver import _get_expr_variables
+import z3
+
+
+def test_get_expr_variables():
+    # Arrange
+    x = z3.Bool('x')
+    y = z3.Int('y')
+    z = z3.Int('z')
+    b = z3.Int('b')
+    expression = z3.If(x, y, z + b)
+
+    # Act
+    variables = _get_expr_variables(expression)
+
+    # Assert
+    assert x in variables
+    assert y in variables
+    assert z in variables
+    assert b in variables
+
+
+def test_get_expr_variables_num():
+    # Arrange
+    b = z3.BitVec('b', 256)
+    expression = b + z3.BitVecVal(2, 256)
+
+    # Act
+    variables = _get_expr_variables(expression)
+
+    # Assert
+    assert [b] == variables

From 8014e546c0474ad0a5e666441eadaf6bc9692caf Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 15:41:21 +0100
Subject: [PATCH 09/32] add create bucket test

---
 tests/laser/smt/independece_solver_test.py | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/tests/laser/smt/independece_solver_test.py b/tests/laser/smt/independece_solver_test.py
index 0505a431..49efbf8b 100644
--- a/tests/laser/smt/independece_solver_test.py
+++ b/tests/laser/smt/independece_solver_test.py
@@ -1,4 +1,4 @@
-from mythril.laser.smt.independence_solver import _get_expr_variables
+from mythril.laser.smt.independence_solver import _get_expr_variables, DependenceBucket, DependenceMap
 import z3
 
 
@@ -30,3 +30,16 @@ def test_get_expr_variables_num():
 
     # Assert
     assert [b] == variables
+
+
+def test_create_bucket():
+    # Arrange
+    x = z3.Bool('x')
+
+    # Act
+    bucket = DependenceBucket([x], [x])
+
+    # Assert
+    assert [x] == bucket.variables
+    assert [x] == bucket.expressions
+

From 9fc48e377ca96d381de20536e5e240e269a94ec6 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 15:51:38 +0100
Subject: [PATCH 10/32] rename expressions to conditions as this is the correct
 term to use

---
 mythril/laser/smt/independence_solver.py | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index 01552410..59a1bfab 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -22,14 +22,14 @@ def _get_expr_variables(expression: z3.ExprRef):
 class DependenceBucket:
     """ Bucket object to contain a set of conditions that are dependent on each other """
 
-    def __init__(self, variables=None, condition=None):
+    def __init__(self, variables=None, conditions=None):
         """
         Initializes a DependenceBucket object
-        :param variables: Variables contained in the expressions
-        :param expressions: The expressions that are dependent on each other
+        :param variables: Variables contained in the conditions
+        :param conditions: The conditions that are dependent on each other
         """
         self.variables = variables or []
-        self.expressions = condition or []
+        self.conditions = conditions or []
 
 
 class DependenceMap:
@@ -67,13 +67,13 @@ class DependenceMap:
     def merge_buckets(self, bucket_list: List[DependenceBucket]):
         """ Merges the buckets in bucket list """
         variables = []
-        expressions = []
+        conditions = []
         for bucket in bucket_list:
             self.buckets.remove(bucket)
             variables += bucket.variables
-            expressions += bucket.expressions
+            conditions += bucket.conditions
 
-        new_bucket = DependenceBucket(variables, expressions)
+        new_bucket = DependenceBucket(variables, conditions)
         self.buckets.append(new_bucket)
 
         return new_bucket
@@ -126,7 +126,7 @@ class IndependenceSolver:
         self.models = []
         for bucket in dependence_map.buckets:
             self.raw.reset()
-            self.raw.append(*bucket.expressions)
+            self.raw.append(*bucket.conditions)
             check_result = self.raw.check()
             if check_result == z3.unsat:
                 return z3.unsat

From 5adb4cd2d0b58c08aab03bd05792f8a2f7215dce Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 15:51:45 +0100
Subject: [PATCH 11/32] add dependence map test

---
 tests/laser/smt/independece_solver_test.py | 53 ++++++++++++++++++----
 1 file changed, 44 insertions(+), 9 deletions(-)

diff --git a/tests/laser/smt/independece_solver_test.py b/tests/laser/smt/independece_solver_test.py
index 49efbf8b..3e6519d1 100644
--- a/tests/laser/smt/independece_solver_test.py
+++ b/tests/laser/smt/independece_solver_test.py
@@ -5,19 +5,19 @@ import z3
 def test_get_expr_variables():
     # Arrange
     x = z3.Bool('x')
-    y = z3.Int('y')
-    z = z3.Int('z')
-    b = z3.Int('b')
+    y = z3.BitVec('y', 256)
+    z = z3.BitVec('z', 256)
+    b = z3.BitVec('b', 256)
     expression = z3.If(x, y, z + b)
 
     # Act
-    variables = _get_expr_variables(expression)
+    variables = list(map(str, _get_expr_variables(expression)))
 
     # Assert
-    assert x in variables
-    assert y in variables
-    assert z in variables
-    assert b in variables
+    assert str(x) in variables
+    assert str(y) in variables
+    assert str(z) in variables
+    assert str(b) in variables
 
 
 def test_get_expr_variables_num():
@@ -41,5 +41,40 @@ def test_create_bucket():
 
     # Assert
     assert [x] == bucket.variables
-    assert [x] == bucket.expressions
+    assert [x] == bucket.conditions
+
+
+def test_dependence_map():
+    # Arrange
+    x = z3.BitVec('x', 256)
+    y = z3.BitVec('y', 256)
+    z = z3.BitVec('z', 256)
+    a = z3.BitVec('a', 256)
+    b = z3.BitVec('b', 256)
+
+    conditions = [
+        x > y,
+        y == z,
+        a == b
+    ]
+
+    dependence_map = DependenceMap()
+
+    # Act
+    for condition in conditions:
+        dependence_map.add_condition(condition)
+
+    # Assert
+    assert 2 == len(dependence_map.buckets)
+
+    assert x in dependence_map.buckets[0].variables
+    assert y in dependence_map.buckets[0].variables
+    assert z in dependence_map.buckets[0].variables
+
+    assert conditions[0] in dependence_map.buckets[0].conditions
+    assert conditions[1] in dependence_map.buckets[0].conditions
+
+    assert a in dependence_map.buckets[1].variables
+    assert b in dependence_map.buckets[1].variables
 
+    assert conditions[2] in dependence_map.buckets[1].conditions

From 19de3edd17d9ce3bfd05995ca8a38324330d510f Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 16:13:42 +0100
Subject: [PATCH 12/32] use set vs list and fix comments

---
 mythril/laser/smt/independence_solver.py | 48 ++++++------------------
 1 file changed, 12 insertions(+), 36 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index 59a1bfab..887c71d6 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -1,7 +1,7 @@
 import z3
 
 from mythril.laser.smt import Model
-from typing import List
+from typing import Set
 
 
 def _get_expr_variables(expression: z3.ExprRef):
@@ -45,12 +45,12 @@ class DependenceMap:
         Add condition to the dependence map
         :param condition: The condition that is to be added to the dependence map
         """
-        variables = _get_expr_variables(condition)
-        relevant_buckets = []
+        variables = set(_get_expr_variables(condition))
+        relevant_buckets = set()
         for variable in variables:
             try:
                 bucket = self.variable_map[str(variable)]
-                relevant_buckets.append(bucket)
+                relevant_buckets.add(bucket)
             except KeyError:
                 continue
 
@@ -59,12 +59,13 @@ class DependenceMap:
 
         if relevant_buckets:
             # Merge buckets, and rewrite variable map accordingly
-            new_bucket = self.merge_buckets(relevant_buckets + [new_bucket])
+            relevant_buckets.add(new_bucket)
+            new_bucket = self.merge_buckets(relevant_buckets)
 
         for variable in variables:
             self.variable_map[str(variable)] = new_bucket
 
-    def merge_buckets(self, bucket_list: List[DependenceBucket]):
+    def merge_buckets(self, bucket_list: Set[DependenceBucket]):
         """ Merges the buckets in bucket list """
         variables = []
         conditions = []
@@ -80,7 +81,7 @@ class DependenceMap:
 
 
 class IndependenceSolver:
-    """An SMT solver object."""
+    """An SMT solver object that uses independence optimization"""
 
     def __init__(self):
         """"""
@@ -99,8 +100,7 @@ class IndependenceSolver:
     def add(self, constraints: list) -> None:
         """Adds the constraints to this solver.
 
-        :param constraints:
-        :return:
+        :param constraints: constraints to add
         """
         constraints = [c.raw for c in constraints]
         self.constraints.extend(constraints)
@@ -108,17 +108,13 @@ class IndependenceSolver:
     def append(self, constraints: list) -> None:
         """Adds the constraints to this solver.
 
-        :param constraints:
-        :return:
+        :param constraints: constraints to add
         """
         constraints = [c.raw for c in constraints]
         self.constraints.extend(constraints)
 
     def check(self):
-        """Returns z3 smt check result.
-
-        :return:
-        """
+        """Returns z3 smt check result. """
         dependence_map = DependenceMap()
         for constraint in self.constraints:
             dependence_map.add_condition(constraint)
@@ -138,10 +134,7 @@ class IndependenceSolver:
         return z3.sat
 
     def model(self):
-        """Returns z3 model for a solution.
-
-        :return:
-        """
+        """Returns z3 model for a solution. """
         return Model(self.models)
 
     def reset(self) -> None:
@@ -150,22 +143,5 @@ class IndependenceSolver:
 
     def pop(self, num) -> None:
         """Pop num constraints from this solver.
-
-        :param num:
         """
         self.constraints.pop(num)
-
-
-from mythril.laser.smt import symbol_factory
-
-a = symbol_factory.BitVecSym("a", 256)
-c = symbol_factory.BitVecSym("c", 256)
-b = c == (a + symbol_factory.BitVecVal(1, 256))
-
-e = symbol_factory.BitVecSym("d", 256) == symbol_factory.BitVecVal(3, 256)
-
-solver = IndependenceSolver()
-solver.add([b, e])
-result = solver.check()
-
-print("hello")

From 4fe49aa2603309051f70bcc92e046f61d57995ca Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 16:14:19 +0100
Subject: [PATCH 13/32] add independence solver tests

---
 tests/laser/smt/independece_solver_test.py | 79 +++++++++++++++++++++-
 1 file changed, 78 insertions(+), 1 deletion(-)

diff --git a/tests/laser/smt/independece_solver_test.py b/tests/laser/smt/independece_solver_test.py
index 3e6519d1..a3a1aeef 100644
--- a/tests/laser/smt/independece_solver_test.py
+++ b/tests/laser/smt/independece_solver_test.py
@@ -1,4 +1,7 @@
-from mythril.laser.smt.independence_solver import _get_expr_variables, DependenceBucket, DependenceMap
+from mythril.laser.smt.independence_solver import _get_expr_variables, DependenceBucket, DependenceMap,\
+    IndependenceSolver
+from mythril.laser.smt import symbol_factory
+
 import z3
 
 
@@ -78,3 +81,77 @@ def test_dependence_map():
     assert b in dependence_map.buckets[1].variables
 
     assert conditions[2] in dependence_map.buckets[1].conditions
+
+
+def test_Independence_solver_unsat():
+    # Arrange
+    x = symbol_factory.BitVecSym('x', 256)
+    y = symbol_factory.BitVecSym('y', 256)
+    z = symbol_factory.BitVecSym('z', 256)
+    a = symbol_factory.BitVecSym('a', 256)
+    b = symbol_factory.BitVecSym('b', 256)
+
+    conditions = [
+        x > y,
+        y == z,
+        y != z,
+        a == b
+    ]
+
+    solver = IndependenceSolver()
+
+    # Act
+    solver.add(conditions)
+    result = solver.check()
+
+    # Assert
+    assert z3.unsat == result
+
+
+def test_independence_solver_unsat_in_second_bucket():
+    # Arrange
+    x = symbol_factory.BitVecSym('x', 256)
+    y = symbol_factory.BitVecSym('y', 256)
+    z = symbol_factory.BitVecSym('z', 256)
+    a = symbol_factory.BitVecSym('a', 256)
+    b = symbol_factory.BitVecSym('b', 256)
+
+    conditions = [
+        x > y,
+        y == z,
+        a == b,
+        a != b
+    ]
+
+    solver = IndependenceSolver()
+
+    # Act
+    solver.add(conditions)
+    result = solver.check()
+
+    # Assert
+    assert z3.unsat == result
+
+
+def test_independence_solver_sat():
+    # Arrange
+    x = symbol_factory.BitVecSym('x', 256)
+    y = symbol_factory.BitVecSym('y', 256)
+    z = symbol_factory.BitVecSym('z', 256)
+    a = symbol_factory.BitVecSym('a', 256)
+    b = symbol_factory.BitVecSym('b', 256)
+
+    conditions = [
+        x > y,
+        y == z,
+        a == b,
+    ]
+
+    solver = IndependenceSolver()
+
+    # Act
+    solver.add(conditions)
+    result = solver.check()
+
+    # Assert
+    assert z3.sat == result

From 05e74735e42e79c3a63954c90d47a018bb61d2cc Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 16:17:45 +0100
Subject: [PATCH 14/32] add edge case handling to model

---
 mythril/laser/smt/model.py | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/mythril/laser/smt/model.py b/mythril/laser/smt/model.py
index 1e758008..a6060d98 100644
--- a/mythril/laser/smt/model.py
+++ b/mythril/laser/smt/model.py
@@ -27,10 +27,17 @@ class Model:
          If item is a declaration, then the interpretation is returned
          """
         for internal_model in self.raw:
+            is_last_model = self.raw.index(internal_model) == len(self.raw) - 1
+
             try:
-                return internal_model[item]
-            except KeyError:
+                result = internal_model[item]
+                if result is None:
+                    continue
+            except IndexError:
+                if is_last_model:
+                    raise
                 continue
+            return None
 
     def eval(self, expression: z3.ExprRef, model_completion: bool = False):
         """ Evaluate the expression using this model

From 79aad17fde626b8387a26384a48edfd8a0e05332 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 16:30:07 +0100
Subject: [PATCH 15/32] add some basic model tests and fix discovered bug

---
 mythril/laser/smt/model.py    |  7 +++--
 tests/laser/smt/model_test.py | 56 +++++++++++++++++++++++++++++++++++
 2 files changed, 60 insertions(+), 3 deletions(-)
 create mode 100644 tests/laser/smt/model_test.py

diff --git a/mythril/laser/smt/model.py b/mythril/laser/smt/model.py
index a6060d98..e0eb3830 100644
--- a/mythril/laser/smt/model.py
+++ b/mythril/laser/smt/model.py
@@ -20,6 +20,7 @@ class Model:
         result = []
         for internal_model in self.raw:
             result.extend(internal_model.decls())
+        return result
 
     def __getitem__(self, item):
         """ Get declaration from model
@@ -31,13 +32,13 @@ class Model:
 
             try:
                 result = internal_model[item]
-                if result is None:
-                    continue
+                if result is not None:
+                    return result
             except IndexError:
                 if is_last_model:
                     raise
                 continue
-            return None
+        return None
 
     def eval(self, expression: z3.ExprRef, model_completion: bool = False):
         """ Evaluate the expression using this model
diff --git a/tests/laser/smt/model_test.py b/tests/laser/smt/model_test.py
new file mode 100644
index 00000000..4b799afe
--- /dev/null
+++ b/tests/laser/smt/model_test.py
@@ -0,0 +1,56 @@
+from mythril.laser.smt import Solver, symbol_factory
+import z3
+
+
+def test_decls():
+    # Arrange
+    solver = Solver()
+    x = symbol_factory.BitVecSym('x', 256)
+    expression = x == symbol_factory.BitVecVal(2 , 256)
+
+    # Act
+    solver.add(expression)
+    result = solver.check()
+    model = solver.model()
+
+    decls = model.decls()
+
+    # Assert
+    assert z3.sat == result
+    assert x.raw.decl() in decls
+
+
+def test_get_item():
+    # Arrange
+    solver = Solver()
+    x = symbol_factory.BitVecSym('x', 256)
+    expression = x == symbol_factory.BitVecVal(2, 256)
+
+    # Act
+    solver.add(expression)
+    result = solver.check()
+    model = solver.model()
+
+    x_concrete = model[x.raw.decl()]
+
+    # Assert
+    assert z3.sat == result
+    assert 2 == x_concrete
+
+
+def test_as_long():
+    # Arrange
+    solver = Solver()
+    x = symbol_factory.BitVecSym('x', 256)
+    expression = x == symbol_factory.BitVecVal(2, 256)
+
+    # Act
+    solver.add(expression)
+    result = solver.check()
+    model = solver.model()
+
+    x_concrete = model.eval(x.raw).as_long()
+
+    # Assert
+    assert z3.sat == result
+    assert 2 == x_concrete

From 1a65e8e4c902e0924e08f9af556635bdbd7b6739 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 28 Jan 2019 16:32:53 +0100
Subject: [PATCH 16/32] adapt tests according to style rules

---
 tests/laser/smt/independece_solver_test.py | 94 +++++++++-------------
 tests/laser/smt/model_test.py              |  8 +-
 2 files changed, 44 insertions(+), 58 deletions(-)

diff --git a/tests/laser/smt/independece_solver_test.py b/tests/laser/smt/independece_solver_test.py
index a3a1aeef..615e92c9 100644
--- a/tests/laser/smt/independece_solver_test.py
+++ b/tests/laser/smt/independece_solver_test.py
@@ -1,5 +1,9 @@
-from mythril.laser.smt.independence_solver import _get_expr_variables, DependenceBucket, DependenceMap,\
-    IndependenceSolver
+from mythril.laser.smt.independence_solver import (
+    _get_expr_variables,
+    DependenceBucket,
+    DependenceMap,
+    IndependenceSolver,
+)
 from mythril.laser.smt import symbol_factory
 
 import z3
@@ -7,10 +11,10 @@ import z3
 
 def test_get_expr_variables():
     # Arrange
-    x = z3.Bool('x')
-    y = z3.BitVec('y', 256)
-    z = z3.BitVec('z', 256)
-    b = z3.BitVec('b', 256)
+    x = z3.Bool("x")
+    y = z3.BitVec("y", 256)
+    z = z3.BitVec("z", 256)
+    b = z3.BitVec("b", 256)
     expression = z3.If(x, y, z + b)
 
     # Act
@@ -25,7 +29,7 @@ def test_get_expr_variables():
 
 def test_get_expr_variables_num():
     # Arrange
-    b = z3.BitVec('b', 256)
+    b = z3.BitVec("b", 256)
     expression = b + z3.BitVecVal(2, 256)
 
     # Act
@@ -37,7 +41,7 @@ def test_get_expr_variables_num():
 
 def test_create_bucket():
     # Arrange
-    x = z3.Bool('x')
+    x = z3.Bool("x")
 
     # Act
     bucket = DependenceBucket([x], [x])
@@ -49,17 +53,13 @@ def test_create_bucket():
 
 def test_dependence_map():
     # Arrange
-    x = z3.BitVec('x', 256)
-    y = z3.BitVec('y', 256)
-    z = z3.BitVec('z', 256)
-    a = z3.BitVec('a', 256)
-    b = z3.BitVec('b', 256)
-
-    conditions = [
-        x > y,
-        y == z,
-        a == b
-    ]
+    x = z3.BitVec("x", 256)
+    y = z3.BitVec("y", 256)
+    z = z3.BitVec("z", 256)
+    a = z3.BitVec("a", 256)
+    b = z3.BitVec("b", 256)
+
+    conditions = [x > y, y == z, a == b]
 
     dependence_map = DependenceMap()
 
@@ -85,18 +85,13 @@ def test_dependence_map():
 
 def test_Independence_solver_unsat():
     # Arrange
-    x = symbol_factory.BitVecSym('x', 256)
-    y = symbol_factory.BitVecSym('y', 256)
-    z = symbol_factory.BitVecSym('z', 256)
-    a = symbol_factory.BitVecSym('a', 256)
-    b = symbol_factory.BitVecSym('b', 256)
-
-    conditions = [
-        x > y,
-        y == z,
-        y != z,
-        a == b
-    ]
+    x = symbol_factory.BitVecSym("x", 256)
+    y = symbol_factory.BitVecSym("y", 256)
+    z = symbol_factory.BitVecSym("z", 256)
+    a = symbol_factory.BitVecSym("a", 256)
+    b = symbol_factory.BitVecSym("b", 256)
+
+    conditions = [x > y, y == z, y != z, a == b]
 
     solver = IndependenceSolver()
 
@@ -110,18 +105,13 @@ def test_Independence_solver_unsat():
 
 def test_independence_solver_unsat_in_second_bucket():
     # Arrange
-    x = symbol_factory.BitVecSym('x', 256)
-    y = symbol_factory.BitVecSym('y', 256)
-    z = symbol_factory.BitVecSym('z', 256)
-    a = symbol_factory.BitVecSym('a', 256)
-    b = symbol_factory.BitVecSym('b', 256)
-
-    conditions = [
-        x > y,
-        y == z,
-        a == b,
-        a != b
-    ]
+    x = symbol_factory.BitVecSym("x", 256)
+    y = symbol_factory.BitVecSym("y", 256)
+    z = symbol_factory.BitVecSym("z", 256)
+    a = symbol_factory.BitVecSym("a", 256)
+    b = symbol_factory.BitVecSym("b", 256)
+
+    conditions = [x > y, y == z, a == b, a != b]
 
     solver = IndependenceSolver()
 
@@ -135,17 +125,13 @@ def test_independence_solver_unsat_in_second_bucket():
 
 def test_independence_solver_sat():
     # Arrange
-    x = symbol_factory.BitVecSym('x', 256)
-    y = symbol_factory.BitVecSym('y', 256)
-    z = symbol_factory.BitVecSym('z', 256)
-    a = symbol_factory.BitVecSym('a', 256)
-    b = symbol_factory.BitVecSym('b', 256)
-
-    conditions = [
-        x > y,
-        y == z,
-        a == b,
-    ]
+    x = symbol_factory.BitVecSym("x", 256)
+    y = symbol_factory.BitVecSym("y", 256)
+    z = symbol_factory.BitVecSym("z", 256)
+    a = symbol_factory.BitVecSym("a", 256)
+    b = symbol_factory.BitVecSym("b", 256)
+
+    conditions = [x > y, y == z, a == b]
 
     solver = IndependenceSolver()
 
diff --git a/tests/laser/smt/model_test.py b/tests/laser/smt/model_test.py
index 4b799afe..7f9ae1d3 100644
--- a/tests/laser/smt/model_test.py
+++ b/tests/laser/smt/model_test.py
@@ -5,8 +5,8 @@ import z3
 def test_decls():
     # Arrange
     solver = Solver()
-    x = symbol_factory.BitVecSym('x', 256)
-    expression = x == symbol_factory.BitVecVal(2 , 256)
+    x = symbol_factory.BitVecSym("x", 256)
+    expression = x == symbol_factory.BitVecVal(2, 256)
 
     # Act
     solver.add(expression)
@@ -23,7 +23,7 @@ def test_decls():
 def test_get_item():
     # Arrange
     solver = Solver()
-    x = symbol_factory.BitVecSym('x', 256)
+    x = symbol_factory.BitVecSym("x", 256)
     expression = x == symbol_factory.BitVecVal(2, 256)
 
     # Act
@@ -41,7 +41,7 @@ def test_get_item():
 def test_as_long():
     # Arrange
     solver = Solver()
-    x = symbol_factory.BitVecSym('x', 256)
+    x = symbol_factory.BitVecSym("x", 256)
     expression = x == symbol_factory.BitVecVal(2, 256)
 
     # Act

From 773583721bff276f818f6ab8ee15211565318369 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 31 Jan 2019 12:24:39 +0100
Subject: [PATCH 17/32] add return value types

---
 mythril/laser/smt/independence_solver.py | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index 887c71d6..b66f14de 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -1,10 +1,10 @@
 import z3
 
 from mythril.laser.smt import Model
-from typing import Set
+from typing import Set, List
 
 
-def _get_expr_variables(expression: z3.ExprRef):
+def _get_expr_variables(expression: z3.ExprRef) -> List[z3.ExprRef]:
     """
     Get's the variables that make up the current expression
     :param expression:
@@ -40,7 +40,7 @@ class DependenceMap:
         self.buckets = []
         self.variable_map = {}
 
-    def add_condition(self, condition: z3.BoolRef):
+    def add_condition(self, condition: z3.BoolRef) -> None:
         """
         Add condition to the dependence map
         :param condition: The condition that is to be added to the dependence map
@@ -65,7 +65,7 @@ class DependenceMap:
         for variable in variables:
             self.variable_map[str(variable)] = new_bucket
 
-    def merge_buckets(self, bucket_list: Set[DependenceBucket]):
+    def merge_buckets(self, bucket_list: Set[DependenceBucket]) -> DependenceBucket:
         """ Merges the buckets in bucket list """
         variables = []
         conditions = []
@@ -113,7 +113,7 @@ class IndependenceSolver:
         constraints = [c.raw for c in constraints]
         self.constraints.extend(constraints)
 
-    def check(self):
+    def check(self) -> z3.CheckSatResult:
         """Returns z3 smt check result. """
         dependence_map = DependenceMap()
         for constraint in self.constraints:
@@ -133,7 +133,7 @@ class IndependenceSolver:
 
         return z3.sat
 
-    def model(self):
+    def model(self) -> Model:
         """Returns z3 model for a solution. """
         return Model(self.models)
 

From d6e30078fbfba3a1e0fb4d41b178396c8b2d0810 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 31 Jan 2019 12:28:31 +0100
Subject: [PATCH 18/32] add variable type annotations

---
 mythril/laser/smt/independence_solver.py | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index b66f14de..74b3f8eb 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -1,7 +1,7 @@
 import z3
 
 from mythril.laser.smt import Model
-from typing import Set, List
+from typing import Set, List, Dict
 
 
 def _get_expr_variables(expression: z3.ExprRef) -> List[z3.ExprRef]:
@@ -28,8 +28,8 @@ class DependenceBucket:
         :param variables: Variables contained in the conditions
         :param conditions: The conditions that are dependent on each other
         """
-        self.variables = variables or []
-        self.conditions = conditions or []
+        self.variables = variables or []  # type: List[z3.ExprRef]
+        self.conditions = conditions or []  # type: List[z3.ExprRef]
 
 
 class DependenceMap:
@@ -37,8 +37,8 @@ class DependenceMap:
 
     def __init__(self):
         """ Initializes a DependenceMap object """
-        self.buckets = []
-        self.variable_map = {}
+        self.buckets = []  # type: List[DependenceBucket]
+        self.variable_map = {}  # type: Dict[str, DependenceBucket]
 
     def add_condition(self, condition: z3.BoolRef) -> None:
         """

From 4d02d5ae54079dd50629402ea7f8b9e9dd341f92 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 31 Jan 2019 12:29:02 +0100
Subject: [PATCH 19/32] fix typo

---
 mythril/laser/smt/independence_solver.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index 74b3f8eb..4ec04c6f 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -6,7 +6,7 @@ from typing import Set, List, Dict
 
 def _get_expr_variables(expression: z3.ExprRef) -> List[z3.ExprRef]:
     """
-    Get's the variables that make up the current expression
+    Gets the variables that make up the current expression
     :param expression:
     :return:
     """

From b336a1813287e741e76026621ca758f1ef54a8b0 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 31 Jan 2019 12:34:36 +0100
Subject: [PATCH 20/32] refactor solvers to work based of * variable

---
 mythril/laser/smt/independence_solver.py   |  9 +++++----
 mythril/laser/smt/solver.py                | 13 +++++--------
 tests/laser/smt/independece_solver_test.py |  6 +++---
 3 files changed, 13 insertions(+), 15 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index 4ec04c6f..39ecb5c1 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -1,7 +1,8 @@
 import z3
 
-from mythril.laser.smt import Model
-from typing import Set, List, Dict
+from mythril.laser.smt.model import Model
+from mythril.laser.smt.bool import Bool
+from typing import Set, List, Dict, Union
 
 
 def _get_expr_variables(expression: z3.ExprRef) -> List[z3.ExprRef]:
@@ -97,7 +98,7 @@ class IndependenceSolver:
         """
         self.raw.set(timeout=timeout)
 
-    def add(self, constraints: list) -> None:
+    def add(self, *constraints: List[Bool]) -> None:
         """Adds the constraints to this solver.
 
         :param constraints: constraints to add
@@ -105,7 +106,7 @@ class IndependenceSolver:
         constraints = [c.raw for c in constraints]
         self.constraints.extend(constraints)
 
-    def append(self, constraints: list) -> None:
+    def append(self, *constraints: List[Bool]) -> None:
         """Adds the constraints to this solver.
 
         :param constraints: constraints to add
diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver.py
index 3794c613..eac02c0d 100644
--- a/mythril/laser/smt/solver.py
+++ b/mythril/laser/smt/solver.py
@@ -3,6 +3,9 @@ import z3
 
 from mythril.laser.smt.expression import Expression
 from mythril.laser.smt.model import Model
+from mythril.laser.smt.bool import Bool
+
+from typing import List
 
 
 class Solver:
@@ -20,27 +23,21 @@ class Solver:
         """
         self.raw.set(timeout=timeout)
 
-    def add(self, constraints: list) -> None:
+    def add(self, *constraints: List[Bool]) -> None:
         """Adds the constraints to this solver.
 
         :param constraints:
         :return:
         """
-        if not isinstance(constraints, list):
-            self.raw.add(constraints.raw)
-            return
         constraints = [c.raw for c in constraints]
         self.raw.add(constraints)
 
-    def append(self, constraints: list) -> None:
+    def append(self, *constraints: List[Bool]) -> None:
         """Adds the constraints to this solver.
 
         :param constraints:
         :return:
         """
-        if not isinstance(constraints, list):
-            self.raw.append(constraints.raw)
-            return
         constraints = [c.raw for c in constraints]
         self.raw.add(constraints)
 
diff --git a/tests/laser/smt/independece_solver_test.py b/tests/laser/smt/independece_solver_test.py
index 615e92c9..26c2eba4 100644
--- a/tests/laser/smt/independece_solver_test.py
+++ b/tests/laser/smt/independece_solver_test.py
@@ -96,7 +96,7 @@ def test_Independence_solver_unsat():
     solver = IndependenceSolver()
 
     # Act
-    solver.add(conditions)
+    solver.add(*conditions)
     result = solver.check()
 
     # Assert
@@ -116,7 +116,7 @@ def test_independence_solver_unsat_in_second_bucket():
     solver = IndependenceSolver()
 
     # Act
-    solver.add(conditions)
+    solver.add(*conditions)
     result = solver.check()
 
     # Assert
@@ -136,7 +136,7 @@ def test_independence_solver_sat():
     solver = IndependenceSolver()
 
     # Act
-    solver.add(conditions)
+    solver.add(*conditions)
     result = solver.check()
 
     # Assert

From 3761a2cbefdd2f9cc3c8ea7b5d0369ddd6003d8c Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 31 Jan 2019 12:38:10 +0100
Subject: [PATCH 21/32] add check to tests

This ensures that not only the variables are in the list, but they
are the only variables in that list
---
 tests/laser/smt/independece_solver_test.py | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tests/laser/smt/independece_solver_test.py b/tests/laser/smt/independece_solver_test.py
index 26c2eba4..829b4707 100644
--- a/tests/laser/smt/independece_solver_test.py
+++ b/tests/laser/smt/independece_solver_test.py
@@ -73,12 +73,14 @@ def test_dependence_map():
     assert x in dependence_map.buckets[0].variables
     assert y in dependence_map.buckets[0].variables
     assert z in dependence_map.buckets[0].variables
+    assert len(set(dependence_map.buckets[0].variables)) == 3
 
     assert conditions[0] in dependence_map.buckets[0].conditions
     assert conditions[1] in dependence_map.buckets[0].conditions
 
     assert a in dependence_map.buckets[1].variables
     assert b in dependence_map.buckets[1].variables
+    assert len(set(dependence_map.buckets[1].variables)) == 2
 
     assert conditions[2] in dependence_map.buckets[1].conditions
 

From ca1e97f965ae586fd659803d30797fbbd8557831 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 31 Jan 2019 12:39:32 +0100
Subject: [PATCH 22/32] refactor a bit of redundant code

---
 mythril/laser/smt/independence_solver.py | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index 39ecb5c1..1bad8261 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -125,12 +125,10 @@ class IndependenceSolver:
             self.raw.reset()
             self.raw.append(*bucket.conditions)
             check_result = self.raw.check()
-            if check_result == z3.unsat:
-                return z3.unsat
-            elif check_result == z3.unknown:
-                return z3.unknown
-            else:
+            if check_result == z3.sat:
                 self.models.append(self.raw.model())
+            else:
+                return check_result
 
         return z3.sat
 

From aa94258e2606c82f7b77f6397ea36fada3d75003 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 31 Jan 2019 12:43:10 +0100
Subject: [PATCH 23/32] add type hints to model

---
 mythril/laser/smt/model.py | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/mythril/laser/smt/model.py b/mythril/laser/smt/model.py
index e0eb3830..76188a22 100644
--- a/mythril/laser/smt/model.py
+++ b/mythril/laser/smt/model.py
@@ -1,5 +1,7 @@
 import z3
 
+from typing import Union, List
+
 
 class Model:
     """ The model class wraps a z3 model
@@ -8,21 +10,21 @@ class Model:
     which has models for multiple queries which need an uniform output.
     """
 
-    def __init__(self, models=None):
+    def __init__(self, models: List[z3.ModelRef] = None):
         """
         Initialize a model object
         :param models: the internal z3 models that this model should use
         """
         self.raw = models or []
 
-    def decls(self):
+    def decls(self) -> List[z3.ExprRef]:
         """Get the declarations for this model"""
         result = []
         for internal_model in self.raw:
             result.extend(internal_model.decls())
         return result
 
-    def __getitem__(self, item):
+    def __getitem__(self, item) -> Union[None, z3.ExprRef]:
         """ Get declaration from model
          If item is an int, then the declaration at offset item is returned
          If item is a declaration, then the interpretation is returned
@@ -40,7 +42,7 @@ class Model:
                 continue
         return None
 
-    def eval(self, expression: z3.ExprRef, model_completion: bool = False):
+    def eval(self, expression: z3.ExprRef, model_completion: bool = False) -> Union[None, z3.ExprRef]:
         """ Evaluate the expression using this model
 
         :param expression: The expression to evaluate

From 05ddc59c77f6a1363a3b61096d3a4ca691222e95 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 31 Jan 2019 12:44:11 +0100
Subject: [PATCH 24/32] refactor merge buckets to be private

---
 mythril/laser/smt/independence_solver.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index 1bad8261..9cafa8db 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -61,12 +61,12 @@ class DependenceMap:
         if relevant_buckets:
             # Merge buckets, and rewrite variable map accordingly
             relevant_buckets.add(new_bucket)
-            new_bucket = self.merge_buckets(relevant_buckets)
+            new_bucket = self._merge_buckets(relevant_buckets)
 
         for variable in variables:
             self.variable_map[str(variable)] = new_bucket
 
-    def merge_buckets(self, bucket_list: Set[DependenceBucket]) -> DependenceBucket:
+    def _merge_buckets(self, bucket_list: Set[DependenceBucket]) -> DependenceBucket:
         """ Merges the buckets in bucket list """
         variables = []
         conditions = []

From 959635253d105d826d4ca061db188577a7d3ee1e Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 31 Jan 2019 13:14:00 +0100
Subject: [PATCH 25/32] apply style rules

---
 mythril/laser/smt/model.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/mythril/laser/smt/model.py b/mythril/laser/smt/model.py
index 76188a22..2cc80351 100644
--- a/mythril/laser/smt/model.py
+++ b/mythril/laser/smt/model.py
@@ -42,7 +42,9 @@ class Model:
                 continue
         return None
 
-    def eval(self, expression: z3.ExprRef, model_completion: bool = False) -> Union[None, z3.ExprRef]:
+    def eval(
+        self, expression: z3.ExprRef, model_completion: bool = False
+    ) -> Union[None, z3.ExprRef]:
         """ Evaluate the expression using this model
 
         :param expression: The expression to evaluate

From 105feb44ac8bb1e1675e0eccb8b45d7aeb6465cd Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 31 Jan 2019 13:29:47 +0100
Subject: [PATCH 26/32] fix calldata tests

---
 tests/laser/state/calldata_test.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/laser/state/calldata_test.py b/tests/laser/state/calldata_test.py
index f32f297a..46c28585 100644
--- a/tests/laser/state/calldata_test.py
+++ b/tests/laser/state/calldata_test.py
@@ -48,7 +48,7 @@ def test_concrete_calldata_constrain_index():
     value = calldata[2]
     constraint = value == 3
 
-    solver.add([constraint])
+    solver.add(constraint)
     result = solver.check()
 
     # Assert
@@ -65,7 +65,7 @@ def test_symbolic_calldata_constrain_index():
 
     constraints = [value == 1, calldata.calldatasize == 50]
 
-    solver.add(constraints)
+    solver.add(*constraints)
 
     result = solver.check()
 

From caa06776c55fff275904a55c4882b2c1337bc558 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 4 Feb 2019 14:47:22 +0100
Subject: [PATCH 27/32] interpret constraints as * argument

---
 mythril/laser/smt/solver.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver.py
index d8e32abc..18b43bca 100644
--- a/mythril/laser/smt/solver.py
+++ b/mythril/laser/smt/solver.py
@@ -38,7 +38,7 @@ class BaseSolver(Generic[T]):
         :param constraints:
         :return:
         """
-        self.add(constraints)
+        self.add(*constraints)
 
     def check(self) -> z3.CheckSatResult:
         """Returns z3 smt check result.

From a772d58caa86526b43a674c61ed112998b8b74f0 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 4 Feb 2019 14:55:30 +0100
Subject: [PATCH 28/32] add type cast to solver

---
 mythril/laser/smt/solver.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver.py
index 18b43bca..d9453263 100644
--- a/mythril/laser/smt/solver.py
+++ b/mythril/laser/smt/solver.py
@@ -29,7 +29,7 @@ class BaseSolver(Generic[T]):
         :param constraints:
         :return:
         """
-        z3_constraints = [c.raw for c in constraints]  # type: Sequence[z3.BoolRef]
+        z3_constraints = [c.raw for c in cast(List[Bool], constraints)]  # type: Sequence[z3.BoolRef]
         self.raw.add(z3_constraints)
 
     def append(self, *constraints: List[Bool]) -> None:

From 94ea7831c60131fbae7baf2ebeaf508777b228ae Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 4 Feb 2019 14:55:39 +0100
Subject: [PATCH 29/32] add required type hint

---
 mythril/laser/smt/model.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mythril/laser/smt/model.py b/mythril/laser/smt/model.py
index 2cc80351..b0c72d5c 100644
--- a/mythril/laser/smt/model.py
+++ b/mythril/laser/smt/model.py
@@ -19,7 +19,7 @@ class Model:
 
     def decls(self) -> List[z3.ExprRef]:
         """Get the declarations for this model"""
-        result = []
+        result = []  # type: List[z3.ExprRef]
         for internal_model in self.raw:
             result.extend(internal_model.decls())
         return result

From 50a6080e78142df9b5a7e222e70294bcc7ca6963 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 4 Feb 2019 14:57:52 +0100
Subject: [PATCH 30/32] add missing type hints to independence solver

---
 mythril/laser/smt/independence_solver.py | 10 +++++-----
 mythril/laser/smt/solver.py              |  4 +++-
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index 9cafa8db..fbb8c9a1 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -2,7 +2,7 @@ import z3
 
 from mythril.laser.smt.model import Model
 from mythril.laser.smt.bool import Bool
-from typing import Set, List, Dict, Union
+from typing import Set, List, Dict, Union, cast
 
 
 def _get_expr_variables(expression: z3.ExprRef) -> List[z3.ExprRef]:
@@ -68,8 +68,8 @@ class DependenceMap:
 
     def _merge_buckets(self, bucket_list: Set[DependenceBucket]) -> DependenceBucket:
         """ Merges the buckets in bucket list """
-        variables = []
-        conditions = []
+        variables = []  # type: List[str]
+        conditions = []  # type: List[z3.BoolRef]
         for bucket in bucket_list:
             self.buckets.remove(bucket)
             variables += bucket.variables
@@ -103,7 +103,7 @@ class IndependenceSolver:
 
         :param constraints: constraints to add
         """
-        constraints = [c.raw for c in constraints]
+        constraints = [c.raw for c in cast(List[Bool], constraints)]
         self.constraints.extend(constraints)
 
     def append(self, *constraints: List[Bool]) -> None:
@@ -111,7 +111,7 @@ class IndependenceSolver:
 
         :param constraints: constraints to add
         """
-        constraints = [c.raw for c in constraints]
+        constraints = [c.raw for c in cast(List[Bool], constraints)]
         self.constraints.extend(constraints)
 
     def check(self) -> z3.CheckSatResult:
diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver.py
index d9453263..b3754e94 100644
--- a/mythril/laser/smt/solver.py
+++ b/mythril/laser/smt/solver.py
@@ -29,7 +29,9 @@ class BaseSolver(Generic[T]):
         :param constraints:
         :return:
         """
-        z3_constraints = [c.raw for c in cast(List[Bool], constraints)]  # type: Sequence[z3.BoolRef]
+        z3_constraints = [
+            c.raw for c in cast(List[Bool], constraints)
+        ]  # type: Sequence[z3.BoolRef]
         self.raw.add(z3_constraints)
 
     def append(self, *constraints: List[Bool]) -> None:

From 3ca11d9262224b90888f219c9d02bb03481a810f Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 4 Feb 2019 17:29:05 +0100
Subject: [PATCH 31/32] fix type errors

---
 mythril/laser/smt/independence_solver.py | 10 +++++-----
 mythril/laser/smt/model.py               |  1 +
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index fbb8c9a1..0a576580 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -2,7 +2,7 @@ import z3
 
 from mythril.laser.smt.model import Model
 from mythril.laser.smt.bool import Bool
-from typing import Set, List, Dict, Union, cast
+from typing import Set, Tuple, Dict, List, cast
 
 
 def _get_expr_variables(expression: z3.ExprRef) -> List[z3.ExprRef]:
@@ -98,20 +98,20 @@ class IndependenceSolver:
         """
         self.raw.set(timeout=timeout)
 
-    def add(self, *constraints: List[Bool]) -> None:
+    def add(self, *constraints: Tuple[Bool]) -> None:
         """Adds the constraints to this solver.
 
         :param constraints: constraints to add
         """
-        constraints = [c.raw for c in cast(List[Bool], constraints)]
+        constraints = [c.raw for c in cast(Tuple[Bool], constraints)]
         self.constraints.extend(constraints)
 
-    def append(self, *constraints: List[Bool]) -> None:
+    def append(self, *constraints: Tuple[Bool]) -> None:
         """Adds the constraints to this solver.
 
         :param constraints: constraints to add
         """
-        constraints = [c.raw for c in cast(List[Bool], constraints)]
+        constraints = [c.raw for c in cast(Tuple[Bool], constraints)]
         self.constraints.extend(constraints)
 
     def check(self) -> z3.CheckSatResult:
diff --git a/mythril/laser/smt/model.py b/mythril/laser/smt/model.py
index b0c72d5c..524683e9 100644
--- a/mythril/laser/smt/model.py
+++ b/mythril/laser/smt/model.py
@@ -56,3 +56,4 @@ class Model:
             is_relevant_model = expression.decl() in list(internal_model.decls())
             if is_relevant_model or is_last_model:
                 return internal_model.eval(expression, model_completion)
+        return None

From 02abfa1d68239b2b2d20420ecae77c2388a96416 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 4 Feb 2019 17:41:43 +0100
Subject: [PATCH 32/32] use separate variable for type purposes

---
 mythril/laser/smt/independence_solver.py | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py
index 0a576580..781a26fd 100644
--- a/mythril/laser/smt/independence_solver.py
+++ b/mythril/laser/smt/independence_solver.py
@@ -103,16 +103,20 @@ class IndependenceSolver:
 
         :param constraints: constraints to add
         """
-        constraints = [c.raw for c in cast(Tuple[Bool], constraints)]
-        self.constraints.extend(constraints)
+        raw_constraints = [
+            c.raw for c in cast(Tuple[Bool], constraints)
+        ]  # type: List[z3.BoolRef]
+        self.constraints.extend(raw_constraints)
 
     def append(self, *constraints: Tuple[Bool]) -> None:
         """Adds the constraints to this solver.
 
         :param constraints: constraints to add
         """
-        constraints = [c.raw for c in cast(Tuple[Bool], constraints)]
-        self.constraints.extend(constraints)
+        raw_constraints = [
+            c.raw for c in cast(Tuple[Bool], constraints)
+        ]  # type: List[z3.BoolRef]
+        self.constraints.extend(raw_constraints)
 
     def check(self) -> z3.CheckSatResult:
         """Returns z3 smt check result. """