Repository: Consensys/mythril (language: python)

Issue:
Issue with Contract construction
## Description
Issue with contract construction for this contract, Found in Discord
```
contract QuickSort {
    
    uint[] array;
    uint[] arrayPrecalced1  = [388, 908, 564, 73, 132, 270, 791, 360, 490, 922, 377, 529, 606, 214, 80, 857, 799, 739, 189, 441, 397, 995, 47, 190, 597, 67, 91, 406, 76, 430, 338, 282, 888, 570, 119, 395, 785, 589, 933, 817, 395, 103, 291, 812, 244, 329, 723, 733, 295, 599, 981, 407, 56, 100, 945, 12, 629, 239, 54, 771, 575, 731, 718, 424, 732, 172, 120, 895, 312, 2, 902, 289, 82, 249, 509, 381, 983, 397, 267, 963, 200, 898, 417, 909, 655, 477, 774, 23, 896, 723, 25, 966, 51, 145, 66, 235, 79, 85, 331, 134];
    uint[] arrayPrecalced2  = [388, 908, 564, 73, 132, 270, 791, 360, 490, 922, 377, 529, 606, 214, 80, 857, 799, 739, 189, 441];


    function sort(uint[] memory data) public returns( uint[] memory) 
    {
       quickSort(data, int(0), int(data.length - 1));
       return data;
    }
    
    function quickSort(uint[] memory arr, int left, int right) internal
    {
        require(arr.length != 0);
        int i = left;
        int j = right;
        if(i==j) 
        {
            return;
        }
        uint pivot = arr[uint(left + (right - left) / 2)];
        while (i <= j) 
        {
            while (arr[uint(i)] < pivot) 
            {
                i++;
            }
            while (pivot < arr[uint(j)]) 
            {
                j--;
            }
            if (i <= j) 
            {
                (arr[uint(i)], arr[uint(j)]) = (arr[uint(j)], arr[uint(i)]);
                i++;
                j--;
            }
        }
        if (left < j)
            quickSort(arr, left, j);
        if (i < right)
            quickSort(arr, i, right);
        
        assert(arr.length > 3);
    }
}

```

## How to Reproduce

```console
$ myth -v4 analyze file.sol
mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout) Check whether the bytecode is indeed the creation code, otherwise use the --bin-runtime flag

$
```





Discussion / hints:

Fix patch:
diff --git a/.github/ISSUE_TEMPLATE/bug-report.md b/.github/ISSUE_TEMPLATE/bug-report.md
index cde4e3079..5c9c55a2c 100644
--- a/.github/ISSUE_TEMPLATE/bug-report.md
+++ b/.github/ISSUE_TEMPLATE/bug-report.md
@@ -37,7 +37,7 @@ or perhaps:
 4. See error
 
 
-If there is a Solidity source code, a truffle project, or bytecode
+If there is a Solidity source code or a bytecode
 that is involved, please provide that or links to it.
 
 -->
diff --git a/docs/source/analysis-modules.rst b/docs/source/analysis-modules.rst
index d17515470..bd1fd71fd 100644
--- a/docs/source/analysis-modules.rst
+++ b/docs/source/analysis-modules.rst
@@ -1,7 +1,7 @@
 Analysis Modules
 ================
 
-Mythril's detection capabilities are written in modules in the `/analysis/modules <https://github.com/ConsenSys/mythril/tree/master/mythril/analysis/modules>`_ directory.
+Mythril's detection capabilities are written in modules in the `/analysis/module/modules <https://github.com/ConsenSys/mythril/tree/master/mythril/analysis/module/modules>`_ directory.
 
 
 .. toctree::
diff --git a/docs/source/conf.py b/docs/source/conf.py
index 1c06fbc47..ec07064bb 100644
--- a/docs/source/conf.py
+++ b/docs/source/conf.py
@@ -132,7 +132,13 @@
 # (source start file, target name, title,
 #  author, documentclass [howto, manual, or own class]).
 latex_documents = [
-    (master_doc, "Mythril.tex", "Mythril Documentation", "Bernhard Mueller", "manual")
+    (
+        master_doc,
+        "Mythril.tex",
+        "Mythril Documentation",
+        "ConsenSys Dilligence",
+        "manual",
+    )
 ]
 
 
diff --git a/docs/source/index.rst b/docs/source/index.rst
index 77ff628d8..4fab9da76 100644
--- a/docs/source/index.rst
+++ b/docs/source/index.rst
@@ -7,9 +7,9 @@ Welcome to Mythril's documentation!
 
    about
    installation
+   tutorial
    security-analysis
    analysis-modules
-   mythx-analysis
    mythril
 
 
diff --git a/docs/source/module-list.rst b/docs/source/module-list.rst
index 106cd8c90..c78a82e1b 100644
--- a/docs/source/module-list.rst
+++ b/docs/source/module-list.rst
@@ -13,11 +13,6 @@ Dependence on Predictable Variables
 
 The `predictable variables module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/dependence_on_predictable_vars.py>`_ detects `SWC-120 (Weak Randomness) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-120>`_ and `SWC-116 (Timestamp Dependence) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-116>`_.
 
-******************
-Deprecated Opcodes
-******************
-
-The `deprecated opcodes module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/deprecated_ops.py>`_ detects `SWC-111 (Use of Deprecated Functions) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-111>`_.
 
 ***********
 Ether Thief
@@ -68,15 +63,15 @@ Unchecked Retval
 
 The `unchecked retval module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/unchecked_retval.py>`_ detects `SWC-104 (Unchecked Call Return Value) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-104>`_.
 
-****************
+************************
 User Supplied assertion
