diff --git a/examples/evm/coverage.py b/examples/evm/coverage.py
index 31722c7..dc2c122 100644
--- a/examples/evm/coverage.py
+++ b/examples/evm/coverage.py
@@ -1,38 +1,38 @@
 from manticore.seth import ManticoreEVM
 
-seth = ManticoreEVM()
-seth.verbosity(3)
+m = ManticoreEVM()
+m.verbosity(3)
 #And now make the contract account to analyze
 source_code = file('coverage.sol').read()
 
-user_account = seth.create_account(balance=1000)
+user_account = m.create_account(balance=1000)
 
-bytecode = seth.compile(source_code)
+bytecode = m.compile(source_code)
 #Initialize contract
-contract_account = seth.create_contract(owner=user_account, 
+contract_account = m.create_contract(owner=user_account, 
                                           balance=0, 
                                           init=bytecode)
 
-seth.transaction(  caller=user_account,
+m.transaction(  caller=user_account,
                     address=contract_account,
                     value=None,
-                    data=seth.SByte(164),
+                    data=m.SByte(164),
                  )
 
 #Up to here we get only ~30% coverage. 
 #We need 2 transactions to fully explore the contract
-seth.transaction(  caller=user_account,
+m.transaction(  caller=user_account,
                     address=contract_account,
                     value=None,
-                    data=seth.SByte(164),
+                    data=m.SByte(164),
                  )
 
-print "[+] There are %d reverted states now"% len(seth.final_state_ids)
-print "[+] There are %d alive states now"% len(seth.running_state_ids)
-for state_id in seth.running_state_ids:
-    print seth.report(state_id)
+print "[+] There are %d reverted states now"% len(m.final_state_ids)
+print "[+] There are %d alive states now"% len(m.running_state_ids)
+for state_id in m.running_state_ids:
+    print m.report(state_id)
 
 print "[+] Global coverage: %x"% contract_account
-print seth.coverage(contract_account)
+print m.coverage(contract_account)
 
 
diff --git a/examples/evm/integer_overflow.py b/examples/evm/integer_overflow.py
index b3ff1ce..b1e477a 100644
--- a/examples/evm/integer_overflow.py
+++ b/examples/evm/integer_overflow.py
@@ -1,39 +1,37 @@
-from manticore.seth import ManticoreEVM
-seth = ManticoreEVM()
+from manticore.seth import ManticoreEVM, IntegerOverflow
+m = ManticoreEVM()
+m.register_detector(IntegerOverflow())
+
 #And now make the contract account to analyze
 source_code = '''
 pragma solidity ^0.4.15;
 contract Overflow {
     uint private sellerBalance=0;
     
-    function add(uint value) returns (bool){
+    function add(uint value) returns (uint){
         sellerBalance += value; // complicated math with possible overflow
 
         // possible auditor assert
         assert(sellerBalance >= value); 
+        return sellerBalance;
     } 
 }
 '''
 #Initialize user and contracts
-user_account = seth.create_account(balance=1000)
-contract_account = seth.solidity_create_contract(source_code, owner=user_account, balance=0)
+user_account = m.create_account(balance=1000)
+contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0)
 
 #First add won't overflow uint256 representation
-contract_account.add(seth.SValue)
+contract_account.add(m.make_symbolic_value())
 
 #Potential overflow
-contract_account.add(seth.SValue)
+contract_account.add(m.make_symbolic_value())
+
+#Let seth know we are not sending more transactions so it can output 
+# info about running states and global statistics
+m.finalize()
+print "[+] Look for results in %s"% m.workspace
 
 
-print "[+] There are %d reverted states now"% len(seth.final_state_ids)
-for state_id in seth.final_state_ids:
-    print seth.report(state_id)
-
-print "[+] There are %d alive states now"% len(seth.running_state_ids)
-for state_id in seth.running_state_ids:
-    print seth.report(state_id)
-
-print "[+] Global coverage: %x"% contract_account
-print seth.coverage(contract_account)
 
 
diff --git a/examples/evm/minimal.py b/examples/evm/minimal.py
index 7cfa02d..1170339 100644
--- a/examples/evm/minimal.py
+++ b/examples/evm/minimal.py
@@ -1,7 +1,7 @@
 from manticore.seth import ManticoreEVM
 ################ Script #######################
 
-seth = ManticoreEVM()
+m = ManticoreEVM()
 #And now make the contract account to analyze
 # cat  | solc --bin 
 source_code = '''
@@ -20,31 +20,22 @@ contract NoDistpatcher {
 }
 '''
 
-print "[+] Creating a user account"
-user_account = seth.create_account(balance=1000)
-
-
-print "[+] Creating a contract account"
-contract_account = seth.solidity_create_contract(source_code, owner=user_account)
+user_account = m.create_account(balance=1000)
+print "[+] Creating a user account", user_account
 
+contract_account = m.solidity_create_contract(source_code, owner=user_account)
+print "[+] Creating a contract account", contract_account
+print "[+] Source code:"
+print source_code
 
 print "[+] Now the symbolic values"
-
-symbolic_data = seth.SByte(320) 
+symbolic_data = m.make_symbolic_buffer(320) 
 symbolic_value = None 
-seth.transaction(caller=user_account,
+m.transaction(caller=user_account,
                 address=contract_account,
                 data=symbolic_data,
                 value=symbolic_value )
 
-print "[+] There are %d reverted states now"% len(seth.final_state_ids)
-
-print "[+] There are %d alive states now"% len(seth.running_state_ids)
-for state_id in seth.running_state_ids:
-    print seth.report(state_id)
-
-print "[+] Global coverage:"
-print seth.coverage(contract_account)
-
-
-
+#Let seth know we are not sending more transactions 
+m.finalize()
+print "[+] Look for results in %s"% m.workspace
diff --git a/examples/evm/reentrancy_concrete.py b/examples/evm/reentrancy_concrete.py
index 92f004d..c4a9b74 100644
--- a/examples/evm/reentrancy_concrete.py
+++ b/examples/evm/reentrancy_concrete.py
@@ -1,8 +1,8 @@
 from manticore.seth import ManticoreEVM, ABI
 ################ Script #######################
 
-seth = ManticoreEVM()
-seth.verbosity(0)
+m = ManticoreEVM()
+m.verbosity(0)
 #The contract account to analyze
 contract_source_code = '''
 pragma solidity ^0.4.15;
@@ -80,31 +80,28 @@ contract GenericReentranceExploit {
 
 
 #Initialize user and contracts
-user_account = seth.create_account(balance=100000000000000000)
-attacker_account = seth.create_account(balance=100000000000000000)
+user_account = m.create_account(balance=100000000000000000)
+attacker_account = m.create_account(balance=100000000000000000)
 
-contract_account = seth.solidity_create_contract(contract_source_code, owner=user_account) #Not payable
-seth.world.set_balance(contract_account, 1000000000000000000)  #give it some ether
+contract_account = m.solidity_create_contract(contract_source_code, owner=user_account) #Not payable
+m.world.set_balance(contract_account, 1000000000000000000)  #give it some ether
 
-exploit_account = seth.solidity_create_contract(exploit_source_code, owner=attacker_account)
+exploit_account = m.solidity_create_contract(exploit_source_code, owner=attacker_account)
 
 print "[+] Setup the exploit"
 exploit_account.set_vulnerable_contract(contract_account)
 exploit_account.set_reentry_reps(30)
 
-
-
-print "\t Setting attack string"
+print "[+] Setting attack string"
 #'\x9d\x15\xfd\x17'+pack_msb(32)+pack_msb(4)+'\x5f\xd8\xc7\x10',
 reentry_string = ABI.make_function_id('withdrawBalance()')
 exploit_account.set_reentry_attack_string(reentry_string)
 
-
 print "[+] Initial world state"
-print " attacker_account %x balance: %d"% (attacker_account, seth.get_balance(attacker_account))
-print " exploit_account %x balance: %d"%  (exploit_account, seth.get_balance(exploit_account))
-print " user_account %x balance: %d"%  (user_account, seth.get_balance(user_account))
-print " contract_account %x balance: %d"%  (contract_account, seth.get_balance(contract_account))
+print " attacker_account %x balance: %d"% (attacker_account, m.get_balance(attacker_account))
+print " exploit_account %x balance: %d"%  (exploit_account, m.get_balance(exploit_account))
+print " user_account %x balance: %d"%  (user_account, m.get_balance(user_account))
+print " contract_account %x balance: %d"%  (contract_account, m.get_balance(contract_account))
 
 
 #User deposits all in contract
@@ -115,26 +112,16 @@ contract_account.addToBalance(value=100000000000000000)
 print "[+] Let attacker deposit some small amount using exploit"
 exploit_account.proxycall(ABI.make_function_id('addToBalance()'), value=100000000000000000)
 
-print "[+] Let attacker extract all  using exploit" 
+print "[+] Let attacker extract all using exploit" 
 exploit_account.proxycall(ABI.make_function_id('withdrawBalance()'))
 
 print "[+] Let attacker destroy the exploit andprofit" 
-exploit_account.get_money()
-
-print " attacker_account %x balance: %d"% (attacker_account, seth.get_balance(attacker_account))
-print " user_account %x balance: %d"%  (user_account, seth.get_balance(user_account))
-print " contract_account %x balance: %d"%  (contract_account, seth.get_balance(contract_account))
-
-print "[+] There are %d reverted states now"% len(seth.final_state_ids)
-for state_id in seth.final_state_ids:
-    print seth.report(state_id)
-
-print "[+] There are %d alive states now"% (len(seth.running_state_ids))
-for state_id in seth.running_state_ids:
-    print seth.report(state_id)
-
-print "[+] Global coverage:"
-print seth.coverage(contract_account)
+exploit_account.get_money() 
 
+print " attacker_account %x balance: %d"% (attacker_account, m.get_balance(attacker_account))
+print " user_account %x balance: %d"%  (user_account, m.get_balance(user_account))
+print " contract_account %x balance: %d"%  (contract_account, m.get_balance(contract_account))
 
+m.finalize()
+print "[+] Look for results in %s"% m.workspace
 
diff --git a/examples/evm/reentrancy_symbolic.py b/examples/evm/reentrancy_symbolic.py
index 9edfe62..6008bbe 100644
--- a/examples/evm/reentrancy_symbolic.py
+++ b/examples/evm/reentrancy_symbolic.py
@@ -1,8 +1,8 @@
 from manticore.seth import ManticoreEVM
 ################ Script #######################
 
-seth = ManticoreEVM()
-seth.verbosity(0)
+m = ManticoreEVM()
+m.verbosity(0)
 #The contract account to analyze
 contract_source_code = '''
 pragma solidity ^0.4.15;
@@ -76,10 +76,10 @@ contract GenericReentranceExploit {
 
 
 #Initialize user and contracts
-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
-exploit_account = seth.solidity_create_contract(exploit_source_code, owner=attacker_account)
+user_account = m.create_account(balance=100000000000000000)
+attacker_account = m.create_account(balance=100000000000000000)
+contract_account = m.solidity_create_contract(contract_source_code, owner=user_account) #Not payable
+exploit_account = m.solidity_create_contract(exploit_source_code, owner=attacker_account)
 
 
 #User deposits all in contract
@@ -87,10 +87,10 @@ print "[+] user deposited some."
 contract_account.addToBalance(value=100000000000000000)
 
 print "[+] Initial world state"
-print "     attacker_account %x balance: %d"% (attacker_account, seth.get_balance(attacker_account))
-print "     exploit_account %x balance: %d"%  (exploit_account, seth.get_balance(exploit_account))
-print "     user_account %x balance: %d"%  (user_account, seth.get_balance(user_account))
-print "     contract_account %x balance: %d"%  (contract_account, seth.get_balance(contract_account))
+print "     attacker_account %x balance: %d"% (attacker_account, m.get_balance(attacker_account))
+print "     exploit_account %x balance: %d"%  (exploit_account, m.get_balance(exploit_account))
+print "     user_account %x balance: %d"%  (user_account, m.get_balance(user_account))
+print "     contract_account %x balance: %d"%  (contract_account, m.get_balance(contract_account))
 
 
 
@@ -101,28 +101,20 @@ print "\t Setting 30 reply reps"
 exploit_account.set_reentry_reps(30)
 
 print "\t Setting reply string"
-exploit_account.set_reentry_attack_string(seth.SByte(4))
+exploit_account.set_reentry_attack_string(m.SByte(4))
 
 #Attacker is
 print "[+] Attacker first transaction"
-exploit_account.proxycall(seth.SByte(4), value=seth.SValue)
+exploit_account.proxycall(m.SByte(4), value=m.SValue)
 
 print "[+] Attacker second transaction" 
-exploit_account.proxycall(seth.SByte(4))
+exploit_account.proxycall(m.SByte(4))
 
 print "[+] The attacker destroys the exploit contract and profit" 
 exploit_account.get_money()
 
-#print "[+] There are %d reverted states now"% len(seth.final_state_ids)
-#for state_id in seth.final_state_ids:
-#     seth.report(state_id)
-
-print "[+] There are %d alive states now"% (len(seth.running_state_ids))
-for state_id in seth.running_state_ids:
-    world = seth.get_world(state_id)
-
-print "[+] Global coverage:"
-print seth.coverage(contract_account, ty='SUICIDE')
-
-
+#Let seth know we are not sending more transactions so it can output 
+# info about running states and global statistics
+m.finalize()
+print "[+] Look for results in %s"% m.workspace
 
diff --git a/examples/evm/simple_functions.py b/examples/evm/simple_functions.py
index 5ac115e..fabd27a 100644
--- a/examples/evm/simple_functions.py
+++ b/examples/evm/simple_functions.py
@@ -1,8 +1,8 @@
 from manticore.seth import ManticoreEVM
 ################ Script #######################
 
-seth = ManticoreEVM()
-seth.verbosity(0)
+m = ManticoreEVM()
+m.verbosity(2)
 #And now make the contract account to analyze
 # cat  | solc --bin 
 source_code = '''
@@ -21,27 +21,17 @@ contract Test {
 }
 '''
 #Initialize accounts
-user_account = seth.create_account(balance=1000)
-contract_account = seth.solidity_create_contract(source_code, owner=user_account)
+user_account = m.create_account(balance=1000)
+contract_account = m.solidity_create_contract(source_code, owner=user_account)
 
-symbolic_data = seth.SByte(4) 
+symbolic_data = m.make_symbolic_buffer(4) 
 symbolic_value = None 
-seth.transaction(  caller=user_account,
+m.transaction(  caller=user_account,
                    address=contract_account,
                    value=symbolic_value,
                    data=symbolic_data
                  )
 
-
-print "[+] There are %d reverted states now"% len(seth.final_state_ids)
-for state_id in seth.final_state_ids:
-    print seth.report(state_id)
-
-print "[+] There are %d alive states now"% len(seth.running_state_ids)
-for state_id in seth.running_state_ids:
-    print seth.report(state_id)
-
-print "[+] Global coverage:"
-print seth.coverage(contract_account)
-
+m.finalize()
+print "[+] Look for results in %s"% m.workspace
 
diff --git a/examples/evm/simple_mapping.py b/examples/evm/simple_mapping.py
index 6c96c51..41ba882 100644
--- a/examples/evm/simple_mapping.py
+++ b/examples/evm/simple_mapping.py
@@ -1,8 +1,8 @@
 from manticore.seth import ManticoreEVM
 ################ Script #######################
 
-seth = ManticoreEVM()
-seth.verbosity(2)
+m = ManticoreEVM()
+m.verbosity(2)
 #And now make the contract account to analyze
 # cat  | solc --bin 
 source_code = '''
@@ -30,28 +30,19 @@ contract Test {
 }
 '''
 #Initialize accounts
-user_account = seth.create_account(balance=1000)
-contract_account = seth.solidity_create_contract(source_code, owner=user_account)
+user_account = m.create_account(balance=1000)
+contract_account = m.solidity_create_contract(source_code, owner=user_account)
 
 
-symbolic_data = seth.SByte(64) 
+symbolic_data = m.SByte(64) 
 symbolic_value = 0
-seth.transaction(  caller=user_account,
+m.transaction(  caller=user_account,
                    address=contract_account,
                    value=symbolic_value,
                    data=symbolic_data
                  )
 
-
-print "[+] There are %d reverted states now"% len(seth.final_state_ids)
-for state_id in seth.final_state_ids:
-    print seth.report(state_id)
-
-print "[+] There are %d alive states now"% len(seth.running_state_ids)
-for state_id in seth.running_state_ids:
-    print seth.report(state_id)
-
-print "[+] Global coverage:"
-print seth.coverage(contract_account)
+m.finalize()
+print "[+] Look for results in %s"% m.workspace
 
 
diff --git a/examples/evm/simple_transaction.py b/examples/evm/simple_transaction.py
index b2b1193..7425a20 100644
--- a/examples/evm/simple_transaction.py
+++ b/examples/evm/simple_transaction.py
@@ -1,8 +1,8 @@
 from manticore.seth import ManticoreEVM
 ################ Script #######################
 
-seth = ManticoreEVM()
-seth.verbosity(0)
+m = ManticoreEVM()
+m.verbosity(0)
 #And now make the contract account to analyze
 # cat  | solc --bin 
 source_code = '''
@@ -22,22 +22,22 @@ contract Test {
 }
 '''
 #Initialize accounts
-user_account = seth.create_account(balance=1000)  
-contract_account = seth.solidity_create_contract(source_code, owner=user_account)
+user_account = m.create_account(balance=1000)  
+contract_account = m.solidity_create_contract(source_code, owner=user_account)
 
 
-contract_account.target(value=seth.SValue)
+contract_account.target(value=m.SValue)
 
 
-print "[+] There are %d reverted states now"% len(seth.final_state_ids)
-for state_id in seth.final_state_ids:
-    print seth.report(state_id)
+print "[+] There are %d reverted states now"% len(m.final_state_ids)
+for state_id in m.final_state_ids:
+    print m.report(state_id)
 
-print "[+] There are %d alive states now"% len(seth.running_state_ids)
-for state_id in seth.running_state_ids:
-    print seth.report(state_id)
+print "[+] There are %d alive states now"% len(m.running_state_ids)
+for state_id in m.running_state_ids:
+    print m.report(state_id)
 
 print "[+] Global coverage:"
-print seth.coverage(contract_account)
+print m.coverage(contract_account)
 
 
diff --git a/examples/evm/solidse.py b/examples/evm/solidse.py
deleted file mode 100644
index cd9179a..0000000
--- a/examples/evm/solidse.py
+++ /dev/null
@@ -1,99 +0,0 @@
-from manticore.seth import ManticoreEVM, calculate_coverage, ABI
-
-################ Script #######################
-seth = ManticoreEVM(procs=8)
-
-seth.verbosity(0)
-#And now make the contract account to analyze
-# cat  | solc --bin 
-source_code = file(sys.argv[1],'rb').read()
-
-user_account = seth.create_account(balance=1000)
-print "[+] Creating a user account", user_account
-
-contract_account = seth.solidity_create_contract(source_code, owner=user_account)
-print "[+] Creating a contract account", contract_account
-
-attacker_account = seth.create_account(balance=1000)
-print "[+] Creating a attacker account", attacker_account
-
-
-last_coverage = None 
-new_coverage = 0
-tx_count = 0
-while new_coverage != last_coverage and new_coverage < 100:
-
-    symbolic_data = seth.make_symbolic_buffer(320)
-    symbolic_value = seth.make_symbolic_value() 
-
-    seth.transaction(caller=attacker_account,
-                    address=contract_account,
-                    data=symbolic_data,
-                    value=symbolic_value )
-
-    tx_count += 1
-    last_coverage = new_coverage
-    new_coverage = seth.global_coverage(contract_account)
-    
-    print "[+] Coverage after %d transactions: %d%%"%(tx_count, new_coverage)
-    print "[+] There are %d reverted states now"% len(seth.terminated_state_ids)
-    print "[+] There are %d alive states now"% len(seth.running_state_ids)
-
-for state in seth.all_states:
-    print "="*20
-    blockchain = state.platform
-    for tx in blockchain.transactions: #external transactions
-        print "Transaction:"
-        print "\tsort %s" % tx.sort    #Last instruction or type? TBD
-        print "\tcaller 0x%x" % state.solve_one(tx.caller)  #The caller as by the yellow paper
-        print "\taddress 0x%x" % state.solve_one(tx.address) #The address as by the yellow paper
-        print "\tvalue: %d" % state.solve_one(tx.value)   #The value as by the yellow paper
-        print "\tcalldata: %r" % state.solve_one(tx.data)
-        print "\tresult: %s" % tx.result  #The result if any RETURN or REVERT
-        print "\treturn_data: %r" % state.solve_one(tx.return_data)  #The returned data if RETURN or REVERT
-
-        metadata = seth.get_metadata(tx.address)
-        if tx.sort == 'Call':
-            if metadata is not None:
-                function_id = tx.data[:4]  #hope there is enough data
-                function_id = state.solve_one(function_id).encode('hex')
-                signature = metadata.get_func_signature(function_id)
-                print "\tparsed calldata", ABI.parse(signature, tx.data) #func_id, *function arguments
-                if tx.result == 'RETURN':
-                    ret_types = metadata.get_func_return_types(function_id)
-                    print '\tparsed return_data', ABI.parse(ret_types, tx.return_data) #function return
-
-        if tx.result in ('THROW', 'REVERT', 'SELFDESTRUCT'):
-            if metadata is not None:
-                address, offset = state.context['seth.trace'][-1]
-                print metadata.get_source_for(offset)
-            
-
-    #the logs
-    for log_item in blockchain.logs:
-        print "log address", log_item.address
-        print "memlog", log_item.memlog
-        for topic in log_item.topics:
-            print "topic", topic
-
-    for address in blockchain.deleted_addresses:
-        print "deleted address", address #selfdestructed address
-
-    #accounts alive in this state
-    for address in blockchain.contract_accounts: 
-        code = blockchain.get_code(address)
-        balance = blockchain.get_balance(address)
-        trace = set(( offset for address_i, offset in state.context['seth.trace'] if address == address_i))        
-        print calculate_coverage(code, trace) #coverage % for address in this state
-
-# All accounts ever created by the script 
-# (may not all be alife in all states)
-# (accounts created by contract code are not in this list )
-print "[+] Global coverage:"
-for address in seth.contract_accounts: 
-    print address, seth.global_coverage(address) #coverage % for address in this state
-
-
-
-
-
diff --git a/manticore/__main__.py b/manticore/__main__.py
index 7f7e0a3..77fed5d 100644
--- a/manticore/__main__.py
+++ b/manticore/__main__.py
@@ -103,75 +103,10 @@ def ethereum_cli(args):
         print "[+] There are %d reverted states now"% len(m.terminated_state_ids)
         print "[+] There are %d alive states now"% len(m.running_state_ids)
 
-    for state in m.all_states:
-        print str(state.context['last_exception'])
 
-    for address, pc, finding in m.global_findings:
-        output = ''
-        output += 'Finding: %s\n' % finding
-        output += '\t Contract: %s\n' % address
-        output += '\t Program counter: %s\n' % pc
-        output += '\t Snippet:\n'
-        src = m.get_metadata(address).get_source_for(pc)
-        output += '\n'.join(('\t\t'+x for x in src.split('\n')))
-        output += '\n'
-        print output
-            
+    m.finalize()
+    print "[+] Look for results in %s"% m.workspace
 
-    # for state in seth.all_states:
-    #     blockchain = state.platform
-    #     for tx in blockchain.transactions:  # external transactions
-    #         print "Transaction:"
-    #         print "\tsort %s" % tx.sort  # Last instruction or type? TBD
-    #         print "\tcaller 0x%x" % state.solve_one(
-    #             tx.caller)  # The caller as by the yellow paper
-    #         print "\taddress 0x%x" % state.solve_one(
-    #             tx.address)  # The address as by the yellow paper
-    #         print "\tvalue: %d" % state.solve_one(
-    #             tx.value)  # The value as by the yellow paper
-    #         print "\tcalldata: %r" % state.solve_one(tx.data)
-    #         print "\tresult: %s" % tx.result  # The result if any RETURN or REVERT
-    #         print "\treturn_data: %r" % state.solve_one(
-    #             tx.return_data)  # The returned data if RETURN or REVERT
-    #
-    #         if tx.sort == 'Call':
-    #             metadata = seth.get_metadata(tx.address)
-    #             if metadata is not None:
-    #                 function_id = tx.data[:4]  # hope there is enough data
-    #                 function_id = state.solve_one(function_id).encode('hex')
-    #                 signature = metadata.get_func_signature(function_id)
-    #                 print "\tparsed calldata", ABI.parse(signature,
-    #                                                      tx.data)  # func_id, *function arguments
-    #                 if tx.result == 'RETURN':
-    #                     ret_types = metadata.get_func_return_types(function_id)
-    #                     print '\tparsed return_data', ABI.parse(ret_types,
-    #                                                             tx.return_data)  # function return
-    #
-    #     # the logs
-    #     for log_item in blockchain.logs:
-    #         print "log address", log_item.address
-    #         print "memlog", log_item.memlog
-    #         for topic in log_item.topics:
-    #             print "topic", topic
-    #
-    #     for address in blockchain.deleted_addresses:
-    #         print "deleted address", address  # selfdestructed address
-    #
-    #     # accounts alive in this state
-    #     for address in blockchain.contract_accounts:
-    #         code = blockchain.get_code(address)
-    #         balance = blockchain.get_balance(address)
-    #         trace = set((offset for address_i, offset in state.context['seth.trace'] if
-    #                      address == address_i))
-    #         print calculate_coverage(code, trace)  # coverage % for address in this state
-    #
-    #         # All accounts ever created by the script
-    #         # (may not all be alife in all states)
-    #         # (accounts created by contract code are not in this list )
-    # print "[+] Global coverage:"
-    # for address in seth.contract_accounts:
-    #     print address, seth.global_coverage(
-    #         address)  # coverage % for address in this state
 
 
 def main():
diff --git a/manticore/core/workspace.py b/manticore/core/workspace.py
index 3bb0a46..0273685 100644
--- a/manticore/core/workspace.py
+++ b/manticore/core/workspace.py
@@ -393,6 +393,14 @@ class Workspace(object):
         self._store.save_state(state, '{}{:08x}{}'.format(self._prefix, id_, self._suffix))
         return id_
 
+    def rm_state(self, state_id):
+        """
+        Remove a state from storage identified by `state_id`.
+
+        :param state_id: The state reference of what to load
+        """
+        return self._store.rm('{}{:08x}{}'.format(self._prefix, state_id, self._suffix))
+
 
 class ManticoreOutput(object):
     """
@@ -415,6 +423,23 @@ class ManticoreOutput(object):
         self._id_gen = manager.Value('i', self._last_id)
         self._lock = manager.Condition(manager.RLock())
 
+    def testcase(self, prefix='test'):
+        class Testcase(object):
+            def __init__(self, workspace, prefix):
+                self._num = workspace._increment_id()
+                self._prefix = prefix
+                self._ws = workspace
+
+            @property
+            def num(self):
+                return self._num
+
+            def open_stream(self, suffix=''):
+                stream_name = '{}_{:08x}.{}'.format(self._prefix, self._num, suffix)
+                return self._ws.save_stream(stream_name)
+ 
+        return Testcase(self, prefix)
+
     @property
     def store(self):
         return self._store
@@ -438,6 +463,7 @@ class ManticoreOutput(object):
     def _increment_id(self):
         self._last_id = self._id_gen.value
         self._id_gen.value += 1
+        return self._last_id
 
     def _named_key(self, suffix):
         return '{}_{:08x}.{}'.format(self._named_key_prefix, self._last_id, suffix)
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 34a0dcc..8d24a34 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -15,7 +15,6 @@ if sys.version_info < (3, 6):
 
 logger = logging.getLogger(__name__)
 
-
 # Auxiliar constants and functions
 TT256 = 2 ** 256
 TT256M1 = 2 ** 256 - 1
@@ -45,6 +44,11 @@ class Transaction(object):
         ''' Implements serialization/pickle '''
         return (self.__class__,  (self.sort,  self.address, self.origin, self.price, self.data, self.caller, self.value, self.return_data, self.result))
 
+class EVMLog():
+    def __init__(self, address, memlog, topics):
+        self.address = address
+        self.memlog = memlog
+        self.topics = topics
 
 
 
@@ -141,6 +145,10 @@ class EVMMemory(object):
         return offset in self._memory or \
                offset in self._symbols
 
+    def items(self):
+        offsets = set( self._symbols.keys() + self._memory.keys())
+        return [(x, self[x]) for x in offsets]
+
     def get(self, offset, default=0):
         result = self.read(offset, 1)
         if not result:
@@ -1722,13 +1730,13 @@ class EVM(Eventful):
     ##########################################################################
     ##Logging Operations
     def LOG(self, address, size, *topics):
+
         if issymbolic(size):
             raise ConcretizeStack(2, policy='ONE')
 
-        memlog = []
-        for i in range(size):
-            memlog.append(self._load(address+i))
-        self.logs.append((self.address, memlog, topics))
+        memlog = self.read_buffer(address, size)
+
+        self.logs.append(EVMLog(self.address, memlog, topics))
         logger.info('LOG %r %r', memlog, topics)
 
     ##########################################################################
@@ -1736,10 +1744,20 @@ class EVM(Eventful):
     def read_buffer(self, offset, size):
         if size:
             self._allocate(offset+size)
-        buf = []
+
+        data = []
         for i in xrange(size):
-            buf.append(Operators.CHR(self._load(offset+i)))
-        return buf
+            data.append(Operators.CHR(self._load(offset+i)))
+
+        if any(map(issymbolic, data)):
+            data_symb = self._constraints.new_array(index_bits=256, index_max=len(data))
+            for i in range(len(data)):
+                data_symb[i] = Operators.ORD(data[i])
+            data = data_symb
+        else:
+            data = ''.join(data)
+
+        return data
 
     def write_buffer(self, offset, buf):
         count = 0
@@ -1979,6 +1997,12 @@ class EVMWorld(Platform):
     def get_storage_data(self, address, offset):
         return self.storage[address]['storage'].get(offset)
 
+    def get_storage_items(self, address):
+        return self.storage[address]['storage'].items()
+
+    def has_storage(self, address):
+        return len(self.storage[address]['storage'].items()) != 0
+
     def set_balance(self, address, value):
         self.storage[int(address)]['balance'] = value
 
@@ -1988,36 +2012,15 @@ class EVMWorld(Platform):
     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 has_code(self, address):
+        return len(self.storage[address]['code']) > 0
+
 
     def log(self, address, topic, data):
         self.logs.append((address, data, topics))
@@ -2080,6 +2083,8 @@ class EVMWorld(Platform):
         if not rollback:
             if self.depth:
                 self.current.global_storage = vm.global_storage
+                self.current.logs += vm.logs
+                self.current.suicides = self.current.suicides.union(vm.suicides)
             else:
                 self._global_storage = vm.global_storage
                 self._deleted_address = self._deleted_address.union(vm.suicides)
@@ -2177,8 +2182,7 @@ class EVMWorld(Platform):
 
         self.storage[address]['storage'] = EVMMemory(self.constraints, 256, 256)
 
-
-        self._pending_transaction = ('Create', address, origin, price, '', origin, balance, init, header)
+        self._pending_transaction = ('Create', address, origin, price, '', origin, balance, ''.join(init), header)
 
         if run:
             assert False
@@ -2197,6 +2201,7 @@ class EVMWorld(Platform):
         caller = self.current.address
         price = self.current.price
         header = {'timestamp': 100}  #FIXME
+
         self.create_contract(origin, price, address=None, balance=value, init=bytecode, run=False)
         self._process_pending_transaction()
 
@@ -2220,6 +2225,8 @@ class EVMWorld(Platform):
             for i in range(len(data)):
                 data_symb[i] = Operators.ORD(data[i])
             data = data_symb
+        else:
+            data = ''.join(data)
         bytecode = self.get_code(address)
         self._pending_transaction = ('Call', address, origin, price, data, caller, value, bytecode, header)
 
@@ -2237,21 +2244,74 @@ class EVMWorld(Platform):
                 pass
 
     def _process_pending_transaction(self):
+        def err():
+            if self.depth == 0:
+                raise TerminateState("Not Enough Funds for transaction", testcase=True)
+
+
         if self._pending_transaction is None:
             return
         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
-        self.send_ether(caller, address, value)
+
+
+        src_balance = self.get_balance(caller) #from
+        dst_balance = self.get_balance(address) #to
+
+        #discarding absurd amount of ether (no ether overflow)
+        self.constraints.add(src_balance + value >= src_balance)
+
+        failed = False
+
+        if self.depth > 1024:
+            failed=True
+
+        if not failed:
+            enough_balance = src_balance >= value
+            if issymbolic(enough_balance):
+                enough_balance_solutions = solver.get_all_values(self._constraints, enough_balance)
+
+                if set(enough_balance_solutions) == set([True, False]): 
+                    raise Concretize('Forking on available funds',
+                                     expression = src_balance < value,
+                                     setstate=lambda a,b: None,
+                                     policy='ALL')
+
+                if set(enough_balance_solutions) == set([False]):
+                    failed = True
+            else:
+                if not enough_balance:
+                    failed = True
+
         self._pending_transaction=None
+
+
+        if ty == 'Create': 
+            data = bytecode
+ 
+        is_human_tx = ( self.depth == 0 )
+
+        if failed:
+            if is_human_tx: #human transaction
+                tx = Transaction(ty, address, origin, price, data, caller, value, 'TXERROR', None)
+                self._transactions.append(tx)
+            else:
+                self.current._push(0)
+                return
+
+        #Here we have enoug funds and room in the callstack
+
+        self.storage[address]['balance'] += value
+        self.storage[caller]['balance'] -= value
+
         new_vm = EVM(self._constraints, address, origin, price, data, caller, value, bytecode, header, global_storage=self.storage)
         self._push_vm(new_vm)
-        if self.depth == 1:
 
+        if is_human_tx:
             #handle human transactions
             if ty == 'Create':
                 self.current.last_exception = Create(None, None, None)
-                data = bytecode
             elif ty == 'Call':
                 self.current.last_exception = Call(None, None, None, None)
 
diff --git a/manticore/seth.py b/manticore/seth.py
index 728b5a6..8555b78 100644
--- a/manticore/seth.py
+++ b/manticore/seth.py
@@ -9,6 +9,7 @@ import sha3
 import json
 import logging
 import StringIO
+import cPickle as pickle
 from .core.plugin import Plugin
 
 logger = logging.getLogger(__name__)
@@ -102,7 +103,7 @@ class UnitializedStorage(Detector):
 
 
 def calculate_coverage(code, seen):
-    '''     '''
+    ''' Calculates what % of code have been seen '''
     runtime_bytecode = code
     end = None
     if  ''.join(runtime_bytecode[-44: -34]) =='\x00\xa1\x65\x62\x7a\x7a\x72\x30\x58\x20' \
@@ -118,34 +119,37 @@ def calculate_coverage(code, seen):
     return count*100.0/total
 
 class SolidityMetadata(object):
-    def __init__(self, name, source_code, init_bytecode, runtime_bytecode, metadata, metadata_runtime, hashes, abi):
+    def __init__(self, name, source_code, init_bytecode, runtime_bytecode, srcmap, srcmap_runtime, hashes, abi, warnings):
+        ''' Contract metadata for solidity based contracts '''
         self.name = name
         self.source_code = source_code
-        self.init_bytecode = init_bytecode
-        self.metadata = metadata
-
+        self._init_bytecode = init_bytecode
+        self._runtime_bytecode = runtime_bytecode
         self.hashes = hashes
         self.abi = dict( [(item.get('name', '{fallback}'), item) for item in abi ])
-        self.runtime_bytecode = runtime_bytecode
+        self.warnings = warnings
+        self.srcmap_runtime = self.__build_source_map(self.runtime_bytecode, srcmap_runtime)
+        self.srcmap = self.__build_source_map(self.init_bytecode, srcmap)
 
+    def __build_source_map(self, bytecode, srcmap):
         # https://solidity.readthedocs.io/en/develop/miscellaneous.html#source-mappings
-        self.metadata_runtime = {}
+        new_srcmap = {}
         end = None
-        if  ''.join(runtime_bytecode[-44: -34]) =='\x00\xa1\x65\x62\x7a\x7a\x72\x30\x58\x20' \
-            and  ''.join(runtime_bytecode[-2:]) =='\x00\x29':
+        if  ''.join(bytecode[-44: -34]) =='\x00\xa1\x65\x62\x7a\x7a\x72\x30\x58\x20' \
+            and  ''.join(bytecode[-2:]) =='\x00\x29':
             end = -9-33-2  #Size of metadata at the end of most contracts
 
         asm_offset = 0
         asm_pos = 0
-        md = dict(enumerate(metadata_runtime[asm_pos].split(':')))
+        md = dict(enumerate(srcmap[asm_pos].split(':')))
         s = int(md.get(0,0))
         l = int(md.get(1,0))
         f = int(md.get(2,0))
         j = md.get(3,None)
 
-        for i in evm.EVMAsm.disassemble_all(self.runtime_bytecode[:end]):
-            if len(metadata_runtime[asm_pos]):
-                md = metadata_runtime[asm_pos]
+        for i in evm.EVMAsm.disassemble_all(bytecode[:end]):
+            if asm_pos in srcmap and len(srcmap[asm_pos]):
+                md = srcmap[asm_pos]
                 if len(md):
                     d = {}
                     for p, k in enumerate(md.split(':')):
@@ -157,14 +161,41 @@ class SolidityMetadata(object):
                     f = int(d.get(2,f))
                     j = d.get(3,j)
 
-            self.metadata_runtime[asm_offset] = (s,l,f,j)
+            new_srcmap[asm_offset] = (s,l,f,j)
             asm_pos += 1
             asm_offset += i.size
 
-    def get_source_for(self, asm_pos):
+        return new_srcmap 
+
+    @property
+    def runtime_bytecode(self):
+        ''' Removes metadata from the tail of bytecode '''
+        end = None
+        if  ''.join(self._runtime_bytecode[-44: -34]) =='\x00\xa1\x65\x62\x7a\x7a\x72\x30\x58\x20' \
+            and  ''.join(self._runtime_bytecode[-2:]) =='\x00\x29':
+            end = -9-33-2  #Size of metadata at the end of most contracts
+        return self._runtime_bytecode[:end]
+    @property
+    def init_bytecode(self):
+        ''' Removes metadata from the tail of bytecode '''
+        end = None
+        if  ''.join(self._init_bytecode[-44: -34]) =='\x00\xa1\x65\x62\x7a\x7a\x72\x30\x58\x20' \
+            and  ''.join(self._init_bytecode[-2:]) =='\x00\x29':
+            end = -9-33-2  #Size of metadata at the end of most contracts
+        return self._init_bytecode[:end]
+
+
+    def get_source_for(self, asm_offset, runtime=True):
         ''' Solidity source code snippet related to `asm_pos` evm bytecode offset
+            if runtime is False it uses initialization bytecode source map
         '''
-        beg, size, _, _ = self.metadata_runtime[asm_pos]
+        if runtime:
+            srcmap = self.srcmap_runtime
+        else:
+            srcmap = self.srcmap
+        
+        beg, size, _, _ = srcmap[asm_offset]
+
         output = ''
         nl = self.source_code.count('\n')
         snippet = self.source_code[beg:beg+size]
@@ -251,18 +282,20 @@ class ABI(object):
         assert isinstance(value, list)
         serialized = [ABI.serialize_uint(len(value))]
         for item in value:
+            #TODO check all values are the same type
             serialized.append(ABI.serialize(item))    
         return reduce(lambda x,y: x+y, serialized)
 
     @staticmethod
-    def make_function_id( method_name):
+    def make_function_id( method_name_and_signature):
+        ''' Makes function hash id from method signature '''
         s = sha3.keccak_256()
-        s.update(method_name)
+        s.update(method_name_and_signature)
         return s.hexdigest()[:8].decode('hex')
 
     @staticmethod
     def make_function_arguments(*args):
-        
+        ''' Serializes a sequence of arguments '''
         if len(args) == 0:
             return () 
         args = list(args)
@@ -299,14 +332,23 @@ class ABI(object):
         result.append(ABI.make_function_arguments(*args))
         return reduce(lambda x,y: x+y, result)
 
-
-
     @staticmethod        
     def _consume_type(ty, data, offset):
+        ''' INTERNAL parses a value of type from data '''
         def get_uint(size, offset):
+            def simplify(x):
+                value = arithmetic_simplifier(x)
+                if isinstance(value, Constant) and not value.taint:
+                    return value.value
+                else:
+                    return value
+
+            size = simplify(size)
+            offset = simplify(offset)
             byte_size = size/8
             padding = 32 - byte_size # for 160
-            return Operators.CONCAT(size, *map(Operators.ORD, data[offset+padding:offset+padding+byte_size]))
+            value = arithmetic_simplifier(Operators.CONCAT(size, *map(Operators.ORD, data[offset+padding:offset+padding+byte_size])))
+            return simplify(value)
         if ty == u'uint256':
             return get_uint(256, offset), offset+32
         if ty == u'bool':
@@ -330,8 +372,9 @@ class ABI(object):
 
     @staticmethod
     def parse(signature, data):
-        is_multiple = '(' in signature
+        ''' Deserialize function ID and arguments specified in `signature` from `data` '''
 
+        is_multiple = '(' in signature
         if is_multiple:
             func_name = signature.split('(')[0]
             types = signature.split('(')[1][:-1].split(',')
@@ -502,7 +545,7 @@ class ManticoreEVM(Manticore):
         with tempfile.NamedTemporaryFile() as temp:
             temp.write(source_code)
             temp.flush()
-            p = Popen([solc, '--combined-json', 'abi,srcmap,srcmap-runtime,bin,hashes,bin-runtime', temp.name], stdout=PIPE)
+            p = Popen([solc, '--combined-json', 'abi,srcmap,srcmap-runtime,bin,hashes,bin-runtime', temp.name], stdout=PIPE, stderr=PIPE)
             outp = json.loads(p.stdout.read())
             assert len(outp['contracts']), "Only one contract by file supported"
             name, outp = outp['contracts'].items()[0]
@@ -513,7 +556,8 @@ class ManticoreEVM(Manticore):
             hashes = outp['hashes']
             abi = json.loads(outp['abi'])
             runtime = outp['bin-runtime'].decode('hex')
-            return name, source_code, bytecode, runtime, srcmap, srcmap_runtime, hashes, abi
+            warnings = p.stderr.read()
+            return name, source_code, bytecode, runtime, srcmap, srcmap_runtime, hashes, abi, warnings
 
     def __init__(self, procs=1):
         ''' A manticere EVM manager 
@@ -561,7 +605,6 @@ class ManticoreEVM(Manticore):
             else:
                 return context['_saved_states']
 
-
     @property
     def all_state_ids(self):
         ''' IDs of the all states ''' 
@@ -594,6 +637,41 @@ class ManticoreEVM(Manticore):
             state = self.load(state_id)
             yield state
 
+    def count_states(self):
+        ''' Total states count '''
+        return len(self.terminated_state_ids + self.running_state_ids)
+
+    def count_running_states(self):
+        ''' Running states count '''
+        return len(self.running_state_ids)
+
+    def count_terminated_states(self):
+        ''' Terminated states count '''
+        return len(self.terminated_state_ids)
+        
+    def terminate_state_id(self, state_id):
+        ''' Manually  terminates a states by state_id.
+            Moves the state from the running list into the terminated list and 
+            generates a testcase for it
+        '''
+        if state_id != -1:
+            with self.locked_context('seth') as seth_context:
+                lst = seth_context['_saved_states']
+                lst.remove(state_id)
+                seth_context['_saved_states'] = lst
+
+        state = self.load(state_id)
+        self._generate_testcase_callback(state, 'test', 'Still Running')
+
+        if state_id == -1:
+            state_id = self.save(state, final=True)
+            self._initial_state=None
+        else:
+            with self.locked_context('seth') as seth_context:
+                lst = seth_context['_final_states']
+                lst.append(state_id)
+                seth_context['_final_states'] = lst
+        
 
     #deprecate this 5 in favor of for sta in seth.all_states: do stuff?
     def get_world(self, state_id=None):
@@ -616,6 +694,12 @@ class ManticoreEVM(Manticore):
             address = int(address)
         return self.get_world(state_id).storage[address]['storage'].get(offset)
 
+    def get_code(self, address, 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]['code']
+
     def last_return(self, state_id=None):
         ''' Last returned buffer for state `state_id` '''
         state = self.load(state_id)
@@ -641,10 +725,12 @@ class ManticoreEVM(Manticore):
             :type args: tuple
             :return: an EVMAccount
         '''
-
-        name, source_code, init_bytecode, runtime_bytecode, metadata, metadata_runtime, hashes, abi = self._compile(source_code)
+        name, source_code, init_bytecode, runtime_bytecode, metadata, metadata_runtime, hashes, abi, warnings = 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.metadata[address] = SolidityMetadata(name, source_code, init_bytecode, runtime_bytecode, metadata, metadata_runtime, hashes, abi)
+        #FIXME different states "could"(VERY UNLIKELY) have different contracts 
+        # asociated with the same address 
+        self.metadata[address] = SolidityMetadata(name, source_code, init_bytecode, runtime_bytecode, metadata, metadata_runtime, hashes, abi, warnings)
+
         return EVMAccount(address, self, default_caller=owner)
 
     def create_contract(self, owner, balance=0, init=None, address=None):
@@ -718,7 +804,7 @@ class ManticoreEVM(Manticore):
         with self.locked_context('seth') as context:
             assert context['_pending_transaction'] is not None
             #there is at least one states in seth saved states
-            assert context['_saved_states'] or self.initial_state
+            assert context['_saved_states'] or self.initial_state is not None
             #there is no states added to the executor queue
             assert len(self._executor.list()) == 0
 
@@ -779,7 +865,6 @@ class ManticoreEVM(Manticore):
             state = self.initial_state
         else:
             state = self._executor._workspace.load_state(state_id, delete=False)
-
         return state
 
     #Callbacks
@@ -854,13 +939,20 @@ class ManticoreEVM(Manticore):
         ''' INTERNAL USE '''
         assert state.constraints == state.platform.constraints
         assert state.platform.constraints == state.platform.current.constraints
+        logger.debug("%s", state.platform.current)
         #print state.platform.current
-        with self.locked_context('coverage', set) as coverage:
+
+        if 'Call' in str(type(state.platform.current.last_exception)):
+            coverage_context_name = 'runtime_coverage'
+        else:
+            coverage_context_name = 'init_coverage'
+
+        with self.locked_context(coverage_context_name, set) as coverage:
             coverage.add((state.platform.current.address, state.platform.current.pc))
         
     def _did_execute_instruction_callback(self, state, prev_pc, pc, instruction):
         ''' INTERNAL USE '''
-        state.context.setdefault('seth.trace',[]).append((state.platform.current.address, pc))
+        state.context.setdefault('seth.trace',[]).append((state.platform.current.address, prev_pc))
 
     def _did_evm_read_code(self, state, offset, size):
         ''' INTERNAL USE '''
@@ -885,188 +977,253 @@ class ManticoreEVM(Manticore):
         with self.locked_context('seth.global_findings', set) as global_findings:
             return global_findings
 
-    def report(self, state, ty=None):
-        ''' Prints a small report on state. Prints a little something about state :) '''
-        world = state.platform
+    @property
+    def workspace(self):
+        return self._executor._workspace._store.uri
 
-        output = StringIO.StringIO()
+    def _generate_testcase_callback(self, state, name, message):
+        '''
+        Create a serialized description of a given state.
+        :param state: The state to generate information about
+        :param message: Accompanying message
+        '''
+        # workspace should not be responsible for formating the output
+        # each object knows its secrets, each class should be able to report its
+        # final state
+        #super(ManticoreEVM, self)._generate_testcase_callback(state, name, message)
+        def flagged(flag):
+            return '(*)' if flag else '' 
+        testcase = self._output.testcase()
+        logger.info("Generated testcase No. {} - {}".format(testcase.num, message))
+        blockchain = state.platform
+        with testcase.open_stream('summary') as summary:            
+            summary.write("Last exception: %s\n" %state.context['last_exception'])
 
-        def compare_buffers(a, b):
-            if len(a) != len(b):
-                return False
-            cond = True
-            for i in range(len(a)):
-                cond = Operators.AND(a[i]==b[i], cond)
-                if cond is False:
-                    return False
-            return cond
+            #Last instruction
+            metadata = self.get_metadata(blockchain.transactions[-1].address)
+            if metadata is not None:
+                address, offset = state.context['seth.trace'][-1]
+                summary.write('Last instruction at contract %x offset %x\n' %(address, offset))
+                at_runtime = blockchain.transactions[-1].sort != 'Create'
+                summary.write(metadata.get_source_for(offset, at_runtime))
+                summary.write('\n')
 
-        trace = state.context['seth.trace']
-        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]
-        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:
-            runtime_bytecode = ''   
 
-        e = state.context['last_exception']
-        if ty is not None:
-            if str(e) != ty:
-                return
+            #Accounts summary
+            is_something_symbolic = False
+            summary.write("%d accounts.\n" % len(blockchain.accounts))
+            for account_address in blockchain.accounts:
+                summary.write("Address: 0x%x\n" % account_address)
+                balance = blockchain.get_balance(account_address)
+                is_balance_symbolic = issymbolic(balance)
+                is_something_symbolic = is_something_symbolic or is_balance_symbolic
+                balance = state.solve_one(balance)
+                summary.write("Balance: %d %s\n" % (balance, flagged(is_balance_symbolic)))
 
-        output.write("REPORT:" + str(e)) 
+                if blockchain.has_storage(account_address):
+                    summary.write("Storage:\n")
+                    for offset, value in blockchain.get_storage_items(account_address):
+                        is_storage_symbolic = issymbolic(offset) or issymbolic(value) 
+                        offset = state.solve_one(offset)
+                        value = state.solve_one(value)
+                        summary.write("\t%032x -> %032x %s\n" % (offset, value, flagged(is_storage_symbolic)))
+                        is_something_symbolic = is_something_symbolic or is_storage_symbolic
 
-        try:
-            # Magic number comes from here:
-            # http://solidity.readthedocs.io/en/develop/metadata.html#encoding-of-the-metadata-hash-in-the-bytecode
-            asm = list(evm.EVMAsm.disassemble_all(runtime_bytecode[:-9-33-2]))
-            asm_offset = 0
-            pos = 0
-            source_pos = md_metadata_runtime[pos]
-            for i in asm:
-                if len(md_metadata_runtime[pos]):
-                    source_pos = md_metadata_runtime[pos]
-                if asm_offset == last_pc:
-                    break
-                asm_offset += i.size
-                pos +=1
+                code = blockchain.get_code(account_address)
+                if len(code):
+                    summary.write("Code:\n")
+                    fcode = StringIO.StringIO(code)
+                    for chunk in iter(lambda: fcode.read(32), b''):
+                        summary.write('\t%s\n' % chunk.encode('hex'))
+                    trace = set(( offset for address_i, offset in state.context['seth.trace'] if address == address_i))        
+                    summary.write("Coverage %d%% (on this state)\n" %  calculate_coverage(code, trace)) #coverage % for address in this account/state
+                summary.write("\n")
 
-            beg, size = map(int, source_pos.split(':'))
 
-            output.write( " at:" )
-            nl = md_source_code.count('\n')
-            snippet = md_source_code[beg:beg+size]
-            for l in snippet.split('\n'):
-                output.write('    %s  %s\n'%(nl, l))
-                nl+=1
-        except Exception as e:
-            output.write('\n')
+            if is_something_symbolic:
+                summary.write('\n\n(*) Example solution given. Value is symbolic and may take other values\n')
 
-        output.write("BALANCES\n")
-        for address, account in world.storage.items():
-            if isinstance(account['balance'], Constant):
-                account['balance'] = account['balance'].value
 
-            if issymbolic(account['balance']):
-                m, M = solver.minmax(world.constraints, arithmetic_simplifier(account['balance']))
-                if m == M:
-                    output.write('\t%x %r\n'%(address, M))
-                else:
-                    output.write('\t%x range:[%x, %x]\n'%(address, m, M))
+        #Transactions
+        with testcase.open_stream('tx') as tx_summary:
+            is_something_symbolic = False
+            for tx in blockchain.transactions: #external transactions
+                tx_summary.write("Transactions Nr. %d\n" % blockchain.transactions.index(tx))
+
+                #The result if any RETURN or REVERT
+                tx_summary.write("Type: %s\n" % tx.sort)
+                tx_summary.write("From: 0x%x %s\n" % (state.solve_one(tx.caller), flagged(issymbolic(tx.caller))))
+                tx_summary.write("To: 0x%x %s\n" % (state.solve_one(tx.address), flagged(issymbolic(tx.address))))
+                tx_summary.write("Value: %d %s\n"% (state.solve_one(tx.value), flagged(issymbolic(tx.value))))
+                tx_summary.write("Data: %s %s\n"% (state.solve_one(tx.data).encode('hex'), flagged(issymbolic(tx.data))))
+                if tx.return_data is not None:
+                    return_data = state.solve_one(tx.return_data)
+                    tx_summary.write("Return_data: %s %s\n" % (''.join(return_data).encode('hex'), flagged(issymbolic(tx.return_data))))
+
+                
+                metadata = self.get_metadata(tx.address)
+                if tx.sort == 'Call':
+                    if metadata is not None:
+                        function_id = tx.data[:4]  #hope there is enough data
+                        function_id = state.solve_one(function_id).encode('hex')
+                        signature = metadata.get_func_signature(function_id)
+                        function_name, arguments = ABI.parse(signature, tx.data)
+
+                        if tx.result == 'RETURN':
+                            ret_types = metadata.get_func_return_types(function_id)
+                            return_data = ABI.parse(ret_types, tx.return_data) #function return
+
+                        tx_summary.write('\n')
+                        tx_summary.write( "Function call:\n")
+                        tx_summary.write("%s(" % state.solve_one(function_name ))
+                        tx_summary.write(','.join(map(str, map(state.solve_one, arguments))))
+                        is_argument_symbolic = any(map(issymbolic, arguments))
+                        is_something_symbolic = is_something_symbolic or is_argument_symbolic
+                        tx_summary.write(') -> %s %s\n' % ( tx.result, flagged(is_argument_symbolic)))
+                        is_return_symbolic = any(map(issymbolic, return_data))
+                        return_values = tuple(map(state.solve_one, return_data))
+                        if len(return_values) == 1:
+                            return_values = return_values[0]
+
+                        tx_summary.write('return: %r %s\n' % ( return_values, flagged(is_return_symbolic)))
+                        is_something_symbolic = is_something_symbolic or is_return_symbolic
+
+
+                tx_summary.write('\n\n')
+
+            if is_something_symbolic:
+                tx_summary.write('\n\n(*) Example solution given. Value is symbolic and may take other values\n')
+            
+        #logs
+        with testcase.open_stream('logs') as logs_summary:
+            is_something_symbolic = False
+            if len(blockchain.logs) > 0:
+                for log_item in blockchain.logs:
+                    logs_summary.write("Address: %x\n" % log_item.address)
+                    is_log_symbolic = issymbolic(log_item.memlog)
+                    is_something_symbolic = is_log_symbolic or is_something_symbolic
+                    logs_summary.write("Memlog: %s %s\n" % (state.solve_one(log_item.memlog).encode('hex'), flagged(is_log_symbolic)))
+                    logs_summary.write("Topics:\n")
+                    for topic in log_item.topics:
+                        logs_summary.write("\t%d) %x %s" %(log_item.topics.index(topic), state.solve_one(topic), flagged(issymbolic(topic))))
             else:
-                output.write('\t%x %d wei\n'%(address, account['balance']))
+                logs_summary.write('No logs\n')
 
-        if world.logs:
-            output.write('LOGS:\n')
-            for address, memlog, topics in world.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)
+        with testcase.open_stream('constraints') as smt_summary:
+            smt_summary.write(str(state.constraints))
 
-                    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)
-
-                    output.write('\t %s: %r %s\n' %( hex(res1), ''.join(map(chr,res)), topics))
-                except Exception,e:
-                    output.write('\t %r %r %r\n' % (address,  repr(memlog), topics))
-
-        output.write('INPUT SYMBOLS\n')
-        for expr in state.input_symbols:
-            res = state.solve_one(expr)
-            if isinstance(expr, Array):
-                state.constrain(compare_buffers(expr, res))
-            else:
-                state.constrain(expr== res)
-   
+        with testcase.open_stream('pkl') as statef:
             try:
-                output.write('\t %s: %s\n'%( expr.name, res.encode('hex')))
-            except:
-                output.write('\t %s: %s\n'% (expr.name, res))
+                statef.write(pickle.dumps(state, 2))
+            except RuntimeError:
+                # recursion exceeded. try a slower, iterative solution
+                from .utils import iterpickle
+                logger.debug("Using iterpickle to dump state")
+                statef.write(iterpickle.dumps(state, 2))
+
+
+
+    def finalize(self):
+        #move runnign states to final states list
+        # and generate a testcase for each
+        lst = tuple(self.running_state_ids)
+        for state_id in lst:
+            self.terminate_state_id(state_id)
+
+        #delete actual streams from storage
+        for state_id in self.all_state_ids:
+            self._executor._workspace.rm_state(state_id)
+
+        #clean up lists
+        with self.locked_context('seth') as seth_context:
+            seth_context['_saved_states'] = []
+        with self.locked_context('seth') as seth_context:
+            seth_context['_final_states'] = []
         
-        #print "Constraints:"
-        #print state.constraints
-
-        tx = state.context['tx']
-        def x(expr):
-            if issymbolic(expr):
-                res = state.solve_one(expr)
-                if isinstance(expr, Array):
-                    state.constrain(compare_buffers(expr, res))
-                else:
-                    state.constrain(expr == res)
-                expr=res
-            if isinstance(expr, tuple):
-                expr = ''.join(expr)
-            return expr
-        tx_num = 0
-        for ty, caller, address, value, data in tx:
-            tx_num += 1
-            def consume_type(ty, data, offset):
-                if ty == u'uint256':
-                    return '0x'+data[offset:offset+64], offset+32*2
-                elif ty == u'address':
-                    return '0x'+data[offset+24:offset+64], offset+32*2
-                elif ty == u'int256':
-                    value = int('0x'+data[offset:offset+64],16)
-                    mask = 2**(256 - 1)
-                    value = -(value & mask) + (value & ~mask)
-                    return value, offset+32*2
-                elif ty == u'':
-                    return '', offset
-                elif ty in (u'bytes', u'string'):
-                    dyn_offset = (4 + int('0x'+data[offset:offset+64],16))*2
-                    size = int('0x'+data[dyn_offset:dyn_offset+64],16)
-                    return data[dyn_offset+64:dyn_offset+64+size*2],offset+8
-                else:
-                    raise NotImplemented(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 
+        #global summary
+        with self._output.save_stream('global.summary') as global_summary :
+            # (accounts created by contract code are not in this list )
+            global_summary.write( "Global coverage:\n")
+            for address in self.contract_accounts: 
+                global_summary.write("%x: %d%%\n" % (address, self.global_coverage(address))) #coverage % for address in this state
 
 
-            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')
-            output.write('\t Data: %s\n'% xdata)
-            if ty == 'CALL':
-                done = False
-                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]
-                    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)
-                        output.write('%s'%val)
-                    output.write(')\n')
-                except Exception,e:
-                    output.write('%s %s\n'%(e, xdata))
-        return output.getvalue()
+            if len(self.global_findings):
+                global_summary.write( "Global Findings:\n")
+
+                for address, pc, finding in self.global_findings:
+                    global_summary.write('- %s -\n' % finding )
+                    global_summary.write( '\t Contract: %s\n' % address )
+                    global_summary.write( '\t Program counter: %s\n' % pc )
+                    md = self.get_metadata(address)
+                    if md is not None:
+                        src = md.get_source_for(pc)
+                        global_summary.write( '\t Snippet:\n' )
+                        global_summary.write( '\n'.join(('\t\t'+x for x in src.split('\n'))) )
+                        global_summary.write( '\n\n' )
+
+
+            md = self.get_metadata(address)
+            if md is not None and len(md.warnings)>0:
+                global_summary.write( '\n\nCompiler warnings for %s:\n' % md.name )
+                global_summary.write( md.warnings )
+
+        for address, md in self.metadata.items():
+            with self._output.save_stream('global_%s.sol'%md.name) as global_src :
+                global_src.write(md.source_code)
+            with self._output.save_stream('global_%s.runtime_bytecode'%md.name) as global_runtime_bytecode :
+                global_runtime_bytecode.write(md.runtime_bytecode)
+            with self._output.save_stream('global_%s.init_bytecode'%md.name) as global_init_bytecode :
+                global_init_bytecode.write(md.init_bytecode)
+
+
+            with self._output.save_stream('global_%s.runtime_asm'%md.name) as global_runtime_asm :
+                runtime_bytecode = md.runtime_bytecode
+
+                with self.locked_context('runtime_coverage') as seen:
+
+                    count, total = 0, 0
+                    for i in evm.EVMAsm.disassemble_all(runtime_bytecode) :
+                        if (address, i.offset) in seen:
+                            count += 1
+                            global_runtime_asm.write( '*') 
+                        else:
+                            global_runtime_asm.write( ' ') 
+
+                        global_runtime_asm.write('%4x: %s\n'%(i.offset, i))
+                        total += 1
+
+            with self._output.save_stream('global_%s.init_asm'%md.name) as global_init_asm :
+                with self.locked_context('init_coverage') as seen:
+                    count, total = 0, 0
+                    for i in evm.EVMAsm.disassemble_all(md.init_bytecode) :
+                        if (address, i.offset) in seen:
+                            count += 1
+                            global_init_asm.write( '*') 
+                        else:
+                            global_init_asm.write( ' ') 
+
+                        global_init_asm.write('%4x: %s\n'%(i.offset, i))
+                        total += 1
+
+            with self._output.save_stream('global_%s.init_visited'%md.name) as f :
+                with self.locked_context('init_coverage') as seen:
+                    visited = set((o for (a,o) in seen if a == address))
+                    for o in sorted(visited):
+                        f.write('0x%x\n'%o)
+
+            with self._output.save_stream('global_%s.runtime_visited'%md.name) as f :
+                with self.locked_context('runtime_coverage') as seen:
+                    visited = set()
+                    for (a,o) in seen:
+                        if a == address:
+                            visited.add(o)
+                    for o in sorted(visited):
+                        f.write('0x%x\n'%o)
+
+
+        logger.info("[+] Look for results in %s", self.workspace )
 
     def global_coverage(self, account_address):
         ''' Returns code coverage for the contract on `account_address`.
@@ -1082,71 +1239,21 @@ class ManticoreEVM(Manticore):
             if account_address in world.storage:
                 break
 
-        seen = self.context['coverage'] #.union( self.context.get('code_data', set()))
-        runtime_bytecode = world.storage[account_address]['code']
 
-        end = None
-        if  ''.join(runtime_bytecode[-44: -34]) =='\x00\xa1\x65\x62\x7a\x7a\x72\x30\x58\x20' \
-            and  ''.join(runtime_bytecode[-2:]) =='\x00\x29':
-            end = -9-33-2  #Size of metadata at the end of most contracts
+        with self.locked_context('runtime_coverage') as coverage:
+            seen = coverage
+        #runtime_bytecode = world.storage[account_address]['code']
+        runtime_bytecode = self.get_metadata(account_address).runtime_bytecode
 
         count, total = 0, 0
-        for i in evm.EVMAsm.disassemble_all(runtime_bytecode[:end]) :
+        for i in evm.EVMAsm.disassemble_all(runtime_bytecode) :
             if (account_address, i.offset) in seen:
                 count += 1            
             total += 1
 
         return count*100.0/total
 
-    def report_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
-        #Search one state in which the account_address exists
-        world=None
-        for state_id in self.all_state_ids:
-            world = self.get_world(state_id)
-            if account_address in world.storage:
-                break
-
-        seen = self.context['coverage'] #.union( self.context.get('code_data', set()))
-        runtime_bytecode = world.storage[account_address]['code']
-        class bcolors:
-            HEADER = '\033[95m'
-            OKBLUE = '\033[94m'
-            OKGREEN = '\033[92m'
-            WARNING = '\033[93m'
-            FAIL = '\033[91m'
-            ENDC = '\033[0m'
-            BOLD = '\033[1m'
-            UNDERLINE = '\033[4m'
-
-
-        end = None
-        if  ''.join(runtime_bytecode[-44: -34]) =='\x00\xa1\x65\x62\x7a\x7a\x72\x30\x58\x20' \
-            and  ''.join(runtime_bytecode[-2:]) =='\x00\x29':
-            end = -9-33-2
-
-
-        output = ''
-        offset = 0
-        count = 0
-        total = 0
-        for i in evm.EVMAsm.disassemble_all(runtime_bytecode[:end]) :
-            
-            if (account_address, offset) in seen:
-                output += bcolors.OKGREEN
-                output += "** 0x%04x %s\n"%(offset, i)
-                output += bcolors.ENDC
-                count += 1
-            else:
-                output += "   0x%04x %s\n"%(offset, i)
-            
-            total += 1
-            offset += i.size
-
-        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
+    #TODO: find a better way to suppress execution of Manticore._did_finish_run_callback    
+    def _did_finish_run_callback(self):
+        _shared_context = self.context
+