diff --git a/docs/api.rst b/docs/api.rst
index c070986..659faf7 100644
--- a/docs/api.rst
+++ b/docs/api.rst
@@ -40,6 +40,10 @@ Models
 EVM
 ---
 .. automodule:: manticore.platforms.evm
+.. automodule:: manticore.seth
+    :members: 
+EVM Assembler
+---------
 .. autoclass:: manticore.platforms.evm::EVMAsm.Instruction
     :members: 
 .. autoclass:: manticore.platforms.evm.EVMAsm
diff --git a/examples/evm/coverage.py b/examples/evm/coverage.py
index 59b8cf1..6cb9761 100644
--- a/examples/evm/coverage.py
+++ b/examples/evm/coverage.py
@@ -1,4 +1,4 @@
-from seth import *
+from manticore.seth import ManticoreEVM
 
 seth = ManticoreEVM()
 seth.verbosity(3)
diff --git a/examples/evm/integer_overflow.py b/examples/evm/integer_overflow.py
index c65ed44..680edae 100644
--- a/examples/evm/integer_overflow.py
+++ b/examples/evm/integer_overflow.py
@@ -1,10 +1,9 @@
-from seth import *
+from manticore.seth import ManticoreEVM
 seth = ManticoreEVM()
 #And now make the contract account to analyze
 source_code = '''
 pragma solidity ^0.4.15;
 contract Overflow {
-    event Log(string);
     uint private sellerBalance=0;
     
     function add(uint value) returns (bool){
@@ -19,7 +18,7 @@ contract Overflow {
 user_account = seth.create_account(balance=1000)
 contract_account = seth.solidity_create_contract(source_code, owner=user_account, balance=0)
 
-#First add wont owerflow uint256 representation
+#First add won't overflow uint256 representation
 contract_account.add(seth.SValue)
 
 #Potential overflow
diff --git a/examples/evm/minimal.py b/examples/evm/minimal.py
index 99e1396..c4aca60 100644
--- a/examples/evm/minimal.py
+++ b/examples/evm/minimal.py
@@ -1,4 +1,4 @@
-from seth import ManticoreEVM
+from manticore.seth import ManticoreEVM
 ################ Script #######################
 
 seth = ManticoreEVM()
@@ -9,7 +9,7 @@ source_code = '''
 pragma solidity ^0.4.13;
 contract NoDistpatcher {
     event Log(string);
-    function address(){}
+
     function() payable {
         if (msg.data[0] == 'A') {
             Log("Got an A");
diff --git a/examples/evm/reentrancy_concrete.py b/examples/evm/reentrancy_concrete.py
index 7ea6e8c..edf0c0f 100644
--- a/examples/evm/reentrancy_concrete.py
+++ b/examples/evm/reentrancy_concrete.py
@@ -1,4 +1,4 @@
-from seth import ManticoreEVM
+from manticore.seth import ManticoreEVM, ABI
 ################ Script #######################
 
 seth = ManticoreEVM()
@@ -58,13 +58,13 @@ contract GenericReentranceExploit {
         reentry_reps = reps;
     }
 
-    function delegate(bytes data) payable{
+    function proxycall(bytes data) payable{
         // call addToBalance with msg.value ethers
         vulnerable_contract.call.value(msg.value)(data);
     }
 
     function get_money(){
-        suicide(owner);
+        selfdestruct(owner);
     }
 
     function () payable{
@@ -76,12 +76,6 @@ contract GenericReentranceExploit {
         }
     }
 }
-//Function signatures: 
-//0ccfac9e: delegate(bytes)
-//b8029269: get_money()
-//9d15fd17: set_reentry_attack_string(bytes)
-//0d4b1aca: set_reentry_reps(int256)
-//beac44e7: set_vulnerable_contract(address)
 '''
 
 
@@ -90,7 +84,7 @@ user_account = seth.create_account(balance=100000000000000000)
 attacker_account = seth.create_account(balance=100000000000000000)
 
 contract_account = seth.solidity_create_contract(contract_source_code, owner=user_account) #Not payable
-seth.world[int(contract_account)]['balance']=1000000000000000000  #give it some ether
+seth.world.set_balance(contract_account, 1000000000000000000)  #give it some ether
 
 exploit_account = seth.solidity_create_contract(exploit_source_code, owner=attacker_account)
 
@@ -102,7 +96,7 @@ exploit_account.set_reentry_reps(30)
 
 print "\t Setting attack string"
 #'\x9d\x15\xfd\x17'+pack_msb(32)+pack_msb(4)+'\x5f\xd8\xc7\x10',
-reentry_string = seth.make_function_id('withdrawBalance()')
+reentry_string = ABI.make_function_id('withdrawBalance()')
 exploit_account.set_reentry_attack_string(reentry_string)
 
 
@@ -119,10 +113,10 @@ contract_account.addToBalance(value=100000000000000000)
 
 
 print "[+] Let attacker deposit some small amount using exploit"
-exploit_account.delegate(seth.make_function_id('addToBalance()'), value=100000000000000000)
+exploit_account.proxycall(ABI.make_function_id('addToBalance()'), value=100000000000000000)
 
 print "[+] Let attacker extract all  using exploit" 
-exploit_account.delegate(seth.make_function_id('withdrawBalance()'))
+exploit_account.proxycall(ABI.make_function_id('withdrawBalance()'))
 
 print "[+] Let attacker destroy the exploit andprofit" 
 exploit_account.get_money()
diff --git a/examples/evm/reentrancy_symbolic.py b/examples/evm/reentrancy_symbolic.py
index 9d78f89..ee3b3b9 100644
--- a/examples/evm/reentrancy_symbolic.py
+++ b/examples/evm/reentrancy_symbolic.py
@@ -1,4 +1,4 @@
-from seth import ManticoreEVM
+from manticore.seth import ManticoreEVM
 ################ Script #######################
 
 seth = ManticoreEVM()
@@ -27,10 +27,6 @@ contract Reentrance {
         userBalance[msg.sender] = 0;
     }   
 }
-//Function signatures: 
-//c0e317fb: addToBalance()
-//f8b2cb4f: getBalance(address)
-//5fd8c710: withdrawBalance()
 '''
 
 exploit_source_code = '''
@@ -58,7 +54,7 @@ contract GenericReentranceExploit {
         reentry_reps = reps;
     }
 
-    function delegate(bytes data) payable{
+    function proxycall(bytes data) payable{
         // call addToBalance with msg.value ethers
         vulnerable_contract.call.value(msg.value)(data);
     }
@@ -76,12 +72,6 @@ contract GenericReentranceExploit {
         }
     }
 }
-//Function signatures: 
-//0ccfac9e: delegate(bytes)
-//b8029269: get_money()
-//9d15fd17: set_reentry_attack_string(bytes)
-//0d4b1aca: set_reentry_reps(int256)
-//beac44e7: set_vulnerable_contract(address)
 '''
 
 
@@ -115,10 +105,10 @@ exploit_account.set_reentry_attack_string(seth.SByte(4))
 
 #Attacker is
 print "[+] Attacker first transaction"
-exploit_account.delegate(seth.SByte(4), value=seth.SValue)
+exploit_account.proxycall(seth.SByte(4), value=seth.SValue)
 
 print "[+] Attacker second transaction" 
-exploit_account.delegate(seth.SByte(4))
+exploit_account.proxycall(seth.SByte(4))
 
 print "[+] The attacker destroys the exploit contract and profit" 
 exploit_account.get_money()
diff --git a/examples/evm/simple_functions.py b/examples/evm/simple_functions.py
index 264254c..bd678eb 100644
--- a/examples/evm/simple_functions.py
+++ b/examples/evm/simple_functions.py
@@ -1,4 +1,4 @@
-from seth import *
+from manticore.seth import ManticoreEVM
 ################ Script #######################
 
 seth = ManticoreEVM()
@@ -24,7 +24,6 @@ contract Test {
 user_account = seth.create_account(balance=1000)
 contract_account = seth.solidity_create_contract(source_code, owner=user_account)
 
-
 symbolic_data = seth.SByte(4) 
 symbolic_value = None 
 seth.transaction(  caller=user_account,
diff --git a/examples/evm/simple_mapping.py b/examples/evm/simple_mapping.py
index 3268360..78f14d9 100644
--- a/examples/evm/simple_mapping.py
+++ b/examples/evm/simple_mapping.py
@@ -1,4 +1,4 @@
-from seth import *
+from manticore.seth import ManticoreEVM
 ################ Script #######################
 
 seth = ManticoreEVM()
diff --git a/examples/evm/simple_transaction.py b/examples/evm/simple_transaction.py
index 33fc0ea..0957e2e 100644
--- a/examples/evm/simple_transaction.py
+++ b/examples/evm/simple_transaction.py
@@ -1,4 +1,4 @@
-from seth import *
+from manticore.seth import ManticoreEVM
 ################ Script #######################
 
 seth = ManticoreEVM()
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index df89774..bfd600a 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -699,7 +699,7 @@ class EVMAsm(object):
             mnemonic = name
             if name == 'PUSH':
                 mnemonic = '%s%d'%(name, (opcode&0x1f) + 1)
-            elif name in ('SWAP', 'LOG'):
+            elif name in ('SWAP', 'LOG', 'DUP'):
                 mnemonic = '%s%d'%(name, (opcode&0xf) + 1)
 
             reverse_table[mnemonic] = opcode, name, immediate_operand_size, pops, pushes, gas, description
@@ -732,7 +732,7 @@ class EVMAsm(object):
 
             return EVMAsm.Instruction(opcode, name, operand_size, pops, pushes, gas, description, operand=operand, offset=offset)
         except:
-            raise Exception("Something wron at offset %d"%offset)
+            raise Exception("Something wrong at offset %d"%offset)
 
     @staticmethod
     def assemble_all(assembler, offset=0):
@@ -1902,14 +1902,53 @@ class EVMWorld(Platform):
         else:
             return self._global_storage
 
-    @storage.setter
-    def storage(self, value):
-        if self.depth:
-            self.current.global_storage = value
-        else:
-            self._global_storage = value
+    def set_storage_data(self, address, offset, value):
+        self.storage[address]['storage'][offset] = value
 
-    def _push(self, vm):
+    def get_storage_data(self, address, offset):
+        return self.storage[address]['storage'].get(offset)
+
+    def set_balance(self, address, value):
+        self.storage[int(address)]['balance'] = value
+
+    def get_balance(self, address):
+        return self.storage[address]['balance']
+
+    def add_to_balance(self, address, value):
+        self.storage[address]['balance'] += value
+
+    def send_ether(self, src, dst, value):
+        src_balance = self.get_balance(src)
+        dst_balance = self.get_balance(dst)
+        #discarding absurd amount of ether
+        self.constraints.add(src_balance + value >= src_balance)
+
+        if issymbolic(src_balance) or issymbolic(value):
+            res = solver.get_all_values(self._constraints, src_balance < value)
+            if set(res) == set([True, False]): 
+                raise Concretize('Forking on available funds',
+                                 expression = src_balance < value,
+                                 setstate=lambda a,b: None,
+                                 policy='ALL')
+            if set(res) == set([True]):
+                self._pending_transaction = None
+                raise TerminateState("Not Enough Funds for transaction", testcase=True)
+        else:
+            if src_balance < value:
+                self._pending_transaction = None
+                raise TerminateState("Not Enough Funds for transaction", testcase=True)
+
+        self.storage[dst]['balance'] += value
+        self.storage[src]['balance'] -= value
+
+    def get_code(self, address):
+        return self.storage[address]['code']
+
+    def set_code(self, address, data):
+        self.storage[address]['code'] = data
+
+
+    def _push_vm(self, vm):
         #Storage address ->  account(value, local_storage)
         vm.global_storage = self.storage
         vm.global_storage[vm.address]['storage'] = copy.copy(self.storage[vm.address]['storage'])
@@ -1926,13 +1965,17 @@ class EVMWorld(Platform):
                 self._pop(rollback=True)
             raise TerminateState("Maximum call depth limit is reached", testcase=True)
 
-    def _pop(self, rollback=False):
+    def _pop_vm(self, rollback=False):
         vm = self._callstack.pop()
         assert self.constraints == vm.constraints
         if self.current:
             self.current.constraints = vm.constraints
         if not rollback:
-            self.storage = vm.global_storage
+            if self.depth:
+                self.current.global_storage = vm.global_storage
+            else:
+                self._global_storage = vm.global_storage
+
             self._deleted_address = self._deleted_address.union(vm.suicide)
             self._logs += vm.logs
             if not self.depth:
@@ -2073,14 +2116,14 @@ class EVMWorld(Platform):
             for i in range(len(data)):
                 data_symb[i] = Operators.ORD(data[i])
             data = data_symb
-        bytecode = self.storage[address]['code']
+        bytecode = self.get_code(address)
         self._pending_transaction = ('Call', address, origin, price, data, caller, value, bytecode, header)
 
         if run:
             assert self.depth == 0
             assert  not issymbolic(caller) 
             assert  not issymbolic(address) 
-            assert self.storage[caller]['balance'] >= value
+            assert self.get_balance(caller) >= value
             #run contract
             #Assert everything is concrete?
             try:
@@ -2095,34 +2138,10 @@ class EVMWorld(Platform):
         assert self.current is None or self.current.last_exception is not None
 
         ty, address, origin, price, data, caller, value, bytecode, header = self._pending_transaction
-
-
-        if issymbolic(self.storage[caller]['balance']) or issymbolic(value):
-            res = solver.get_all_values(self._constraints, self.storage[caller]['balance'] < value)
-            if set(res) == set([True, False]): 
-                raise Concretize('Forking on available funds',
-                                 expression = self.storage[caller]['balance'] < value,
-                                 setstate=lambda a,b: None,
-                                 policy='ALL')
-            if set(res) == set([True]): 
-                self._pending_transaction = None
-                raise TerminateState("Not Enough Funds for transaction", testcase=True)
-        else:
-            if self.storage[caller]['balance'] < value:
-                self._pending_transaction = None
-                raise TerminateState("Not Enough Funds for transaction", testcase=True)
-
-        self._pending_transaction = None
-
-        #discarding absurd amount of ether
-        self.constraints.add(self.storage[address]['balance'] + value >= self.storage[address]['balance'])
-
-        self.storage[caller]['balance'] -= value
-        self.storage[address]['balance'] += value
-
+        self.send_ether(caller, address, value)
+        self._pending_transaction=None
         new_vm = EVM(self._constraints, address, origin, price, data, caller, value, bytecode, header, global_storage=self.storage)
-        
-        self._push(new_vm)
+        self._push_vm(new_vm)
         if self.depth == 1:
             #handle human transactions
             if ty == 'Create':
@@ -2137,14 +2156,14 @@ class EVMWorld(Platform):
         caller = self.current.address
         price = self.current.price
         depth = self.depth + 1
-        bytecode = self.storage[to]['code']
+        bytecode = self.get_code(to)
         header = {'timestamp' :1}
         self.transaction(address, origin, price, data, caller, value, header)
         self._process_pending_transaction()
 
 
     def RETURN(self, data):
-        prev_vm = self._pop() #current VM changed!
+        prev_vm = self._pop_vm() #current VM changed!
         if self.depth == 0:
             self.last_return=data
             self.last_pc = prev_vm.pc
@@ -2157,8 +2176,7 @@ class EVMWorld(Platform):
 
         if isinstance(last_ex, Create):
             self.current._push(prev_vm.address)
-            self.storage[prev_vm.address]['code'] = data
-
+            self.set_code(prev_vm.address, data)
         else:
             size = min(last_ex.out_size, len(data))
             self.current.write_buffer(last_ex.out_offset, data[:size])
@@ -2167,7 +2185,7 @@ class EVMWorld(Platform):
         self.current.pc += self.current.instruction.size
 
     def STOP(self):
-        prev_vm = self._pop(rollback=False)
+        prev_vm = self._pop_vm(rollback=False)
         if self.depth == 0:
             self.last_pc = prev_vm.pc
             raise TerminateState("STOP", testcase=True)
@@ -2178,7 +2196,7 @@ class EVMWorld(Platform):
         self.current.pc += self.current.instruction.size
 
     def THROW(self):
-        prev_vm = self._pop(rollback=True)
+        prev_vm = self._pop_vm(rollback=True)
         #revert balance on CALL fail
         self.storage[prev_vm.caller]['balance'] += prev_vm.value
         self.storage[prev_vm.address]['balance'] -= prev_vm.value
@@ -2193,7 +2211,7 @@ class EVMWorld(Platform):
         self.current.pc += self.current.instruction.size
 
     def REVERT(self, data):
-        prev_vm = self._pop(rollback=True)
+        prev_vm = self._pop_vm(rollback=True)
         #revert balance on CALL fail
         self.storage[prev_vm.caller]['balance'] += prev_vm.value
         self.storage[prev_vm.address]['balance'] -= prev_vm.value
@@ -2216,7 +2234,7 @@ class EVMWorld(Platform):
         self.storage[recipient]['balance'] += self.storage[address]['balance']
         self.storage[address]['balance'] = 0
         self.suicide.add(address)
-        prev_vm = self._pop(rollback=False)
+        prev_vm = self._pop_vm(rollback=False)
         if self.depth == 0:
             self.last_pc = prev_vm.pc
             raise TerminateState("SELFDESTRUCT", testcase=True)
diff --git a/examples/evm/seth.py b/manticore/seth.py
similarity index 59%
rename from examples/evm/seth.py
rename to manticore/seth.py
index 2c0c9fc..d4421e6 100644
--- a/examples/evm/seth.py
+++ b/manticore/seth.py
@@ -1,97 +1,52 @@
-from manticore import Manticore
-from manticore.core.smtlib import ConstraintSet, Operators, solver, issymbolic, Array, Expression, Constant
-from manticore.core.smtlib.visitors import arithmetic_simplifier
-from manticore.platforms import evm
-from manticore.core.state import State
+from . import Manticore
+from .core.smtlib import ConstraintSet, Operators, solver, issymbolic, Array, Expression, Constant
+from .core.smtlib.visitors import arithmetic_simplifier
+from .platforms import evm
+from .core.state import State
 import tempfile
 from subprocess import Popen, PIPE
 import sha3
 import json
+import StringIO
 
 
-class EVMContract(object):
+class ABI(object):
+    '''
+        This class contains methods to handle the ABI.
+        The Application Binary Interface is the standard way to interact with
+        contracts in the Ethereum ecosystem, both from outside the blockchain 
+        and for contract-to-contract interaction. 
 
-    def __init__(self, address, seth=None, default_caller=None):
-        self._default_caller = default_caller
-        self._seth=seth
-        self._address=address
-        self._hashes = {}
-        self._caller = None
-        self._value = 0
-
-        name, source_code, init_bytecode, metadata, metadata_runtime, hashes = self._seth.context['seth']['metadata'][address]
-        for signature in hashes.keys():
-            func_name = str(signature.split('(')[0])
-            self._hashes[func_name] = signature, hashes[signature]
-
-    def __int__(self):
-        return self._address
-
-    @property
-    def address(self):
-        return self._address
-
-    def value(self, value):
-        self._value = value
-        return self
-
-    def caller(self, caller):
-        self._caller = caller
-        return self
-
-    def __getattribute__(self, name):
-        if not name.startswith('_') and name in self._hashes.keys():
-            def f(*args, **kwargs):
-                caller = kwargs.get('caller', self._caller)
-                value = kwargs.get('value', self._value)
-                tx_data = self._seth.make_function_call(str(self._hashes[name][0]),*args)
-                if caller is not None:
-                    caller = int(caller)
-                else:
-                    caller = self._default_caller
-                self._seth.transaction(caller=caller,
-                                        address=self._address,
-                                        value=value,
-                                        data=tx_data
-                                     )
-                self._caller = None
-                self._value = 0
-            return f
-        else:
-            return object.__getattribute__(self, name)            
-
-class ManticoreEVM(Manticore):
+    '''
     class SByte():
+        ''' Unconstrained symbolic byte, not asociated with any constraint set '''
         def __init__(self, size=1):
             self.size=size
         def __mul__(self, reps):
             return Symbol(self.size*reps)
+
     SCHAR = SByte(1)
     SUINT = SByte(32)
     SValue = None
-        
-
-    @staticmethod
-    def pack_msb(value):
-        return ''.join(ManticoreEVM.serialize_uint(value))
 
     @staticmethod
     def serialize(value):
+        ''' Translates a python object to its EVM ABI serialization.
+            It supports s '''
         if isinstance(value, (str,tuple)):
-            return ManticoreEVM.serialize_string(value)
+            return ABI.serialize_string(value)
         if isinstance(value, (list)):
-            return ManticoreEVM.serialize_array(value)
+            return ABI.serialize_array(value)
         if isinstance(value, (int, long)):
-            return ManticoreEVM.serialize_uint(value)
-        if isinstance(value, ManticoreEVM.SByte):
-            return ManticoreEVM.serialize_uint(value.size) + (None,)*value.size + (('\x00',)*(32-(value.size%32)))
+            return ABI.serialize_uint(value)
+        if isinstance(value, ABI.SByte):
+            return ABI.serialize_uint(value.size) + (None,)*value.size + (('\x00',)*(32-(value.size%32)))
         if value is None:
             return (None,)*32
 
-
     @staticmethod
     def serialize_uint(value, size=32):
-        '''takes an int and packs it into a 32 byte string, msb first''' 
+        '''Translates a python int into a 32 byte string, msb first''' 
         assert size >=1
         bytes = []
         for position in range(size):
@@ -101,15 +56,16 @@ class ManticoreEVM(Manticore):
 
     @staticmethod
     def serialize_string(value):
+        '''Translates a string or a tuple of chars its EVM ABI serialization''' 
         assert isinstance(value, (str,tuple))
-        return ManticoreEVM.serialize_uint(len(value)) + tuple(value) + tuple('\x00'*(32-(len(value)%32)))
+        return ABI.serialize_uint(len(value)) + tuple(value) + tuple('\x00'*(32-(len(value)%32)))
 
     @staticmethod
     def serialize_array(value):
         assert isinstance(value, list)
-        serialized = [ManticoreEVM.serialize_uint(len(value))]
+        serialized = [ABI.serialize_uint(len(value))]
         for item in value:
-            serialized.append(ManticoreEVM.serialize(item))    
+            serialized.append(ABI.serialize(item))    
         return reduce(lambda x,y: x+y, serialized)
 
     @staticmethod
@@ -125,20 +81,20 @@ class ManticoreEVM(Manticore):
             return () 
         args = list(args)
         for i in range(len(args)):
-            if isinstance(args[i], EVMContract):
+            if isinstance(args[i], EVMAccount):
                  args[i] = int(args[i])
         result = []
         dynamic_args = []
         dynamic_offset = 32*len(args)
         for arg in args:
             if isinstance(arg, (list, tuple, str, ManticoreEVM.SByte)):
-                result.append(ManticoreEVM.serialize(dynamic_offset))
-                serialized_arg = ManticoreEVM.serialize(arg)
+                result.append(ABI.serialize(dynamic_offset))
+                serialized_arg = ABI.serialize(arg)
                 dynamic_args.append(serialized_arg)
                 assert len(serialized_arg)%32 ==0
                 dynamic_offset += len(serialized_arg)
             else:
-                result.append(ManticoreEVM.serialize(arg))
+                result.append(ABI.serialize(arg))
 
         for arg in dynamic_args:
             result.append(arg)
@@ -147,20 +103,114 @@ class ManticoreEVM(Manticore):
         
     @staticmethod
     def make_function_call(method_name, *args):
-        function_id = ManticoreEVM.make_function_id(method_name)
+        function_id = ABI.make_function_id(method_name)
         def check_bitsize(value, size):
             if isinstance(value, BitVec):
                 return value.size==size
             return (value & ~((1<<size)-1)) == 0
         assert len(function_id) == 4
         result = [tuple(function_id)]
-        result.append(ManticoreEVM.make_function_arguments(*args))
+        result.append(ABI.make_function_arguments(*args))
         return reduce(lambda x,y: x+y, result)
 
+
+class EVMAccount(object):
+    ''' An EVM account '''
+    def __init__(self, address, seth=None, default_caller=None):
+        ''' Encapsulates an account. 
+
+            :param address: the address of this account
+            :type address: 160 bit long integer
+            :param seth: the controlling manticore
+            :param default_caller: the default caller address for any transaction
+
+        '''
+        self._default_caller = default_caller
+        self._seth=seth
+        self._address=address
+        self._hashes = {}
+
+        if self._seth:
+            name, source_code, init_bytecode, metadata, metadata_runtime, hashes = self._seth.context['seth']['metadata'][address]
+            for signature in hashes.keys():
+                func_name = str(signature.split('(')[0])
+                self._hashes[func_name] = signature, hashes[signature]
+
+    def __int__(self):
+        return self._address
+
+    def __getattribute__(self, name):
+        ''' If this is a contract account of which we know the functions hashes
+            this will build the transaction for the function call.
+
+            Example use::
+        
+                #call funtion `add` on contract_account with argument `1000`
+                contract_account.add(1000)
+         
+        '''
+        if not name.startswith('_') and name in self._hashes.keys():
+            def f(*args, **kwargs):
+                caller = kwargs.get('caller', None)
+                value = kwargs.get('value', 0)
+                tx_data = ABI.make_function_call(str(self._hashes[name][0]), *args)
+                if caller is not None:
+                    caller = int(caller)
+                else:
+                    caller = self._default_caller
+                self._seth.transaction(caller=caller,
+                                        address=self._address,
+                                        value=value,
+                                        data=tx_data
+                                     )
+                self._caller = None
+                self._value = 0
+            return f
+        else:
+            return object.__getattribute__(self, name)            
+
+
+
+class ManticoreEVM(Manticore):
+    ''' Manticore EVM manager
+    
+        Usage Ex::
+
+            from manticore.seth import ManticoreEVM, ABI
+            seth = ManticoreEVM()
+            #And now make the contract account to analyze
+            source_code = """
+                pragma solidity ^0.4.15;
+                contract AnInt {
+                    uint private i=0;                    
+                    function set(uint value){
+                        i=value
+                    } 
+                }
+            """
+            #Initialize user and contracts
+            user_account = seth.create_account(balance=1000)
+            contract_account = seth.solidity_create_contract(source_code, owner=user_account, balance=0)
+            contract_account.set(12345, value=100) 
+
+            seth.report()
+            print seth.coverage(contract_account)
+    '''
+    SByte=ABI.SByte
+    SValue=ABI.SValue
+
+
     @staticmethod
     def compile(source_code):
-        """
-        Compile a solidity source code
+        name, source_code, bytecode, srcmap, srcmap_runtime, hashes = ManticoreEVM._compile(source_code)
+        return bytecode
+
+    @staticmethod
+    def _compile(source_code):
+        """ Compile a solidity contract, used internally
+            
+            :param source_code: a solidity source code
+            :return: name, source_code, bytecode, srcmap, srcmap_runtime, hashes
         """
         solc = "solc"
         with tempfile.NamedTemporaryFile() as temp:
@@ -178,7 +228,6 @@ class ManticoreEVM(Manticore):
             return name, source_code, bytecode, srcmap, srcmap_runtime, hashes
 
     def __init__(self):
-
         #Make the constraint store
         constraints = ConstraintSet()
         #make the ethereum world state
@@ -196,22 +245,22 @@ class ManticoreEVM(Manticore):
         self.context['seth']['_saved_states'] = []
         self.context['seth']['_final_states'] = []
 
-        self._executor.subscribe('did_load_state', self.load_state_callback)
-        self._executor.subscribe('will_terminate_state', self.terminate_state_callback)
-        self._executor.subscribe('will_execute_instruction', self.will_execute_instruction_callback)
-        self._executor.subscribe('did_execute_instruction', self.did_execute_instruction_callback)
-        self._executor.subscribe('did_read_code', self.did_read_code)
-        self._executor.subscribe('on_symbolic_sha3', self.symbolic_sha3)
-        self._executor.subscribe('on_concrete_sha3', self.concrete_sha3)
+        self._executor.subscribe('did_load_state', self._load_state_callback)
+        self._executor.subscribe('will_terminate_state', self._terminate_state_callback)
+        self._executor.subscribe('will_execute_instruction', self._will_execute_instruction_callback)
+        self._executor.subscribe('did_execute_instruction', self._did_execute_instruction_callback)
+        self._executor.subscribe('did_read_code', self._did_read_code)
+        self._executor.subscribe('on_symbolic_sha3', self._symbolic_sha3)
+        self._executor.subscribe('on_concrete_sha3', self._concrete_sha3)
 
     @property
     def world(self):
-        if self.initial_state is None:
-            return None
-        return self.initial_state.platform
+        ''' The world instance or None if there is more than one state '''  
+        return self.get_world(None)
 
     @property
     def running_state_ids(self):
+        ''' IDs of the running states''' 
         with self.locked_context('seth') as context:
             if self.initial_state is not None:
                 return context['_saved_states'] + [-1]
@@ -220,29 +269,69 @@ class ManticoreEVM(Manticore):
 
     @property
     def final_state_ids(self):
+        ''' IDs of the terminated states ''' 
         with self.locked_context('seth') as context:
             return context['_final_states']
 
-    def get_world(self, state_id=-1):
-        if state_id == -1:
-            return self.initial_state.platform
+    def get_world(self, state_id=None):
+        ''' Returns the evm world of `state_id` state. '''
+        state = self.load(state_id)
+        if state is None:
+            return None
+        else:
+            return state.platform
 
-        state = self._executor._workspace.load_state(state_id, delete=False)
-        return state.platform
-
-    def get_balance(self, address):
-        if isinstance(address, EVMContract):
+    def get_balance(self, address, state_id=None):
+        ''' Balance for account `address` on state `state_id` '''
+        if isinstance(address, EVMAccount):
             address = int(address)
-        return self.get_world().storage[address]['balance']
+        return self.get_world(state_id).storage[address]['balance']
+
+    def get_storage(self, address, offset, state_id=None):
+        ''' Storage data for `offset` on account `address` on state `state_id` '''
+        if isinstance(address, EVMAccount):
+            address = int(address)
+        return self.get_world(state_id).storage[address]['storage'].get(offset)
+
+    def last_return(self, state_id=None):
+        ''' last returned buffer for state `state_id` '''
+        state = self.load(state_id)
+        return state.world.last_return
 
     def solidity_create_contract(self, source_code, owner, balance=0, address=None, args=()):
-        name, source_code, init_bytecode, metadata, metadata_runtime, hashes = self.compile(source_code)
-        address = self.create_contract(owner=owner, address=address, balance=balance, init=tuple(init_bytecode)+tuple(ManticoreEVM.make_function_arguments(*args)))
+        ''' Creates a solidity contract 
+
+            :param source_code: solidity source code
+            :type source_code: str
+            :param owner: owner account (will be default caller in any transactions)
+            :type owner: int or EVMAccount
+            :param balance: balance to be transfered on creation
+            :type balance: int or SValue
+            :param address: the address for the new contract (optional)
+            :type address: int or EVMAccount
+            :param args: constructor arguments
+            :type args: tuple
+            :return: an EVMAccount
+        '''
+
+        name, source_code, init_bytecode, metadata, metadata_runtime, hashes = self._compile(source_code)
+        address = self.create_contract(owner=owner, address=address, balance=balance, init=tuple(init_bytecode)+tuple(ABI.make_function_arguments(*args)))
         self.context['seth']['metadata'][address] = name, source_code, init_bytecode, metadata, metadata_runtime, hashes
-        return EVMContract(address, self, default_caller=owner)
+        return EVMAccount(address, self, default_caller=owner)
 
     def create_contract(self, owner, balance=0, init=None, address=None):
-        ''' Only available when there is a single state of the world'''
+        ''' Creates a contract 
+
+            :param init: initializing evm bytecode and arguments
+            :type init: str
+            :param owner: owner account (will be default caller in any transactions)
+            :type owner: int or EVMAccount
+            :param balance: balance to be transfered on creation
+            :type balance: int or SValue
+            :param address: the address for the new contract (optional)
+            :type address: int or EVMAccount
+            :return: an EVMAccount
+        '''
         with self.locked_context('seth') as context:
             assert context['_pending_transaction'] is None
         assert init is not None
@@ -255,15 +344,32 @@ class ManticoreEVM(Manticore):
         return address
 
     def create_account(self, balance=0, address=None, code=''):
-        ''' Only available when there is a single state of the world'''
+        ''' Creates a normal account
+
+            :param balance: balance to be transfered on creation
+            :type balance: int or SValue
+            :param address: the address for the new contract (optional)
+            :type address: int or EVMAccount
+            :return: an EVMAccount
+        '''
         with self.locked_context('seth') as context:
            assert context['_pending_transaction'] is None
         return self.world.create_account( address, balance, code=code, storage=None)
 
     def transaction(self, caller, address, value, data):
-        if isinstance(address, EVMContract):
+        ''' Issue a transaction 
+
+            :param caller: the address of the account sending the transaction
+            :type caller: int or EVMAccount
+            :param value: balance to be transfered on creation
+            :type value: int or SValue
+            :param address: the address of the contract to call
+            :type address: int or EVMAccount
+            :return: an EVMAccount
+        '''
+        if isinstance(address, EVMAccount):
             address = int(address)
-        if isinstance(caller, EVMContract):
+        if isinstance(caller, EVMAccount):
             caller = int(caller)
 
 
@@ -274,6 +380,8 @@ class ManticoreEVM(Manticore):
         return self.run(procs=10)
 
     def run(self, **kwargs):
+        ''' Run any pending transaction on any running state '''
+
         #Check if there is a pending transaction
         with self.locked_context('seth') as context:
             assert context['_pending_transaction'] is not None
@@ -302,6 +410,13 @@ class ManticoreEVM(Manticore):
         return result
           
     def save(self, state, final=False):
+        ''' Save a state in secondary storage and add it to running or final lists
+
+            :param state: A manticore State
+            :param final: True if state is final
+            :returns: a state id
+
+        '''
         #save the state to secondary storage
         state_id = self._executor._workspace.save_state(state)
 
@@ -314,8 +429,33 @@ class ManticoreEVM(Manticore):
                 context['_saved_states'].append(state_id)
         return state_id
 
+    def load(self, state_id=None):
+        ''' Load one of the running or final states.
+            
+            :param state_id: If None it assumes there is a single running state
+            :type state_id: int or None
+        '''
+        state = None
+        if state_id is None:
+            #a single state was assumed
+            if len(self.running_state_ids) == 1:  
+                #Get the ID of the single running state              
+                state_id = self.running_state_ids[0]
+                if state_id != -1:
+                    #if there is a single running state with id != 1. We consider it is a new initial_state
+                    assert self.initial_state is None
+                    state = self.initial_state = self._executor._workspace.load_state(state_id, delete=True)
+            else:
+                raise Exception("More than one state running. Do not know which to choose.")
+        if state_id == -1:
+            state = self.initial_state
+        else:
+            state = self._executor._workspace.load_state(state_id, delete=False)
+
+        return state
+
     #Callbacks
-    def terminate_state_callback(self, state, state_id, e):
+    def _terminate_state_callback(self, state, state_id, e):
         ''' INTERNAL USE 
             Every time a state finishes executing last transaction we save it in
             our private list 
@@ -339,7 +479,7 @@ class ManticoreEVM(Manticore):
 
 
     #Callbacks
-    def load_state_callback(self, state, state_id):
+    def _load_state_callback(self, state, state_id):
         ''' INTERNAL USE 
             When a state was just loaded from stoage we do the pending transaction
         '''
@@ -370,31 +510,28 @@ class ManticoreEVM(Manticore):
             assert ty == 'CREATE_CONTRACT'
             world.create_contract(caller=caller, address=address, balance=value, init=data)
 
-    def will_execute_instruction_callback(self, state, pc, instruction):
+    def _will_execute_instruction_callback(self, state, pc, instruction):
+        ''' INTERNAL USE '''
         assert state.constraints == state.platform.constraints
         assert state.platform.constraints == state.platform.current.constraints
 
         with self.locked_context('coverage', set) as coverage:
             coverage.add((state.platform.current.address, state.platform.current.pc))
 
-    def did_execute_instruction_callback(self, state, prev_pc, pc, instruction):
+    def _did_execute_instruction_callback(self, state, prev_pc, pc, instruction):
+        ''' INTERNAL USE '''
         state.context.setdefault('seth.trace',[]).append((state.platform.current.address, pc))
 
-    def did_read_code(self, state, offset, size):
+    def _did_read_code(self, state, offset, size):
+        ''' INTERNAL USE '''
         with self.locked_context('code_data', set) as code_data:
             for i in range(offset, offset+size):
                 code_data.add((state.platform.current.address, i))
 
+    def report(self, state_id=None, ty=None):
+        ''' Prints a small report on state id '''
+        output = StringIO.StringIO()
 
-    def last_return(self, state_id=-1):
-        if state_id == -1:
-            state = self.initial_state
-        else:
-            state = self._executor._workspace.load_state(state_id, delete=False)
-        return state.world.last_return
-
-
-    def report(self, state_id, ty=None):
         def compare_buffers(a, b):
             if len(a) != len(b):
                 return False
@@ -405,21 +542,18 @@ class ManticoreEVM(Manticore):
                     return False
             return cond
 
-        if state_id == -1:
-            state = self.initial_state
-        else:
-            state = self._executor._workspace.load_state(state_id, delete=False)
-
+        state = self.load(state_id)
         world = state.platform
         trace = state.context['seth.trace']
-        last_pc = trace[-1][1]
-        last_address = trace[-1][0]
+        last_address, last_pc = trace[-1]
+        
+        #Try to recover metadata from solidity based contracts
         try:
-            md_name, md_source_code, md_init_bytecode, md_metadata, md_metadata_runtime, md_hashes= self.context['seth']['metadata'][last_address]
+            md_name, md_source_code, md_init_bytecode, md_metadata, md_metadata_runtime, md_hashes = self.context['seth']['metadata'][last_address]
         except:
             md_name, md_source_code, md_init_bytecode, md_metadata, md_metadata_runtime, md_hashes = None,None,None,None,None,None 
 
-
+        # try to get the runtime bytecode from the account
         try:
             runtime_bytecode = world.storage[last_address]['code']
         except:
@@ -429,8 +563,8 @@ class ManticoreEVM(Manticore):
         if ty is not None:
             if str(e) != ty:
                 return
-        print "="*20
-        print "REPORT:", e, 
+
+        output.write("REPORT:" + str(e)) 
 
         try:
             # Magic number comes from here:
@@ -449,16 +583,16 @@ class ManticoreEVM(Manticore):
 
             beg, size = map(int, source_pos.split(':'))
 
-            print " at:"
+            output.write( " at:" )
             nl = md_source_code.count('\n')
             snippet = md_source_code[beg:beg+size]
             for l in snippet.split('\n'):
-                print '    ',nl,'  ', l
+                output.write('    %s  %s\n'%(nl, l))
                 nl+=1
         except:
-            print
+            output.write('\n')
 
-        print "BALANCES"
+        output.write("BALANCES\n")
         for address, account in world.storage.items():
             if isinstance(account['balance'], Constant):
                 account['balance'] = account['balance'].value
@@ -466,38 +600,38 @@ class ManticoreEVM(Manticore):
             if issymbolic(account['balance']):
                 m, M = solver.minmax(world.constraints, arithmetic_simplifier(account['balance']))
                 if m == M:
-                    print "\t", hex(address), M
+                    output.write('\t%x %r\n'%(address, M))
                 else:
-                    print "\t", hex(address), "range:[%x, %x]"%(m,M)                
+                    output.write('\t%x range:[%x, %x]\n'%(address, m, M))
             else:
-                print "\t", hex(address), account['balance'],"wei"
+                output.write('\t%x %d wei\n'%(address, account['balance']))
 
         if state.platform.logs:
-            print "LOGS:"
-        for address, memlog, topics in state.platform.logs:
-            try:
-                res = memlog
-                if isinstance(memlog, Expression):
-                    res = state.solve_one(memlog)
-                    if isinstance(memlog, Array):
-                        state.constrain(compare_buffers(memlog, res))
-                    else:
-                        state.constrain(memlog== res)
+            output.write('LOGS:\n')
+            for address, memlog, topics in state.platform.logs:
+                try:
+                    res = memlog
+                    if isinstance(memlog, Expression):
+                        res = state.solve_one(memlog)
+                        if isinstance(memlog, Array):
+                            state.constrain(compare_buffers(memlog, res))
+                        else:
+                            state.constrain(memlog== res)
 
-                res1 = address
-                if isinstance(address, Expression):
-                    res = state.solve_one(address)
-                    if isinstance(address, Array):
-                        state.constrain(compare_buffers(address, res))
-                    else:
-                        state.constrain(address == res)
+                    res1 = address
+                    if isinstance(address, Expression):
+                        res = state.solve_one(address)
+                        if isinstance(address, Array):
+                            state.constrain(compare_buffers(address, res))
+                        else:
+                            state.constrain(address == res)
 
-                print  "\t %s: %r %s" %( hex(res1), ''.join(map(chr,res)), topics)
-            except Exception,e:
-                print e
-                print  "\t", address,  repr(memlog), topics
+                    output.write('\t %s: %r %s\n' %( hex(res1), ''.join(map(chr,res)), topics))
+                except Exception,e:
+                    print e
+                    output.write('\t %r %r %r\n' % (address,  repr(memlog), topics))
 
-        print "INPUT SYMBOLS"
+        output.write('INPUT SYMBOLS\n')
         for expr in state.input_symbols:
             res = state.solve_one(expr)
             if isinstance(expr, Array):
@@ -506,9 +640,9 @@ class ManticoreEVM(Manticore):
                 state.constrain(expr== res)
    
             try:
-                print "\t %s: %s"%( expr.name, res.encode('hex'))
+                output.write('\t %s: %s\n'%( expr.name, res.encode('hex')))
             except:
-                print "\t", expr.name+':',  res
+                output.write('\t %s: %s'% (expr.name, res))
         
         #print "Constraints:"
         #print state.constraints
@@ -545,47 +679,42 @@ class ManticoreEVM(Manticore):
                     size = int('0x'+data[dyn_offset:dyn_offset+64],16)
                     return data[dyn_offset+64:dyn_offset+64+size*2],offset+8
                 else:
-                    print "<",ty,">"
-                    raise NotImplemented
+                    raise NotImplemented(ty)
 
-            print "TRANSACTION ", tx_num, '-', ty
+            output.write('TRANSACTION %d - %s' % (tx_num, ty))
             try:
                 md_name, md_source_code, md_init_bytecode, md_metadata, md_metadata_runtime, md_hashes= self.context['seth']['metadata'][address]
             except:
                 md_name, md_source_code, md_init_bytecode, md_metadata, md_metadata_runtime, md_hashes = None,None,None,None,None,None 
 
 
-            print '\t From: 0x%x'%x(caller)
-            print '\t To: 0x%x'%x(address)
-            print '\t Value: %d wei'%x(value)
+            output.write('\t From: 0x%x\n'% x(caller) )
+            output.write('\t To: 0x%x\n'%x(address))
+            output.write('\t Value: %d wei\n'%x(value))
             xdata = x(data).encode('hex')
-            print '\t Data:', xdata
+            output.write('\t Data: %s\n'% xdata)
             if ty == 'CALL':
-                print '\t Function: ', 
                 done = False
-                rhashes = dict((hsh, signature) for signature, hsh in md_hashes.iteritems())
                 try:
+                    rhashes = dict((hsh, signature) for signature, hsh in md_hashes.iteritems())
                     signature = rhashes.get(xdata[:8], '{fallback}()')
                     done = True
                     func_name = signature.split('(')[0]
-                    print func_name,'(',
+                    output.write('\t Function: %s(' % func_name)
                     types = signature.split('(')[1][:-1].split(',')
                     off = 8
                     for ty in types:
                         if off != 8:
                             print ',',
                         val, off = consume_type(ty, xdata, off)
-                        print val,
-                    print ')'
+                        output.write('%s'%val)
+                    output.write(')\n')
                 except Exception,e:
-                    print e, xdata   
-
-        
-        
-            
-
+                    output.write('%s %s\n'%(e, xdata))
+        return output.getvalue()
 
     def coverage(self, account_address):
+        ''' Output a code coverage report for contract account_address '''
         account_address = int(account_address)
         #This will just pick one of the running states.
         #This assumes the code and the accounts are the same in all versions of the world
@@ -613,7 +742,7 @@ class ManticoreEVM(Manticore):
         offset = 0
         count = 0
         total = 0
-        for i in evm.EVMDecoder.decode_all(runtime_bytecode[:end]) :
+        for i in evm.EVMAsm.disassemble_all(runtime_bytecode[:end]) :
             
             if (account_address, offset) in seen:
                 output += bcolors.OKGREEN
@@ -629,16 +758,16 @@ class ManticoreEVM(Manticore):
         output += "Total assembler lines: %d\n"% total
         output += "Total assembler lines visited: %d\n"% count
         output += "Coverage: %2.2f%%\n"%  (count*100.0/total)
-
-
         return output
 
+    def _symbolic_sha3(self, state, data, known_hashes):
+        ''' INTERNAL USE '''
 
-    def symbolic_sha3(self, state, data, known_hashes):
         with self.locked_context('known_sha3', set) as known_sha3:
             state.platform._sha3.update(known_sha3)
 
-    def concrete_sha3(self, state, buf, value):
+    def _concrete_sha3(self, state, buf, value):
+        ''' INTERNAL USE '''
         with self.locked_context('known_sha3', set) as known_sha3:
             known_sha3.add((buf,value))