-****************
+************************
 
 The `user supplied assertion module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/user_assertions.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_ for user-supplied assertions. User supplied assertions should be log messages of the form: :code:`emit AssertionFailed(string)`.
 
-****************
+************************
 Arbitrary Storage Write
-****************
+************************
 
 The `arbitrary storage write module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/arbitrary_write.py>`_ detects `SWC-124 (Write to Arbitrary Storage Location) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-124>`_.
 
diff --git a/docs/source/modules.rst b/docs/source/modules.rst
new file mode 100644
index 000000000..cbf872198
--- /dev/null
+++ b/docs/source/modules.rst
@@ -0,0 +1,7 @@
+mythril
+=======
+
+.. toctree::
+   :maxdepth: 4
+
+   mythril
diff --git a/docs/source/mythril.analysis.module.modules.rst b/docs/source/mythril.analysis.module.modules.rst
new file mode 100644
index 000000000..b758edc3d
--- /dev/null
+++ b/docs/source/mythril.analysis.module.modules.rst
@@ -0,0 +1,125 @@
+mythril.analysis.module.modules package
+=======================================
+
+Submodules
+----------
+
+mythril.analysis.module.modules.arbitrary\_jump module
+------------------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.arbitrary_jump
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.modules.arbitrary\_write module
+-------------------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.arbitrary_write
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.modules.delegatecall module
+---------------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.delegatecall
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.modules.dependence\_on\_origin module
+-------------------------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.dependence_on_origin
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.modules.dependence\_on\_predictable\_vars module
+------------------------------------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.dependence_on_predictable_vars
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.modules.ether\_thief module
+---------------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.ether_thief
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.modules.exceptions module
+-------------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.exceptions
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.modules.external\_calls module
+------------------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.external_calls
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.modules.integer module
+----------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.integer
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.modules.multiple\_sends module
+------------------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.multiple_sends
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.modules.state\_change\_external\_calls module
+---------------------------------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.state_change_external_calls
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.modules.suicide module
+----------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.suicide
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.modules.unchecked\_retval module
+--------------------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.unchecked_retval
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.modules.user\_assertions module
+-------------------------------------------------------
+
+.. automodule:: mythril.analysis.module.modules.user_assertions
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+Module contents
+---------------
+
+.. automodule:: mythril.analysis.module.modules
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.analysis.module.rst b/docs/source/mythril.analysis.module.rst
new file mode 100644
index 000000000..a701c70f0
--- /dev/null
+++ b/docs/source/mythril.analysis.module.rst
@@ -0,0 +1,53 @@
+mythril.analysis.module package
+===============================
+
+Subpackages
+-----------
+
+.. toctree::
+   :maxdepth: 4
+
+   mythril.analysis.module.modules
+
+Submodules
+----------
+
+mythril.analysis.module.base module
+-----------------------------------
+
+.. automodule:: mythril.analysis.module.base
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.loader module
+-------------------------------------
+
+.. automodule:: mythril.analysis.module.loader
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.module\_helpers module
+----------------------------------------------
+
+.. automodule:: mythril.analysis.module.module_helpers
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.module.util module
+-----------------------------------
+
+.. automodule:: mythril.analysis.module.util
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+Module contents
+---------------
+
+.. automodule:: mythril.analysis.module
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.analysis.modules.rst b/docs/source/mythril.analysis.modules.rst
deleted file mode 100644
index 1db8bef4c..000000000
--- a/docs/source/mythril.analysis.modules.rst
+++ /dev/null
@@ -1,110 +0,0 @@
-mythril.analysis.modules package
-================================
-
-Submodules
-----------
-
-mythril.analysis.modules.base module
-------------------------------------
-
-.. automodule:: mythril.analysis.modules.base
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.analysis.modules.delegatecall module
---------------------------------------------
-
-.. automodule:: mythril.analysis.modules.delegatecall
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.analysis.modules.dependence\_on\_predictable\_vars module
------------------------------------------------------------------
-
-.. automodule:: mythril.analysis.modules.dependence_on_predictable_vars
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.analysis.modules.deprecated\_ops module
------------------------------------------------
-
-.. automodule:: mythril.analysis.modules.deprecated_ops
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.analysis.modules.ether\_thief module
---------------------------------------------
-
-.. automodule:: mythril.analysis.modules.ether_thief
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.analysis.modules.exceptions module
-------------------------------------------
-
-.. automodule:: mythril.analysis.modules.exceptions
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.analysis.modules.external\_calls module
------------------------------------------------
-
-.. automodule:: mythril.analysis.modules.external_calls
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.analysis.modules.integer module
----------------------------------------
-
-.. automodule:: mythril.analysis.modules.integer
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.analysis.modules.multiple\_sends module
------------------------------------------------
-
-.. automodule:: mythril.analysis.modules.multiple_sends
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.analysis.modules.suicide module
----------------------------------------
-
-.. automodule:: mythril.analysis.modules.suicide
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.analysis.modules.transaction\_order\_dependence module
---------------------------------------------------------------
-
-.. automodule:: mythril.analysis.modules.transaction_order_dependence
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.analysis.modules.unchecked\_retval module
--------------------------------------------------
-
-.. automodule:: mythril.analysis.modules.unchecked_retval
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-
-Module contents
----------------
-
-.. automodule:: mythril.analysis.modules
-    :members:
-    :undoc-members:
-    :show-inheritance:
diff --git a/docs/source/mythril.analysis.rst b/docs/source/mythril.analysis.rst
index 4b0003c0b..6f0f30f44 100644
--- a/docs/source/mythril.analysis.rst
+++ b/docs/source/mythril.analysis.rst
@@ -5,81 +5,113 @@ Subpackages
 -----------
 
 .. toctree::
+   :maxdepth: 4
 
-    mythril.analysis.modules
+   mythril.analysis.module
 
 Submodules
 ----------
 
+mythril.analysis.analysis\_args module
+--------------------------------------
+
+.. automodule:: mythril.analysis.analysis_args
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.call\_helpers module
+-------------------------------------
+
+.. automodule:: mythril.analysis.call_helpers
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
 mythril.analysis.callgraph module
 ---------------------------------
 
 .. automodule:: mythril.analysis.callgraph
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.issue\_annotation module
+-----------------------------------------
+
+.. automodule:: mythril.analysis.issue_annotation
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.analysis.ops module
 ---------------------------
 
 .. automodule:: mythril.analysis.ops
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.analysis.potential\_issues module
+-----------------------------------------
+
+.. automodule:: mythril.analysis.potential_issues
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.analysis.report module
 ------------------------------
 
 .. automodule:: mythril.analysis.report
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.analysis.security module
 --------------------------------
 
 .. automodule:: mythril.analysis.security
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.analysis.solver module
 ------------------------------
 
 .. automodule:: mythril.analysis.solver
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.analysis.swc\_data module
 ---------------------------------
 
 .. automodule:: mythril.analysis.swc_data
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.analysis.symbolic module
 --------------------------------
 
 .. automodule:: mythril.analysis.symbolic
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.analysis.traceexplore module
 ------------------------------------
 
 .. automodule:: mythril.analysis.traceexplore
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril.analysis
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.concolic.rst b/docs/source/mythril.concolic.rst
new file mode 100644
index 000000000..2b988b5f5
--- /dev/null
+++ b/docs/source/mythril.concolic.rst
@@ -0,0 +1,37 @@
+mythril.concolic package
+========================
+
+Submodules
+----------
+
+mythril.concolic.concolic\_execution module
+-------------------------------------------
+
+.. automodule:: mythril.concolic.concolic_execution
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.concolic.concrete\_data module
+--------------------------------------
+
+.. automodule:: mythril.concolic.concrete_data
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.concolic.find\_trace module
+-----------------------------------
+
+.. automodule:: mythril.concolic.find_trace
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+Module contents
+---------------
+
+.. automodule:: mythril.concolic
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.disassembler.rst b/docs/source/mythril.disassembler.rst
index d43c432b1..da8aa5086 100644
--- a/docs/source/mythril.disassembler.rst
+++ b/docs/source/mythril.disassembler.rst
@@ -8,23 +8,22 @@ mythril.disassembler.asm module
 -------------------------------
 
 .. automodule:: mythril.disassembler.asm
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.disassembler.disassembly module
 ---------------------------------------
 
 .. automodule:: mythril.disassembler.disassembly
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril.disassembler
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.ethereum.interface.leveldb.rst b/docs/source/mythril.ethereum.interface.leveldb.rst
deleted file mode 100644
index 8ef8f144b..000000000
--- a/docs/source/mythril.ethereum.interface.leveldb.rst
+++ /dev/null
@@ -1,46 +0,0 @@
-mythril.ethereum.interface.leveldb package
-==========================================
-
-Submodules
-----------
-
-mythril.ethereum.interface.leveldb.accountindexing module
----------------------------------------------------------
-
-.. automodule:: mythril.ethereum.interface.leveldb.accountindexing
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.ethereum.interface.leveldb.client module
-------------------------------------------------
-
-.. automodule:: mythril.ethereum.interface.leveldb.client
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.ethereum.interface.leveldb.eth\_db module
--------------------------------------------------
-
-.. automodule:: mythril.ethereum.interface.leveldb.eth_db
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.ethereum.interface.leveldb.state module
------------------------------------------------
-
-.. automodule:: mythril.ethereum.interface.leveldb.state
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-
-Module contents
----------------
-
-.. automodule:: mythril.ethereum.interface.leveldb
-    :members:
-    :undoc-members:
-    :show-inheritance:
diff --git a/docs/source/mythril.ethereum.interface.rpc.rst b/docs/source/mythril.ethereum.interface.rpc.rst
index 6e1d5c033..669c18202 100644
--- a/docs/source/mythril.ethereum.interface.rpc.rst
+++ b/docs/source/mythril.ethereum.interface.rpc.rst
@@ -8,47 +8,46 @@ mythril.ethereum.interface.rpc.base\_client module
 --------------------------------------------------
 
 .. automodule:: mythril.ethereum.interface.rpc.base_client
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.ethereum.interface.rpc.client module
 --------------------------------------------
 
 .. automodule:: mythril.ethereum.interface.rpc.client
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.ethereum.interface.rpc.constants module
 -----------------------------------------------
 
 .. automodule:: mythril.ethereum.interface.rpc.constants
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.ethereum.interface.rpc.exceptions module
 ------------------------------------------------
 
 .. automodule:: mythril.ethereum.interface.rpc.exceptions
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.ethereum.interface.rpc.utils module
 -------------------------------------------
 
 .. automodule:: mythril.ethereum.interface.rpc.utils
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril.ethereum.interface.rpc
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.ethereum.interface.rst b/docs/source/mythril.ethereum.interface.rst
index 5d96ee301..7d30ec4e5 100644
--- a/docs/source/mythril.ethereum.interface.rst
+++ b/docs/source/mythril.ethereum.interface.rst
@@ -5,14 +5,14 @@ Subpackages
 -----------
 
 .. toctree::
+   :maxdepth: 4
 
-    mythril.ethereum.interface.leveldb
-    mythril.ethereum.interface.rpc
+   mythril.ethereum.interface.rpc
 
 Module contents
 ---------------
 
 .. automodule:: mythril.ethereum.interface
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.ethereum.rst b/docs/source/mythril.ethereum.rst
index bc74d90a5..fc5008719 100644
--- a/docs/source/mythril.ethereum.rst
+++ b/docs/source/mythril.ethereum.rst
@@ -5,8 +5,9 @@ Subpackages
 -----------
 
 .. toctree::
+   :maxdepth: 4
 
-    mythril.ethereum.interface
+   mythril.ethereum.interface
 
 Submodules
 ----------
@@ -15,23 +16,22 @@ mythril.ethereum.evmcontract module
 -----------------------------------
 
 .. automodule:: mythril.ethereum.evmcontract
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.ethereum.util module
 ----------------------------
 
 .. automodule:: mythril.ethereum.util
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril.ethereum
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.interfaces.rst b/docs/source/mythril.interfaces.rst
index f4302787f..f43a2eff2 100644
--- a/docs/source/mythril.interfaces.rst
+++ b/docs/source/mythril.interfaces.rst
@@ -8,23 +8,22 @@ mythril.interfaces.cli module
 -----------------------------
 
 .. automodule:: mythril.interfaces.cli
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.interfaces.epic module
 ------------------------------
 
 .. automodule:: mythril.interfaces.epic
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril.interfaces
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.laser.ethereum.function_managers.rst b/docs/source/mythril.laser.ethereum.function_managers.rst
new file mode 100644
index 000000000..8f2182d12
--- /dev/null
+++ b/docs/source/mythril.laser.ethereum.function_managers.rst
@@ -0,0 +1,29 @@
+mythril.laser.ethereum.function\_managers package
+=================================================
+
+Submodules
+----------
+
+mythril.laser.ethereum.function\_managers.exponent\_function\_manager module
+----------------------------------------------------------------------------
+
+.. automodule:: mythril.laser.ethereum.function_managers.exponent_function_manager
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.ethereum.function\_managers.keccak\_function\_manager module
+--------------------------------------------------------------------------
+
+.. automodule:: mythril.laser.ethereum.function_managers.keccak_function_manager
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+Module contents
+---------------
+
+.. automodule:: mythril.laser.ethereum.function_managers
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.laser.ethereum.rst b/docs/source/mythril.laser.ethereum.rst
index 4750a605f..23cfb35a4 100644
--- a/docs/source/mythril.laser.ethereum.rst
+++ b/docs/source/mythril.laser.ethereum.rst
@@ -5,10 +5,12 @@ Subpackages
 -----------
 
 .. toctree::
+   :maxdepth: 4
 
-    mythril.laser.ethereum.state
-    mythril.laser.ethereum.strategy
-    mythril.laser.ethereum.transaction
+   mythril.laser.ethereum.function_managers
+   mythril.laser.ethereum.state
+   mythril.laser.ethereum.strategy
+   mythril.laser.ethereum.transaction
 
 Submodules
 ----------
@@ -17,87 +19,78 @@ mythril.laser.ethereum.call module
 ----------------------------------
 
 .. automodule:: mythril.laser.ethereum.call
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.cfg module
 ---------------------------------
 
 .. automodule:: mythril.laser.ethereum.cfg
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.evm\_exceptions module
 ---------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.evm_exceptions
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
-mythril.laser.ethereum.gas module
----------------------------------
+mythril.laser.ethereum.instruction\_data module
+-----------------------------------------------
 
-.. automodule:: mythril.laser.ethereum.gas
-    :members:
-    :undoc-members:
-    :show-inheritance:
+.. automodule:: mythril.laser.ethereum.instruction_data
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.instructions module
 ------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.instructions
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.laser.ethereum.keccak module
-------------------------------------
-
-.. automodule:: mythril.laser.ethereum.keccak
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.natives module
 -------------------------------------
 
 .. automodule:: mythril.laser.ethereum.natives
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.svm module
 ---------------------------------
 
 .. automodule:: mythril.laser.ethereum.svm
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
-mythril.laser.ethereum.taint\_analysis module
----------------------------------------------
+mythril.laser.ethereum.time\_handler module
+-------------------------------------------
 
-.. automodule:: mythril.laser.ethereum.taint_analysis
-    :members:
-    :undoc-members:
-    :show-inheritance:
+.. automodule:: mythril.laser.ethereum.time_handler
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.util module
 ----------------------------------
 
 .. automodule:: mythril.laser.ethereum.util
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril.laser.ethereum
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.laser.ethereum.state.rst b/docs/source/mythril.laser.ethereum.state.rst
index 188f7d585..5c132a849 100644
--- a/docs/source/mythril.laser.ethereum.state.rst
+++ b/docs/source/mythril.laser.ethereum.state.rst
@@ -8,79 +8,86 @@ mythril.laser.ethereum.state.account module
 -------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.state.account
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.state.annotation module
 ----------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.state.annotation
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.state.calldata module
 --------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.state.calldata
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.state.constraints module
 -----------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.state.constraints
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.state.environment module
 -----------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.state.environment
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.state.global\_state module
 -------------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.state.global_state
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.state.machine\_state module
 --------------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.state.machine_state
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.state.memory module
 ------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.state.memory
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.ethereum.state.return\_data module
+------------------------------------------------
+
+.. automodule:: mythril.laser.ethereum.state.return_data
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.state.world\_state module
 ------------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.state.world_state
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril.laser.ethereum.state
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.laser.ethereum.strategy.extensions.rst b/docs/source/mythril.laser.ethereum.strategy.extensions.rst
new file mode 100644
index 000000000..4d843dd45
--- /dev/null
+++ b/docs/source/mythril.laser.ethereum.strategy.extensions.rst
@@ -0,0 +1,21 @@
+mythril.laser.ethereum.strategy.extensions package
+==================================================
+
+Submodules
+----------
+
+mythril.laser.ethereum.strategy.extensions.bounded\_loops module
+----------------------------------------------------------------
+
+.. automodule:: mythril.laser.ethereum.strategy.extensions.bounded_loops
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+Module contents
+---------------
+
+.. automodule:: mythril.laser.ethereum.strategy.extensions
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.laser.ethereum.strategy.rst b/docs/source/mythril.laser.ethereum.strategy.rst
index 5175c866a..7b0cff889 100644
--- a/docs/source/mythril.laser.ethereum.strategy.rst
+++ b/docs/source/mythril.laser.ethereum.strategy.rst
@@ -1,6 +1,14 @@
 mythril.laser.ethereum.strategy package
 =======================================
 
+Subpackages
+-----------
+
+.. toctree::
+   :maxdepth: 4
+
+   mythril.laser.ethereum.strategy.extensions
+
 Submodules
 ----------
 
@@ -8,15 +16,30 @@ mythril.laser.ethereum.strategy.basic module
 --------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.strategy.basic
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.ethereum.strategy.beam module
+-------------------------------------------
+
+.. automodule:: mythril.laser.ethereum.strategy.beam
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.ethereum.strategy.concolic module
+-----------------------------------------------
 
+.. automodule:: mythril.laser.ethereum.strategy.concolic
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril.laser.ethereum.strategy
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.laser.ethereum.transaction.rst b/docs/source/mythril.laser.ethereum.transaction.rst
index 339e1683d..3a063bf2e 100644
--- a/docs/source/mythril.laser.ethereum.transaction.rst
+++ b/docs/source/mythril.laser.ethereum.transaction.rst
@@ -8,31 +8,30 @@ mythril.laser.ethereum.transaction.concolic module
 --------------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.transaction.concolic
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.transaction.symbolic module
 --------------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.transaction.symbolic
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.ethereum.transaction.transaction\_models module
 -------------------------------------------------------------
 
 .. automodule:: mythril.laser.ethereum.transaction.transaction_models
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril.laser.ethereum.transaction
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.laser.plugin.plugins.coverage.rst b/docs/source/mythril.laser.plugin.plugins.coverage.rst
new file mode 100644
index 000000000..147d3c828
--- /dev/null
+++ b/docs/source/mythril.laser.plugin.plugins.coverage.rst
@@ -0,0 +1,29 @@
+mythril.laser.plugin.plugins.coverage package
+=============================================
+
+Submodules
+----------
+
+mythril.laser.plugin.plugins.coverage.coverage\_plugin module
+-------------------------------------------------------------
+
+.. automodule:: mythril.laser.plugin.plugins.coverage.coverage_plugin
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.plugin.plugins.coverage.coverage\_strategy module
+---------------------------------------------------------------
+
+.. automodule:: mythril.laser.plugin.plugins.coverage.coverage_strategy
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+Module contents
+---------------
+
+.. automodule:: mythril.laser.plugin.plugins.coverage
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.laser.plugin.plugins.rst b/docs/source/mythril.laser.plugin.plugins.rst
new file mode 100644
index 000000000..f291de8da
--- /dev/null
+++ b/docs/source/mythril.laser.plugin.plugins.rst
@@ -0,0 +1,70 @@
+mythril.laser.plugin.plugins package
+====================================
+
+Subpackages
+-----------
+
+.. toctree::
+   :maxdepth: 4
+
+   mythril.laser.plugin.plugins.coverage
+   mythril.laser.plugin.plugins.summary_backup
+
+Submodules
+----------
+
+mythril.laser.plugin.plugins.benchmark module
+---------------------------------------------
+
+.. automodule:: mythril.laser.plugin.plugins.benchmark
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.plugin.plugins.call\_depth\_limiter module
+--------------------------------------------------------
+
+.. automodule:: mythril.laser.plugin.plugins.call_depth_limiter
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.plugin.plugins.dependency\_pruner module
+------------------------------------------------------
+
+.. automodule:: mythril.laser.plugin.plugins.dependency_pruner
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.plugin.plugins.instruction\_profiler module
+---------------------------------------------------------
+
+.. automodule:: mythril.laser.plugin.plugins.instruction_profiler
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.plugin.plugins.mutation\_pruner module
+----------------------------------------------------
+
+.. automodule:: mythril.laser.plugin.plugins.mutation_pruner
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.plugin.plugins.plugin\_annotations module
+-------------------------------------------------------
+
+.. automodule:: mythril.laser.plugin.plugins.plugin_annotations
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+Module contents
+---------------
+
+.. automodule:: mythril.laser.plugin.plugins
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.laser.plugin.plugins.summary_backup.rst b/docs/source/mythril.laser.plugin.plugins.summary_backup.rst
new file mode 100644
index 000000000..134b486b5
--- /dev/null
+++ b/docs/source/mythril.laser.plugin.plugins.summary_backup.rst
@@ -0,0 +1,10 @@
+mythril.laser.plugin.plugins.summary\_backup package
+====================================================
+
+Module contents
+---------------
+
+.. automodule:: mythril.laser.plugin.plugins.summary_backup
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.laser.plugin.rst b/docs/source/mythril.laser.plugin.rst
new file mode 100644
index 000000000..8e32f4f54
--- /dev/null
+++ b/docs/source/mythril.laser.plugin.rst
@@ -0,0 +1,53 @@
+mythril.laser.plugin package
+============================
+
+Subpackages
+-----------
+
+.. toctree::
+   :maxdepth: 4
+
+   mythril.laser.plugin.plugins
+
+Submodules
+----------
+
+mythril.laser.plugin.builder module
+-----------------------------------
+
+.. automodule:: mythril.laser.plugin.builder
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.plugin.interface module
+-------------------------------------
+
+.. automodule:: mythril.laser.plugin.interface
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.plugin.loader module
+----------------------------------
+
+.. automodule:: mythril.laser.plugin.loader
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.plugin.signals module
+-----------------------------------
+
+.. automodule:: mythril.laser.plugin.signals
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+Module contents
+---------------
+
+.. automodule:: mythril.laser.plugin
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.laser.rst b/docs/source/mythril.laser.rst
index cbe0b2a55..4e5d397a9 100644
--- a/docs/source/mythril.laser.rst
+++ b/docs/source/mythril.laser.rst
@@ -5,14 +5,27 @@ Subpackages
 -----------
 
 .. toctree::
+   :maxdepth: 4
 
-    mythril.laser.ethereum
-    mythril.laser.smt
+   mythril.laser.ethereum
+   mythril.laser.plugin
+   mythril.laser.smt
+
+Submodules
+----------
+
+mythril.laser.execution\_info module
+------------------------------------
+
+.. automodule:: mythril.laser.execution_info
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril.laser
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.laser.smt.rst b/docs/source/mythril.laser.smt.rst
index 31e86e3e0..31abab710 100644
--- a/docs/source/mythril.laser.smt.rst
+++ b/docs/source/mythril.laser.smt.rst
@@ -1,38 +1,77 @@
 mythril.laser.smt package
 =========================
 
+Subpackages
+-----------
+
+.. toctree::
+   :maxdepth: 4
+
+   mythril.laser.smt.solver
+
 Submodules
 ----------
 
+mythril.laser.smt.array module
+------------------------------
+
+.. automodule:: mythril.laser.smt.array
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
 mythril.laser.smt.bitvec module
 -------------------------------
 
 .. automodule:: mythril.laser.smt.bitvec
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.smt.bitvec\_helper module
+---------------------------------------
+
+.. automodule:: mythril.laser.smt.bitvec_helper
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.smt.bool module
 -----------------------------
 
 .. automodule:: mythril.laser.smt.bool
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.laser.smt.expression module
 -----------------------------------
 
 .. automodule:: mythril.laser.smt.expression
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.smt.function module
+---------------------------------
+
+.. automodule:: mythril.laser.smt.function
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.smt.model module
+------------------------------
 
+.. automodule:: mythril.laser.smt.model
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril.laser.smt
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.laser.smt.solver.rst b/docs/source/mythril.laser.smt.solver.rst
new file mode 100644
index 000000000..b328f4b39
--- /dev/null
+++ b/docs/source/mythril.laser.smt.solver.rst
@@ -0,0 +1,37 @@
+mythril.laser.smt.solver package
+================================
+
+Submodules
+----------
+
+mythril.laser.smt.solver.independence\_solver module
+----------------------------------------------------
+
+.. automodule:: mythril.laser.smt.solver.independence_solver
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.smt.solver.solver module
+--------------------------------------
+
+.. automodule:: mythril.laser.smt.solver.solver
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.laser.smt.solver.solver\_statistics module
+--------------------------------------------------
+
+.. automodule:: mythril.laser.smt.solver.solver_statistics
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+Module contents
+---------------
+
+.. automodule:: mythril.laser.smt.solver
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.mythril.rst b/docs/source/mythril.mythril.rst
new file mode 100644
index 000000000..abcbf0a93
--- /dev/null
+++ b/docs/source/mythril.mythril.rst
@@ -0,0 +1,37 @@
+mythril.mythril package
+=======================
+
+Submodules
+----------
+
+mythril.mythril.mythril\_analyzer module
+----------------------------------------
+
+.. automodule:: mythril.mythril.mythril_analyzer
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.mythril.mythril\_config module
+--------------------------------------
+
+.. automodule:: mythril.mythril.mythril_config
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.mythril.mythril\_disassembler module
+--------------------------------------------
+
+.. automodule:: mythril.mythril.mythril_disassembler
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+Module contents
+---------------
+
+.. automodule:: mythril.mythril
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.plugin.rst b/docs/source/mythril.plugin.rst
new file mode 100644
index 000000000..323f1ccb6
--- /dev/null
+++ b/docs/source/mythril.plugin.rst
@@ -0,0 +1,37 @@
+mythril.plugin package
+======================
+
+Submodules
+----------
+
+mythril.plugin.discovery module
+-------------------------------
+
+.. automodule:: mythril.plugin.discovery
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.plugin.interface module
+-------------------------------
+
+.. automodule:: mythril.plugin.interface
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.plugin.loader module
+----------------------------
+
+.. automodule:: mythril.plugin.loader
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+Module contents
+---------------
+
+.. automodule:: mythril.plugin
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.rst b/docs/source/mythril.rst
index ca3d14ed7..e30a3779d 100644
--- a/docs/source/mythril.rst
+++ b/docs/source/mythril.rst
@@ -1,18 +1,22 @@
-Mythril Package
+mythril package
 ===============
 
 Subpackages
 -----------
 
 .. toctree::
-
-    mythril.analysis
-    mythril.disassembler
-    mythril.ethereum
-    mythril.interfaces
-    mythril.laser
-    mythril.solidity
-    mythril.support
+   :maxdepth: 4
+
+   mythril.analysis
+   mythril.concolic
+   mythril.disassembler
+   mythril.ethereum
+   mythril.interfaces
+   mythril.laser
+   mythril.mythril
+   mythril.plugin
+   mythril.solidity
+   mythril.support
 
 Submodules
 ----------
@@ -21,31 +25,14 @@ mythril.exceptions module
 -------------------------
 
 .. automodule:: mythril.exceptions
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.mythril module
-----------------------
-
-.. automodule:: mythril.mythril
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
-mythril.version module
-----------------------
-
-.. automodule:: mythril.version
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.solidity.rst b/docs/source/mythril.solidity.rst
index d5080892a..d13d33da4 100644
--- a/docs/source/mythril.solidity.rst
+++ b/docs/source/mythril.solidity.rst
@@ -8,15 +8,14 @@ mythril.solidity.soliditycontract module
 ----------------------------------------
 
 .. automodule:: mythril.solidity.soliditycontract
-    :members:
-    :undoc-members:
-    :show-inheritance:
-
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril.solidity
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/mythril.support.rst b/docs/source/mythril.support.rst
index 94e6e009f..ed23b9506 100644
--- a/docs/source/mythril.support.rst
+++ b/docs/source/mythril.support.rst
@@ -8,39 +8,78 @@ mythril.support.loader module
 -----------------------------
 
 .. automodule:: mythril.support.loader
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.support.lock module
+---------------------------
+
+.. automodule:: mythril.support.lock
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.support.model module
+----------------------------
+
+.. automodule:: mythril.support.model
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.support.opcodes module
+------------------------------
+
+.. automodule:: mythril.support.opcodes
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 mythril.support.signatures module
 ---------------------------------
 
 .. automodule:: mythril.support.signatures
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
-mythril.support.support\_utils module
--------------------------------------
+mythril.support.source\_support module
+--------------------------------------
 
-.. automodule:: mythril.support.support_utils
-    :members:
-    :undoc-members:
-    :show-inheritance:
+.. automodule:: mythril.support.source_support
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
-mythril.support.truffle module
-------------------------------
+mythril.support.start\_time module
+----------------------------------
+
+.. automodule:: mythril.support.start_time
+   :members:
+   :undoc-members:
+   :show-inheritance:
+
+mythril.support.support\_args module
+------------------------------------
 
-.. automodule:: mythril.support.truffle
-    :members:
-    :undoc-members:
-    :show-inheritance:
+.. automodule:: mythril.support.support_args
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
+mythril.support.support\_utils module
+-------------------------------------
+
+.. automodule:: mythril.support.support_utils
+   :members:
+   :undoc-members:
+   :show-inheritance:
 
 Module contents
 ---------------
 
 .. automodule:: mythril.support
-    :members:
-    :undoc-members:
-    :show-inheritance:
+   :members:
+   :undoc-members:
+   :show-inheritance:
diff --git a/docs/source/tutorial.rst b/docs/source/tutorial.rst
new file mode 100644
index 000000000..f73ae2a24
--- /dev/null
+++ b/docs/source/tutorial.rst
@@ -0,0 +1,511 @@
+Tutorial
+======================
+
+******************************************
+Executing Mythril on Simple Contracts
+******************************************
+
+We consider a contract simple if it does not have any imports, like the following contract:
+
+   .. code-block:: solidity
+
+        contract Exceptions {
+
+            uint256[8] myarray;
+            uint counter = 0;
+            function assert1() public pure {
+                uint256 i = 1;
+                assert(i == 0);
+            }
+            function counter_increase() public {
+                counter+=1;
+            }
+            function assert5(uint input_x) public view{
+                require(counter>2);
+                assert(input_x > 10);
+            }
+            function assert2() public pure {
+                uint256 i = 1;
+                assert(i > 0);
+            }
+
+            function assert3(uint256 input) public pure {
+                assert(input != 23);
+            }
+
+            function require_is_fine(uint256 input) public pure {
+                require(input != 23);
+            }
+
+            function this_is_fine(uint256 input) public pure {
+                if (input > 0) {
+                    uint256 i = 1/input;
+                }
+            }
+
+            function this_is_find_2(uint256 index) public view {
+                if (index < 8) {
+                    uint256 i = myarray[index];
+                }
+            }
+
+        }
+
+We can execute such a contract by directly using the following command:
+
+    .. code-block:: bash
+
+        $ myth analyze <file_path>
+
+This execution can give the following output:
+
+    .. code-block:: none
+
+        ==== Exception State ====
+        SWC ID: 110
+        Severity: Medium
+        Contract: Exceptions
+        Function name: assert1()
+        PC address: 708
+        Estimated Gas Usage: 207 - 492
+        An assertion violation was triggered.
+        It is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).
+        --------------------
+        In file: solidity_examples/exceptions.sol:7
+
+        assert(i == 0)
+
+        --------------------
+        Initial State:
+
+        Account: [CREATOR], balance: 0x2, nonce:0, storage:{}
+        Account: [ATTACKER], balance: 0x0, nonce:0, storage:{}
+
+        Transaction Sequence:
+
+        Caller: [CREATOR], calldata: , value: 0x0
+        Caller: [ATTACKER], function: assert1(), txdata: 0xb34c3610, value: 0x0
+
+        ==== Exception State ====
+        SWC ID: 110
+        Severity: Medium
+        Contract: Exceptions
+        Function name: assert3(uint256)
+        PC address: 708
+        Estimated Gas Usage: 482 - 767
+        An assertion violation was triggered.
+        It is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).
+        --------------------
+        In file: solidity_examples/exceptions.sol:20
+
+        assert(input != 23)
+
+        --------------------
+        Initial State:
+
+        Account: [CREATOR], balance: 0x40207f9b0, nonce:0, storage:{}
+        Account: [ATTACKER], balance: 0x0, nonce:0, storage:{}
+
+        Transaction Sequence:
+
+        Caller: [CREATOR], calldata: , value: 0x0
+        Caller: [SOMEGUY], function: assert3(uint256), txdata: 0x546455b50000000000000000000000000000000000000000000000000000000000000017, value: 0x0
+
+
+We can observe that the function ``assert5(uint256)`` should have an assertion failure 
+with the assertion ``assert(input_x > 10)`` which is missing from our output. This can be attributed to
+Mythril's default configuration of running three transactions. We can increase the transaction count to 4
+using the ``-t <tx_count>``.
+
+.. code-block:: bash
+
+    $ myth analyze <file_path> -t 4
+
+This gives the following execution output:
+
+    .. code-block:: none
+
+        ==== Exception State ====
+        SWC ID: 110
+        Severity: Medium
+        Contract: Exceptions
+        Function name: assert1()
+        PC address: 731
+        Estimated Gas Usage: 207 - 492
+        An assertion violation was triggered.
+        It is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).
+        --------------------
+        In file: solidity_examples/exceptions.sol:7
+
+        assert(i == 0)
+
+        --------------------
+        Initial State:
+
+        Account: [CREATOR], balance: 0x2, nonce:0, storage:{}
+        Account: [ATTACKER], balance: 0x0, nonce:0, storage:{}
+
+        Transaction Sequence:
+
+        Caller: [CREATOR], calldata: , value: 0x0
+        Caller: [ATTACKER], function: assert1(), txdata: 0xb34c3610, value: 0x0
+
+        ==== Exception State ====
+        SWC ID: 110
+        Severity: Medium
+        Contract: Exceptions
+        Function name: assert3(uint256)
+        PC address: 731
+        Estimated Gas Usage: 504 - 789
+        An assertion violation was triggered.
+        It is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).
+        --------------------
+        In file: solidity_examples/exceptions.sol:22
+
+        assert(input != 23)
+
+        --------------------
+        Initial State:
+
+        Account: [CREATOR], balance: 0x3, nonce:0, storage:{}
+        Account: [ATTACKER], balance: 0x0, nonce:0, storage:{}
+
+        Transaction Sequence:
+
+        Caller: [CREATOR], calldata: , value: 0x0
+        Caller: [ATTACKER], function: assert3(uint256), txdata: 0x546455b50000000000000000000000000000000000000000000000000000000000000017, value: 0x0
+
+        ==== Exception State ====
+        SWC ID: 110
+        Severity: Medium
+        Contract: Exceptions
+        Function name: assert5(uint256)
+        PC address: 731
+        Estimated Gas Usage: 1302 - 1587
+        An assertion violation was triggered.
+        It is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).
+        --------------------
+        In file: solidity_examples/exceptions.sol:14
+
+        assert(input_x > 10)
+
+        --------------------
+        Initial State:
+
+        Account: [CREATOR], balance: 0x20000000, nonce:0, storage:{}
+        Account: [ATTACKER], balance: 0x1000000, nonce:0, storage:{}
+
+        Transaction Sequence:
+
+        Caller: [CREATOR], calldata: , value: 0x0
+        Caller: [ATTACKER], function: counter_increase(), txdata: 0xe47b0253, value: 0x0
+        Caller: [CREATOR], function: counter_increase(), txdata: 0xe47b0253, value: 0x0
+        Caller: [CREATOR], function: counter_increase(), txdata: 0xe47b0253, value: 0x0
+        Caller: [ATTACKER], function: assert5(uint256), txdata: 0x1d5d53dd0000000000000000000000000000000000000000000000000000000000000003, value: 0x0
+
+
+For the violation in the 4th transaction, the input value should be less than 10. The transaction data generated by Mythril for the
+4th transaction is ``0x1d5d53dd0000000000000000000000000000000000000000000000000000000000000003``, the first 4 bytes ``1d5d53dd``
+correspond to the function signature hence the input generated by Mythril is ``0000000000000000000000000000000000000000000000000000000000000003``
+in hex, which is 3. For automated resolution of the input try using a different output format such as JSON.
+
+    .. code-block:: bash
+
+        $ myth analyze <file_path> -o json
+
+This leads to the following output:
+
+    .. code-block:: json
+
+        {
+            "error": null,
+            "issues": [{
+                "address": 731,
+                "code": "assert(i == 0)",
+                "contract": "Exceptions",
+                "description": "An assertion violation was triggered.\nIt is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).",
+                "filename": "solidity_examples/exceptions.sol",
+                "function": "assert1()",
+                "lineno": 7,
+                "max_gas_used": 492,
+                "min_gas_used": 207,
+                "severity": "Medium",
+                "sourceMap": ":::i",
+                "swc-id": "110",
+                "title": "Exception State",
+                "tx_sequence": {
+                    "initialState": {
+                        "accounts": {
+                            "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe": {
+                                "balance": "0x2",
+                                "code": "",
+                                "nonce": 0,
+                                "storage": "{}"
+                            },
+                            "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef": {
+                                "balance": "0x0",
+                                "code": "",
+                                "nonce": 0,
+                                "storage": "{}"
+                            }
+                        }
+                    },
+                    "steps": [{
+                        "address": "",
+                        "calldata": "",
+                        "input": "0x6080604052600060085534801561001557600080fd5b506103f7806100256000396000f3fe608060405234801561001057600080fd5b50600436106100885760003560e01c8063b34c36101161005b578063b34c3610146100fd578063b630d70614610107578063e47b025314610123578063f44f13d81461012d57610088565b806301d4277c1461008d5780631d5d53dd146100a9578063546455b5146100c557806378375f14146100e1575b600080fd5b6100a760048036038101906100a29190610251565b610137565b005b6100c360048036038101906100be9190610251565b61015e565b005b6100df60048036038101906100da9190610251565b610181565b005b6100fb60048036038101906100f69190610251565b610196565b005b6101056101a7565b005b610121600480360381019061011c9190610251565b6101c1565b005b61012b6101e0565b005b6101356101fc565b005b600881101561015b5760008082600881106101555761015461027e565b5b01549050505b50565b60026008541161016d57600080fd5b600a811161017e5761017d6102ad565b5b50565b6017811415610193576101926102ad565b5b50565b60178114156101a457600080fd5b50565b600060019050600081146101be576101bd6102ad565b5b50565b60008111156101dd5760008160016101d9919061033a565b9050505b50565b6001600860008282546101f3919061036b565b92505081905550565b60006001905060008111610213576102126102ad565b5b50565b600080fd5b6000819050919050565b61022e8161021b565b811461023957600080fd5b50565b60008135905061024b81610225565b92915050565b60006020828403121561026757610266610216565b5b60006102758482850161023c565b91505092915050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052603260045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052600160045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601260045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b60006103458261021b565b91506103508361021b565b9250826103605761035f6102dc565b5b828204905092915050565b60006103768261021b565b91506103818361021b565b9250827fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff038211156103b6576103b561030b565b5b82820190509291505056fea2646970667358221220b474c01fa60d997027e1ceb779bcb2b34b6752282e0ea3a038a08b889fe0163f64736f6c634300080c0033",
+                        "name": "unknown",
+                        "origin": "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe",
+                        "value": "0x0"
+                    }, {
+                        "address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
+                        "calldata": "0xb34c3610",
+                        "input": "0xb34c3610",
+                        "name": "assert1()",
+                        "origin": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef",
+                        "resolved_input": null,
+                        "value": "0x0"
+                    }]
+                }
+            }, {
+                "address": 731,
+                "code": "assert(input != 23)",
+                "contract": "Exceptions",
+                "description": "An assertion violation was triggered.\nIt is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).",
+                "filename": "solidity_examples/exceptions.sol",
+                "function": "assert3(uint256)",
+                "lineno": 22,
+                "max_gas_used": 789,
+                "min_gas_used": 504,
+                "severity": "Medium",
+                "sourceMap": ":::i",
+                "swc-id": "110",
+                "title": "Exception State",
+                "tx_sequence": {
+                    "initialState": {
+                        "accounts": {
+                            "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe": {
+                                "balance": "0x3",
+                                "code": "",
+                                "nonce": 0,
+                                "storage": "{}"
+                            },
+                            "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef": {
+                                "balance": "0x0",
+                                "code": "",
+                                "nonce": 0,
+                                "storage": "{}"
+                            }
+                        }
+                    },
+                    "steps": [{
+                        "address": "",
+                        "calldata": "",
+                        "input": "0x6080604052600060085534801561001557600080fd5b506103f7806100256000396000f3fe608060405234801561001057600080fd5b50600436106100885760003560e01c8063b34c36101161005b578063b34c3610146100fd578063b630d70614610107578063e47b025314610123578063f44f13d81461012d57610088565b806301d4277c1461008d5780631d5d53dd146100a9578063546455b5146100c557806378375f14146100e1575b600080fd5b6100a760048036038101906100a29190610251565b610137565b005b6100c360048036038101906100be9190610251565b61015e565b005b6100df60048036038101906100da9190610251565b610181565b005b6100fb60048036038101906100f69190610251565b610196565b005b6101056101a7565b005b610121600480360381019061011c9190610251565b6101c1565b005b61012b6101e0565b005b6101356101fc565b005b600881101561015b5760008082600881106101555761015461027e565b5b01549050505b50565b60026008541161016d57600080fd5b600a811161017e5761017d6102ad565b5b50565b6017811415610193576101926102ad565b5b50565b60178114156101a457600080fd5b50565b600060019050600081146101be576101bd6102ad565b5b50565b60008111156101dd5760008160016101d9919061033a565b9050505b50565b6001600860008282546101f3919061036b565b92505081905550565b60006001905060008111610213576102126102ad565b5b50565b600080fd5b6000819050919050565b61022e8161021b565b811461023957600080fd5b50565b60008135905061024b81610225565b92915050565b60006020828403121561026757610266610216565b5b60006102758482850161023c565b91505092915050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052603260045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052600160045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601260045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b60006103458261021b565b91506103508361021b565b9250826103605761035f6102dc565b5b828204905092915050565b60006103768261021b565b91506103818361021b565b9250827fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff038211156103b6576103b561030b565b5b82820190509291505056fea2646970667358221220b474c01fa60d997027e1ceb779bcb2b34b6752282e0ea3a038a08b889fe0163f64736f6c634300080c0033",
+                        "name": "unknown",
+                        "origin": "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe",
+                        "value": "0x0"
+                    }, {
+                        "address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
+                        "calldata": "0x546455b50000000000000000000000000000000000000000000000000000000000000017",
+                        "input": "0x546455b50000000000000000000000000000000000000000000000000000000000000017",
+                        "name": "assert3(uint256)",
+                        "origin": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef",
+                        "resolved_input": [23],
+                        "value": "0x0"
+                    }]
+                }
+            }, {
+                "address": 731,
+                "code": "assert(input_x > 10)",
+                "contract": "Exceptions",
+                "description": "An assertion violation was triggered.\nIt is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).",
+                "filename": "solidity_examples/exceptions.sol",
+                "function": "assert5(uint256)",
+                "lineno": 14,
+                "max_gas_used": 1587,
+                "min_gas_used": 1302,
+                "severity": "Medium",
+                "sourceMap": ":::i",
+                "swc-id": "110",
+                "title": "Exception State",
+                "tx_sequence": {
+                    "initialState": {
+                        "accounts": {
+                            "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe": {
+                                "balance": "0x0",
+                                "code": "",
+                                "nonce": 0,
+                                "storage": "{}"
+                            },
+                            "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef": {
+                                "balance": "0x0",
+                                "code": "",
+                                "nonce": 0,
+                                "storage": "{}"
+                            }
+                        }
+                    },
+                    "steps": [{
+                        "address": "",
+                        "calldata": "",
+                        "input": "0x6080604052600060085534801561001557600080fd5b506103f7806100256000396000f3fe608060405234801561001057600080fd5b50600436106100885760003560e01c8063b34c36101161005b578063b34c3610146100fd578063b630d70614610107578063e47b025314610123578063f44f13d81461012d57610088565b806301d4277c1461008d5780631d5d53dd146100a9578063546455b5146100c557806378375f14146100e1575b600080fd5b6100a760048036038101906100a29190610251565b610137565b005b6100c360048036038101906100be9190610251565b61015e565b005b6100df60048036038101906100da9190610251565b610181565b005b6100fb60048036038101906100f69190610251565b610196565b005b6101056101a7565b005b610121600480360381019061011c9190610251565b6101c1565b005b61012b6101e0565b005b6101356101fc565b005b600881101561015b5760008082600881106101555761015461027e565b5b01549050505b50565b60026008541161016d57600080fd5b600a811161017e5761017d6102ad565b5b50565b6017811415610193576101926102ad565b5b50565b60178114156101a457600080fd5b50565b600060019050600081146101be576101bd6102ad565b5b50565b60008111156101dd5760008160016101d9919061033a565b9050505b50565b6001600860008282546101f3919061036b565b92505081905550565b60006001905060008111610213576102126102ad565b5b50565b600080fd5b6000819050919050565b61022e8161021b565b811461023957600080fd5b50565b60008135905061024b81610225565b92915050565b60006020828403121561026757610266610216565b5b60006102758482850161023c565b91505092915050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052603260045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052600160045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601260045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b60006103458261021b565b91506103508361021b565b9250826103605761035f6102dc565b5b828204905092915050565b60006103768261021b565b91506103818361021b565b9250827fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff038211156103b6576103b561030b565b5b82820190509291505056fea2646970667358221220b474c01fa60d997027e1ceb779bcb2b34b6752282e0ea3a038a08b889fe0163f64736f6c634300080c0033",
+                        "name": "unknown",
+                        "origin": "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe",
+                        "value": "0x0"
+                    }, {
+                        "address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
+                        "calldata": "0xe47b0253",
+                        "input": "0xe47b0253",
+                        "name": "counter_increase()",
+                        "origin": "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe",
+                        "resolved_input": null,
+                        "value": "0x0"
+                    }, {
+                        "address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
+                        "calldata": "0xe47b0253",
+                        "input": "0xe47b0253",
+                        "name": "counter_increase()",
+                        "origin": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef",
+                        "resolved_input": null,
+                        "value": "0x0"
+                    }, {
+                        "address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
+                        "calldata": "0xe47b0253",
+                        "input": "0xe47b0253",
+                        "name": "counter_increase()",
+                        "origin": "0xaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa",
+                        "resolved_input": null,
+                        "value": "0x0"
+                    }, {
+                        "address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
+                        "calldata": "0x1d5d53dd0000000000000000000000000000000000000000000000000000000000000003",
+                        "input": "0x1d5d53dd0000000000000000000000000000000000000000000000000000000000000003",
+                        "name": "assert5(uint256)",
+                        "origin": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef",
+                        "resolved_input": [3],
+                        "value": "0x0"
+                    }]
+                }
+            }],
+            "success": true
+        }
+
+We can observe that the "resolved_input" field for the final transaction resolves to ``[3]``. Although this resolution
+fails in some circumstances where output generated by Mythril is although executable on the bytecode, it cannot be decoded due 
+to not being a valid ABI.
+
+There are interesting options such as ``--execution-timeout <seconds>`` and ``--solver-timeout <milliseconds>`` 
+which can be increased for better results. The default execution-timeout and solver-timeout are 86400 seconds and
+25000 milliseconds respectively.
+
+
+
+
+
+********************************************************
+Executing Mythril on Contracts with Imports
+********************************************************
+
+Consider the following contract:
+
+    .. code-block:: solidity
+
+        import "@openzeppelin/contracts/token/PRC20/PRC20.sol";
+
+        contract Nothing is PRC20{
+            string x_0 = "";
+
+            bytes3 x_1 = "A";
+
+            bytes5 x_2 = "E";
+
+            bytes5 x_3 = "";
+
+            bytes3 x_4 = "I";
+
+            bytes3 x_5 = "U";
+
+            bytes3 x_6 = "O";
+
+            bytes3 x_7 = "0";
+
+            bytes3 x_8 = "U";
+
+            bytes3 x_9 = "U";
+            function stringCompare(string memory a, string memory b) internal pure returns (bool) {
+                if(bytes(a).length != bytes(b).length) {
+                    return false;
+                } else {
+                    return keccak256(bytes(a)) == keccak256(bytes(b));
+                }
+            }
+
+            function nothing(string memory g_0, bytes3 g_1, bytes5 g_2, bytes5 g_3, bytes3 g_4, bytes3 g_5, bytes3 g_6, bytes3 g_7, bytes3 g_8, bytes3 g_9, bytes3 g_10, bytes3 g_11) public view returns (bool){
+                if (!stringCompare(g_0, x_0)) return false;
+                        
+                if (g_1 != x_1) return false;
+                        
+                if (g_2 != x_2) return false;
+                        
+                if (g_3 != x_3) return false;
+                        
+                if (g_4 != x_4) return false;
+                        
+                if (g_5 != x_5) return false;
+                        
+                if (g_6 != x_6) return false;
+                        
+                if (g_7 != x_7) return false;
+                        
+                if (g_8 != x_8) return false;
+                        
+                if (g_9 != x_9) return false;
+                
+                if (g_10 != x_9) return false;
+
+                if (g_11 != x_9) return false;
+
+                return true;
+
+            }
+        }
+
+
+When this contract is directly executed, by using the following command:
+
+    .. code-block:: bash
+
+        $ myth analyze <file_path>
+
+We encounter the following error:
+
+    .. code-block:: none
+
+        mythril.interfaces.cli [ERROR]: Solc experienced a fatal error.
+
+        ParserError: Source "@openzeppelin/contracts/token/PRC20/PRC20.sol" not found: File not found. Searched the following locations: "".
+        --> <file_path>:1:1:
+        |
+        1 | import "@openzeppelin/contracts/token/PRC20/PRC20.sol";
+        | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+This is because Mythril uses Solidity to compile the program, to circumvent this issue we can use the following solc-json file:
+
+    .. code-block:: json
+
+        {
+        "remappings": [ "@openzeppelin/contracts/token/PRC20/=node_modules/PRC20" ],
+        }
+
+Here we are mapping the import ``@openzeppelin/contracts/token/PRC20/`` to the path which contains ``PRC20.sol`` which in this case
+is ``node_modules/PRC20``. This instructs the compiler to search for anything with the prefix ``@openzeppelin/contracts/token/PRC20/` `
+in the path ``node_modules/PRC20`` in our file system. We feed to file to Mythril using ``--solc-json`` argument.
+
+    .. code-block:: bash
+
+        $ myth analyze {file_path} --solc-json {json_file_path}
+
+
+This can effectively execute the file since the Solidity compiler can locate `PRC20.sol`. For more information on remappings, you can
+refer to `Solc docs <https://docs.soliditylang.org/en/v0.8.14/using-the-compiler.html#base-path-and-import-remapping>`_.
\ No newline at end of file
diff --git a/docs/source/wiki.rst b/docs/source/wiki.rst
deleted file mode 100644
index e69de29bb..000000000
diff --git a/mythril/analysis/module/base.py b/mythril/analysis/module/base.py
index cf1b77cfd..a39de8214 100644
--- a/mythril/analysis/module/base.py
+++ b/mythril/analysis/module/base.py
@@ -34,13 +34,14 @@ class DetectionModule(ABC):
     All custom-built detection modules must inherit from this class.
 
     There are several class properties that expose information about the detection modules
-    - name: The name of the detection module
-    - swc_id: The SWC ID associated with the weakness that the module detects
-    - description: A description of the detection module, and what it detects
-    - entry_point: Mythril can run callback style detection modules, or modules that search the statespace.
+
+    :param name: The name of the detection module
+    :param swc_id: The SWC ID associated with the weakness that the module detects
+    :param description: A description of the detection module, and what it detects
+    :param entry_point: Mythril can run callback style detection modules, or modules that search the statespace.
                 [IMPORTANT] POST entry points severely slow down the analysis, try to always use callback style modules
-    - pre_hooks: A list of instructions to hook the laser vm for (pre execution of the instruction)
-    - post_hooks: A list of instructions to hook the laser vm for (post execution of the instruction)
+    :param pre_hooks: A list of instructions to hook the laser vm for (pre execution of the instruction)
+    :param post_hooks: A list of instructions to hook the laser vm for (post execution of the instruction)
     """
 
     name = "Detection Module Name / Title"
@@ -62,7 +63,7 @@ def reset_module(self):
     def update_cache(self, issues=None):
         """
         Updates cache with param issues, updates against self.issues, if the param is None
-        - issues: The issues used to update the cache
+        :param issues: The issues used to update the cache
         """
         issues = issues or self.issues
         for issue in issues:
diff --git a/mythril/exceptions.py b/mythril/exceptions.py
index cb708213c..782c16892 100644
--- a/mythril/exceptions.py
+++ b/mythril/exceptions.py
@@ -20,6 +20,13 @@ class UnsatError(MythrilBaseException):
     pass
 
 
+class SolverTimeOutException(UnsatError):
+    """A Mythril exception denoting the unsatisfiability of a series of
+    constraints."""
+
+    pass
+
+
 class NoContractFoundError(MythrilBaseException):
     """A Mythril exception denoting that a given contract file was not
     found."""
diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py
index 7d625f8b3..bfa3182d4 100644
--- a/mythril/interfaces/cli.py
+++ b/mythril/interfaces/cli.py
@@ -403,6 +403,7 @@ def add_graph_commands(parser: ArgumentParser):
 def create_safe_functions_parser(parser: ArgumentParser):
     """
     The duplication exists between safe-functions and analyze as some of them have different default values.
+    :param parser: Parser
     """
     parser.add_argument(
         "solidity_files",
@@ -416,11 +417,12 @@ def create_safe_functions_parser(parser: ArgumentParser):
 
 
 def add_analysis_args(options):
-    """[summary]
+    """
     Adds arguments for analysis
-    Args:
-        options ([type]): [description]
+
+    :param options: Analysis Options
     """
+
     options.add_argument(
         "-m",
         "--modules",
@@ -509,9 +511,10 @@ def add_analysis_args(options):
         help="Don't attempt to retrieve contract code, variables and balances from the blockchain",
     )
     options.add_argument(
-        "--sparse-pruning",
-        action="store_true",
-        help="Checks for reachability after the end of tx. Recommended for short execution timeouts < 1 min",
+        "--pruning-factor",
+        type=float,
+        default=1,
+        help="Checks for reachability at the rate of <pruning-factor>. Where 1 means checks every execution",
     )
     options.add_argument(
         "--unconstrained-storage",
@@ -750,7 +753,7 @@ def execute_command(
 
     elif args.command == SAFE_FUNCTIONS_COMMAND:
         args.unconstrained_storage = True
-        args.sparse_pruning = False
+        args.pruning_factor = 1
         args.disable_dependency_pruning = True
         args.no_onchain_data = True
         function_analyzer = MythrilAnalyzer(
diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index 23211928a..1b6713888 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/mythril/laser/ethereum/state/constraints.py
@@ -1,6 +1,6 @@
 """This module contains the class used to represent state-change constraints in
 the call graph."""
-from mythril.exceptions import UnsatError
+from mythril.exceptions import UnsatError, SolverTimeOutException
 from mythril.laser.smt import symbol_factory, simplify, Bool
 from mythril.support.model import get_model
 from mythril.laser.ethereum.function_managers import keccak_function_manager
@@ -25,13 +25,19 @@ def __init__(self, constraint_list: Optional[List[Bool]] = None) -> None:
         constraint_list = self._get_smt_bool_list(constraint_list)
         super(Constraints, self).__init__(constraint_list)
 
-    @property
-    def is_possible(self) -> bool:
+    def is_possible(self, solver_timeout=None) -> bool:
         """
+        :param solver_timeout: The default timeout uses analysis timeout from args.solver_timeout
         :return: True/False based on the existence of solution of constraints
         """
         try:
-            get_model(self)
+            get_model(self, solver_timeout=solver_timeout)
+        except SolverTimeOutException:
+            # If it uses the long analysis solver timeout
+            if solver_timeout is None:
+                return False
+            # If it uses a short custom solver timeout
+            return True
         except UnsatError:
             return False
         return True
diff --git a/mythril/laser/ethereum/state/machine_state.py b/mythril/laser/ethereum/state/machine_state.py
index 927f0c95f..78b8880dd 100644
--- a/mythril/laser/ethereum/state/machine_state.py
+++ b/mythril/laser/ethereum/state/machine_state.py
@@ -32,6 +32,7 @@ def append(self, element: Union[int, Expression]) -> None:
         This function ensures the following properties when appending to a list:
             - Element appended to this list should be a BitVec
             - Ensures stack overflow bound
+
         :param element: element to be appended to the list
         :function: appends the element to list if the size is less than STACK_LIMIT, else throws an error
         """
diff --git a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py
index 751921bdb..604f84d93 100644
--- a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py
+++ b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py
@@ -135,7 +135,7 @@ def get_strategic_global_state(self) -> GlobalState:
             # TODO: There's probably a nicer way to do this
             if isinstance(
                 state.current_transaction, ContractCreationTransaction
-            ) and count < max(20, self.bound):
+            ) and count < max(128, self.bound):
                 return state
 
             elif count > self.bound:
diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 01b905cc5..3f8087327 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -3,6 +3,7 @@
 from collections import defaultdict
 from copy import copy
 from datetime import datetime, timedelta
+import random
 from typing import Callable, Dict, DefaultDict, List, Tuple, Optional
 
 from mythril.support.opcodes import OPCODES
@@ -218,7 +219,9 @@ def _execute_transactions(self, address):
             old_states_count = len(self.open_states)
             if self.use_reachability_check:
                 self.open_states = [
-                    state for state in self.open_states if state.constraints.is_possible
+                    state
+                    for state in self.open_states
+                    if state.constraints.is_possible()
                 ]
                 prune_count = old_states_count - len(self.open_states)
                 if prune_count:
@@ -282,11 +285,11 @@ def exec(self, create=False, track_gas=False) -> Optional[List[GlobalState]]:
             except NotImplementedError:
                 log.debug("Encountered unimplemented instruction")
                 continue
-            if args.sparse_pruning is False:
+            if len(new_states) > 1 and random.uniform(0, 1) < args.pruning_factor:
                 new_states = [
                     state
                     for state in new_states
-                    if state.world_state.constraints.is_possible
+                    if state.world_state.constraints.is_possible()
                 ]
 
             self.manage_cfg(op_code, new_states)  # TODO: What about op_code is None?
diff --git a/mythril/mythril/mythril_analyzer.py b/mythril/mythril/mythril_analyzer.py
index e886d77f3..f8da16892 100644
--- a/mythril/mythril/mythril_analyzer.py
+++ b/mythril/mythril/mythril_analyzer.py
@@ -60,7 +60,7 @@ def __init__(
             if cmd_args.custom_modules_directory
             else ""
         )
-        args.sparse_pruning = cmd_args.sparse_pruning
+        args.pruning_factor = cmd_args.pruning_factor
         args.solver_timeout = cmd_args.solver_timeout
         args.parallel_solving = cmd_args.parallel_solving
         args.unconstrained_storage = cmd_args.unconstrained_storage
diff --git a/mythril/mythril/mythril_disassembler.py b/mythril/mythril/mythril_disassembler.py
index fa31199e4..b0bb23cf5 100644
--- a/mythril/mythril/mythril_disassembler.py
+++ b/mythril/mythril/mythril_disassembler.py
@@ -26,7 +26,7 @@
 class MythrilDisassembler:
     """
     The Mythril Disassembler class
-    Responsible for generating disassembly of smart contracts
+    Responsible for generating disassembly of smart contracts:
         - Compiles solc code from file/onchain
         - Can also be used to access onchain storage data
     """
@@ -239,9 +239,8 @@ def get_state_variable_from_storage(
         """
         Get variables from the storage
         :param address: The contract address
-        :param params: The list of parameters
-                        param types: [position, length] or ["mapping", position, key1, key2, ...  ]
-                        or [position, length, array]
+        :param params: The list of parameters param types: [position, length] or ["mapping", position, key1, key2, ...  ]
+                       or [position, length, array]
         :return: The corresponding storage slot and its value
         """
         params = params or []
diff --git a/mythril/support/model.py b/mythril/support/model.py
index 77e224aa8..6997d90d4 100644
--- a/mythril/support/model.py
+++ b/mythril/support/model.py
@@ -5,7 +5,7 @@
 from mythril.support.support_args import args
 from mythril.laser.smt import Optimize
 from mythril.laser.ethereum.time_handler import time_handler
-from mythril.exceptions import UnsatError
+from mythril.exceptions import UnsatError, SolverTimeOutException
 import logging
 
 log = logging.getLogger(__name__)
@@ -13,7 +13,13 @@
 
 
 @lru_cache(maxsize=2**23)
-def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True):
+def get_model(
+    constraints,
+    minimize=(),
+    maximize=(),
+    enforce_execution_time=True,
+    solver_timeout=None,
+):
     """
     Returns a model based on given constraints as a tuple
     :param constraints: Tuple of constraints
@@ -23,7 +29,7 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True
     :return:
     """
     s = Optimize()
-    timeout = args.solver_timeout
+    timeout = solver_timeout or args.solver_timeout
     if enforce_execution_time:
         timeout = min(timeout, time_handler.time_remaining() - 500)
         if timeout <= 0:
@@ -60,4 +66,5 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True
         return s.model()
     elif result == unknown:
         log.debug("Timeout/Error encountered while solving expression using z3")
+        raise SolverTimeOutException
     raise UnsatError
diff --git a/mythril/support/support_args.py b/mythril/support/support_args.py
index 8734a36c6..10f20288c 100644
--- a/mythril/support/support_args.py
+++ b/mythril/support/support_args.py
@@ -10,7 +10,7 @@ class Args(object, metaclass=Singleton):
 
     def __init__(self):
         self.solver_timeout = 10000
-        self.sparse_pruning = True
+        self.pruning_factor = 1
         self.unconstrained_storage = False
         self.parallel_solving = False
         self.call_depth_limit = 3
diff --git a/requirements.txt b/requirements.txt
index 840a9b3d5..03036c068 100644
--- a/requirements.txt
+++ b/requirements.txt
@@ -16,6 +16,7 @@ eth-keys<0.4.0,>=0.2.1
 eth-rlp<0.3.0,>=0.1.0
 eth-typing<3.0.0,>=2.1.0
 eth-utils<2
+hexbytes<0.3.0
 jinja2>=2.9
 MarkupSafe<2.1.0
 mock


Test patch:
diff --git a/all_tests.sh b/all_tests.sh
index 7fd0ae819..f9b283e1f 100755
--- a/all_tests.sh
+++ b/all_tests.sh
@@ -7,11 +7,6 @@ assert sys.version_info[0:2] >= (3,5), \
 """Please make sure you are using Python 3.5 or later.
 You ran with {}""".format(sys.version)' || exit $?
 
-echo "Checking that truffle is installed..."
-if ! which truffle ; then
-    echo "Please make sure you have etherum truffle installed (npm install -g truffle)"
-    exit 2
-fi
 
 rm -rf ./tests/testdata/outputs_current/
 mkdir -p ./tests/testdata/outputs_current/
diff --git a/tests/graph_test.py b/tests/graph_test.py
index cb3d915eb..1beaa3cc3 100644
--- a/tests/graph_test.py
+++ b/tests/graph_test.py
@@ -25,7 +25,7 @@ def test_generate_graph():
             create_timeout=None,
             disable_dependency_pruning=False,
             custom_modules_directory=None,
-            sparse_pruning=True,
+            pruning_factor=0,
             parallel_solving=True,
             unconstrained_storage=True,
             call_depth_limit=3,
diff --git a/tests/mythril/mythril_analyzer_test.py b/tests/mythril/mythril_analyzer_test.py
index 63df5e9d6..456082312 100644
--- a/tests/mythril/mythril_analyzer_test.py
+++ b/tests/mythril/mythril_analyzer_test.py
@@ -32,7 +32,7 @@ def test_fire_lasers(mock_sym, mock_fire_lasers, mock_code_info):
         create_timeout=None,
         disable_dependency_pruning=False,
         custom_modules_directory=None,
-        sparse_pruning=True,
+        pruning_factor=0,
         parallel_solving=True,
         unconstrained_storage=True,
         call_depth_limit=3,
diff --git a/tests/statespace_test.py b/tests/statespace_test.py
index e83127438..c3db46350 100644
--- a/tests/statespace_test.py
+++ b/tests/statespace_test.py
@@ -22,7 +22,7 @@ def test_statespace_dump():
             create_timeout=None,
             disable_dependency_pruning=False,
             custom_modules_directory=None,
-            sparse_pruning=True,
+            pruning_factor=0,
             parallel_solving=True,
             unconstrained_storage=True,
             call_depth_limit=3,