diff --git a/manticore/__main__.py b/manticore/__main__.py
index f666a97a..efc1e90e 100644
--- a/manticore/__main__.py
+++ b/manticore/__main__.py
@@ -95,7 +95,10 @@ def parse_arguments():
                         help='Enable detection of reentrancy bug (Ethereum only)')
 
     parser.add_argument('--detect-unused-retval', action='store_true',
-                        help='Enable detection of not used internal transaction return value')
+                        help='Enable detection of not used internal transaction return value (Ethereum only)')
+
+    parser.add_argument('--detect-delegatecall', action='store_true',
+                        help='Enable detection of problematic uses of DELEGATECALL instruction (Ethereum only)')
 
     parser.add_argument('--detect-selfdestruct', action='store_true',
                         help='Enable detection of reachable selfdestruct instructions')
@@ -131,7 +134,8 @@ def parse_arguments():
 
 
 def ethereum_cli(args):
-    from .ethereum import ManticoreEVM, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, FilterFunctions, DetectUnusedRetVal, DetectSelfdestruct, LoopDepthLimiter, DetectExternalCallAndLeak, DetectReentrancySimple, DetectEnvInstruction
+    from .ethereum import ManticoreEVM, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, FilterFunctions, DetectReentrancySimple, DetectUnusedRetVal, DetectSelfdestruct, LoopDepthLimiter, DetectDelegatecall, DetectExternalCallAndLeak, DetectReentrancySimple, DetectEnvInstruction
+
     log.init_logging()
 
     m = ManticoreEVM(procs=args.procs, workspace_url=args.workspace)
@@ -148,6 +152,8 @@ def ethereum_cli(args):
         m.register_detector(DetectReentrancySimple())
     if args.detect_all or args.detect_unused_retval:
         m.register_detector(DetectUnusedRetVal())
+    if args.detect_all or args.detect_delegatecall:
+        m.register_detector(DetectDelegatecall())
     if args.detect_all or args.detect_selfdestruct:
         m.register_detector(DetectSelfdestruct())
     if args.detect_all or args.detect_externalcall:
diff --git a/manticore/core/smtlib/constraints.py b/manticore/core/smtlib/constraints.py
index be01c479..c398e84c 100644
--- a/manticore/core/smtlib/constraints.py
+++ b/manticore/core/smtlib/constraints.py
@@ -51,7 +51,6 @@ class ConstraintSet(object):
         :param check: Currently unused.
         :return:
         '''
-        # XXX(yan): check is an unused param
         if isinstance(constraint, bool):
             constraint = BoolConstant(constraint)
         assert isinstance(constraint, Bool)
@@ -72,6 +71,11 @@ class ConstraintSet(object):
 
         self._constraints.append(constraint)
 
+        if check:
+            from manticore.core.smtlib import solver
+            if not solver.check(self):
+                raise ValueError("Added an impossible constraint")
+
     def _get_sid(self):
         ''' Returns an unique id. '''
         assert self._child is None
diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py
index acdd8c34..f83c2e22 100644
--- a/manticore/core/smtlib/expression.py
+++ b/manticore/core/smtlib/expression.py
@@ -635,7 +635,8 @@ class Array(Expression):
         return self._index_max
 
     def select(self, index):
-        return ArraySelect(self, self.cast_index(index))
+        index = self.cast_index(index)
+        return ArraySelect(self, index)
 
     def store(self, index, value):
         return ArrayStore(self, self.cast_index(index), self.cast_value(value))
diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py
index 2ee32d4e..27fdf92b 100644
--- a/manticore/core/smtlib/solver.py
+++ b/manticore/core/smtlib/solver.py
@@ -308,17 +308,27 @@ class Z3Solver(Solver):
             return expression
         assert isinstance(expression, Variable)
 
-        self._send('(get-value (%s))' % expression.name)
-        ret = self._recv()
-        assert ret.startswith('((') and ret.endswith('))'), ret
+        if isinstance(expression, Array):
+            result = bytearray()
+            for c in expression:
+                expression_str = translate_to_smtlib(c)
+                self._send('(get-value (%s))' % expression_str)
+                response = self._recv()
+                result.append(int('0x{:s}'.format(response.split(expression_str)[1][3:-2]), 16))
+            return bytes(result)
+        else:
+            self._send('(get-value (%s))' % expression.name)
+            ret = self._recv()
+            assert ret.startswith('((') and ret.endswith('))'), ret
+
+            if isinstance(expression, Bool):
+                return {'true': True, 'false': False}[ret[2:-2].split(' ')[1]]
+            elif isinstance(expression, BitVec):
+                pattern, base = self._get_value_fmt
+                m = pattern.match(ret)
+                expr, value = m.group('expr'), m.group('value')
+                return int(value, base)
 
-        if isinstance(expression, Bool):
-            return {'true': True, 'false': False}[ret[2:-2].split(' ')[1]]
-        elif isinstance(expression, BitVec):
-            pattern, base = self._get_value_fmt
-            m = pattern.match(ret)
-            expr, value = m.group('expr'), m.group('value')
-            return int(value, base)
         raise NotImplementedError("_getvalue only implemented for Bool and BitVec")
 
     # push pop
@@ -361,6 +371,8 @@ class Z3Solver(Solver):
                 var = temp_cs.new_bool()
             elif isinstance(expression, BitVec):
                 var = temp_cs.new_bitvec(expression.size)
+            elif isinstance(expression, Array):
+                var = temp_cs.new_array(index_max=expression.index_max, value_bits=expression.value_bits, taint=expression.taint).array
             else:
                 raise NotImplementedError("get_all_values only implemented for Bool and BitVec")
 
diff --git a/manticore/core/smtlib/visitors.py b/manticore/core/smtlib/visitors.py
index 28a7af9f..911bdbe0 100644
--- a/manticore/core/smtlib/visitors.py
+++ b/manticore/core/smtlib/visitors.py
@@ -393,15 +393,18 @@ class ArithmeticSimplifier(Visitor):
             return BitVecITE(expression.size, *operands, taint=expression.taint)
 
     def visit_BitVecExtract(self, expression, *operands):
-        ''' extract(0,sizeof(a))(a)  ==> a
-            extract(0, 16 )( concat(a,b,c,d) ) => concat(c, d)
+        ''' extract(sizeof(a), 0)(a)  ==> a
+            extract(16, 0)( concat(a,b,c,d) ) => concat(c, d)
             extract(m,M)(and/or/xor a b ) => and/or/xor((extract(m,M) a) (extract(m,M) a)
         '''
         op = expression.operands[0]
         begining = expression.begining
         end = expression.end
 
-        if isinstance(op, BitVecConcat):
+        # extract(sizeof(a), 0)(a)  ==> a
+        if begining == 0 and end + 1 == op.size:
+            return op
+        elif isinstance(op, BitVecConcat):
             new_operands = []
             bitcount = 0
             for item in reversed(op.operands):
@@ -515,6 +518,7 @@ class ArithmeticSimplifier(Visitor):
 
         if isinstance(index, BitVecConstant):
             ival = index.value
+
             # props are slow and using them tight loops should be avoided, esp when they offer no additional validation
             # arr._operands[1] = arr.index, arr._operands[0] = arr.array
             while isinstance(arr, ArrayStore) and isinstance(arr._operands[1], BitVecConstant) and arr._operands[1]._value != ival:
diff --git a/manticore/core/state.py b/manticore/core/state.py
index 72e80c83..0eeb0b73 100644
--- a/manticore/core/state.py
+++ b/manticore/core/state.py
@@ -35,7 +35,9 @@ class Concretize(StateException):
     '''
     _ValidPolicies = ['MINMAX', 'ALL', 'SAMPLED', 'ONE']
 
-    def __init__(self, message, expression, setstate=None, policy='ALL', **kwargs):
+    def __init__(self, message, expression, setstate=None, policy=None, **kwargs):
+        if policy is None:
+            policy = 'ALL'
         if policy not in self._ValidPolicies:
             raise Exception("Policy (%s) must be one of: %s" % (policy, ', '.join(self._ValidPolicies),))
         self.expression = expression
@@ -107,13 +109,14 @@ class State(Eventful):
         self.forward_events_from(self._platform)
 
     # Fixme(felipe) change for with "state.cow_copy() as st_temp":.
+    # This need to change. this is the center of ALL the problems. re. CoW
     def __enter__(self):
         assert self._child is None
         self._platform.constraints = None
-        new_state = State(self._constraints.__enter__(), copy.deepcopy(self._platform))
+        new_state = State(self._constraints.__enter__(), self._platform)
         self.platform.constraints = new_state.constraints
         new_state._input_symbols = list(self._input_symbols)
-        new_state._context = copy.deepcopy(self._context)
+        new_state._context = copy.copy(self._context)
         self._child = new_state
         assert new_state.platform.constraints is new_state.constraints
 
@@ -245,7 +248,7 @@ class State(Eventful):
         self._input_symbols.append(expr)
         return expr
 
-    def concretize(self, symbolic, policy, maxcount=5):
+    def concretize(self, symbolic, policy, maxcount=7):
         ''' This finds a set of solutions for symbolic using policy.
             This raises TooManySolutions if more solutions than maxcount
         '''
@@ -253,6 +256,10 @@ class State(Eventful):
         vals = []
         if policy == 'MINMAX':
             vals = self._solver.minmax(self._constraints, symbolic)
+        elif policy == 'MAX':
+            vals = self._solver.max(self._constraints, symbolic)
+        elif policy == 'MIN':
+            vals = self._solver.min(self._constraints, symbolic)
         elif policy == 'SAMPLED':
             m, M = self._solver.minmax(self._constraints, symbolic)
             vals += [m, M]
@@ -260,14 +267,19 @@ class State(Eventful):
                 if self._solver.can_be_true(self._constraints, symbolic == (m + M) // 2):
                     vals.append((m + M) // 2)
             if M - m > 100:
+                for i in (0, 1, 2, 5, 32, 64, 128, 320):
+                    if self._solver.can_be_true(self._constraints, symbolic == m + i):
+                        vals.append(m + i)
+                    if maxcount <= len(vals):
+                        break
+            if M - m > 1000 and maxcount > len(vals):
                 vals += self._solver.get_all_values(self._constraints, symbolic,
-                                                    maxcnt=maxcount, silent=True)
+                                                    maxcnt=maxcount - len(vals), silent=True)
         elif policy == 'ONE':
             vals = [self._solver.get_value(self._constraints, symbolic)]
         else:
             assert policy == 'ALL'
-            vals = solver.get_all_values(self._constraints, symbolic, maxcnt=maxcount,
-                                         silent=False)
+            vals = solver.get_all_values(self._constraints, symbolic, maxcnt=maxcount, silent=True)
 
         return tuple(set(vals))
 
diff --git a/manticore/ethereum.py b/manticore/ethereum.py
index 0d9a4fb4..2e4fdde8 100644
--- a/manticore/ethereum.py
+++ b/manticore/ethereum.py
@@ -125,7 +125,6 @@ class FilterFunctions(Plugin):
                 #Avoid all not selected hashes
                 for func_hsh in md.hashes:
                     if func_hsh in selected_functions:
-                        # Was constraint = Operators.NOT(tx.data[:4] == func_hsh)
                         constraint = tx.data[:4] != func_hsh
                         state.constrain(constraint)
 
@@ -642,6 +641,38 @@ class DetectUnusedRetVal(Detector):
                 self._remove_retval_taint(state, used_taint)
 
 
+class DetectDelegatecall(Detector):
+    '''
+        Detects DELEGATECALLs to controlled addresses and or with controlled function id.
+        This detector finds and reports on any delegatecall instruction any the following propositions are hold:
+            * the destination address can be controlled by the caller
+            * the first 4 bytes of the calldata are controlled by the caller
+    '''
+
+    def will_evm_execute_instruction_callback(self, state, instruction, arguments):
+        world = state.platform
+        mnemonic = instruction.semantics
+        current_vm = world.current_vm
+        # If it executed a DELEGATECALL
+        # TODO: Check the transaction was success
+        # if blockchain.last_transaction.return_value:
+        # TODO: check if any of the potential target addresses has code
+        # if not any( world.get_code, possible_addresses):
+        if mnemonic == 'DELEGATECALL':
+            gas, address, in_offset, in_size, out_offset, out_size = arguments
+            if issymbolic(address):
+                possible_addresses = state.solve_n(address, 2)
+                if len(possible_addresses) > 1:
+                    self.add_finding_here(state, "Delegatecall to user controlled address")
+
+            calldata = world.current_vm.read_buffer(in_offset, in_size)
+            func_id = calldata[:4]
+            if issymbolic(func_id):
+                possible_func_ids = state.solve_n(func_id, 2)
+                if len(possible_func_ids) > 1:
+                    self.add_finding_here(state, "Delegatecall to user controlled function")
+
+
 class DetectUninitializedMemory(Detector):
     """
         Detects uses of uninitialized memory
@@ -1532,6 +1563,7 @@ class ManticoreEVM(Manticore):
                 output, warnings = ManticoreEVM._run_solc(temp, solc_bin, solc_remaps)
         elif isinstance(source_code, io.IOBase):
             output, warnings = ManticoreEVM._run_solc(source_code, solc_bin, solc_remaps)
+            source_code.seek(0)
             source_code = source_code.read()
         else:
             raise TypeError
@@ -1597,7 +1629,7 @@ class ManticoreEVM(Manticore):
         # Make the constraint store
         constraints = ConstraintSet()
         # make the ethereum world state
-        world = evm.EVMWorld(constraints)
+        world = evm.EVMWorld(constraints, initial_timestamp=1524785992)
         initial_state = State(constraints, world)
         super().__init__(initial_state, **kwargs)
 
@@ -1829,7 +1861,7 @@ class ManticoreEVM(Manticore):
             return None
         return contract_account
 
-    def create_contract(self, owner, balance=0, address=None, init=None, name=None):
+    def create_contract(self, owner, balance=0, address=None, init=None, name=None, gas=21000):
         """ Creates a contract
 
             :param owner: owner account (will be default caller in any transactions)
@@ -1839,6 +1871,7 @@ class ManticoreEVM(Manticore):
             :param int address: the address for the new contract (optional)
             :param str init: initializing evm bytecode and arguments
             :param str name: a uniq name for reference
+            :param gas: gas budget for the creation/inititialization of the contract
             :rtype: EVMAccount
         """
         if not self.count_running_states():
@@ -1859,7 +1892,7 @@ class ManticoreEVM(Manticore):
             # Account name already used
             raise EthereumError("Name already used")
 
-        self._transaction('CREATE', owner, balance, address, data=init)
+        self._transaction('CREATE', owner, balance, address, data=init, gaslimit=gas)
         # TODO detect failure in the constructor
 
         self._accounts[name] = EVMContract(address=address, manticore=self, default_caller=owner, name=name)
@@ -1884,7 +1917,7 @@ class ManticoreEVM(Manticore):
             return self.new_address()
         return new_address
 
-    def transaction(self, caller, address, value, data):
+    def transaction(self, caller, address, value, data, gas=21000):
         """ Issue a symbolic transaction in all running states
 
             :param caller: the address of the account sending the transaction
@@ -1894,9 +1927,10 @@ class ManticoreEVM(Manticore):
             :param value: balance to be transfered on creation
             :type value: int or SValue
             :param data: initial data
+            :param gas: gas budget
             :raises NoAliveStates: if there are no alive states to execute
         """
-        self._transaction('CALL', caller, value=value, address=address, data=data)
+        self._transaction('CALL', caller, value=value, address=address, data=data, gaslimit=gas)
 
     def create_account(self, balance=0, address=None, code=None, name=None):
         """ Low level creates an account. This won't generate a transaction.
@@ -1994,8 +2028,8 @@ class ManticoreEVM(Manticore):
 
             return caller, address, value, data
 
-    def _transaction(self, sort, caller, value=0, address=None, data=None, price=1):
-        """ Creates a contract
+    def _transaction(self, sort, caller, value=0, address=None, data=None, gaslimit=0, price=1):
+        """ Initiates a transaction
 
             :param caller: caller account
             :type caller: int or EVMAccount
@@ -2004,6 +2038,7 @@ class ManticoreEVM(Manticore):
             :param price: the price of gas for this transaction. Mostly unused.
             :type value: int or SValue
             :param str data: initializing evm bytecode and arguments or transaction call data
+            :param gaslimit: gas budget
             :rtype: EVMAccount
         """
         #Type Forgiveness
@@ -2071,7 +2106,7 @@ class ManticoreEVM(Manticore):
                     # Address already used
                     raise EthereumError("This is bad. Same address used for different contracts in different states")
 
-            state.context['_pending_transaction'] = (sort, caller, address, value, data, price)
+            state.context['_pending_transaction'] = (sort, caller, address, value, data, gaslimit, price)
 
         # run over potentially several states and
         # generating potentially several others
@@ -2119,7 +2154,8 @@ class ManticoreEVM(Manticore):
                 self.transaction(caller=tx_account[min(tx_no, len(tx_account) - 1)],
                                  address=contract_account,
                                  data=symbolic_data,
-                                 value=value)
+                                 value=value,
+                                 gas=2100000)
                 logger.info("%d alive states, %d terminated states", self.count_running_states(), self.count_terminated_states())
             except NoAliveStates:
                 break
@@ -2245,7 +2281,6 @@ class ManticoreEVM(Manticore):
                 results.append((data_concrete, data_hash))
                 known_hashes_cond = data_concrete == data
                 known_sha3.append((data_concrete, data_hash))
-
             not_known_hashes_cond = Operators.NOT(known_hashes_cond)
 
             # We need to fork/save the state
@@ -2323,14 +2358,14 @@ class ManticoreEVM(Manticore):
         if '_pending_transaction' not in state.context:
             return
         world = state.platform
-        ty, caller, address, value, data, price = state.context['_pending_transaction']
+        ty, caller, address, value, data, gaslimit, price = state.context['_pending_transaction']
         del state.context['_pending_transaction']
 
         if ty == 'CALL':
-            world.transaction(address=address, caller=caller, data=data, value=value, price=price)
+            world.transaction(address=address, caller=caller, data=data, value=value, price=price, gas=gaslimit)
         else:
             assert ty == 'CREATE'
-            world.create_contract(caller=caller, address=address, balance=value, init=data, price=price)
+            world.create_contract(caller=caller, address=address, balance=value, init=data, price=price, gas=gaslimit)
 
     def _did_evm_execute_instruction_callback(self, state, instruction, arguments, result):
         """ INTERNAL USE """
@@ -2466,7 +2501,6 @@ class ManticoreEVM(Manticore):
             # Accounts summary
             is_something_symbolic = False
             summary.write("%d accounts.\n" % len(blockchain.accounts))
-
             for account_address in blockchain.accounts:
                 is_account_address_symbolic = issymbolic(account_address)
                 account_address = state.solve_one(account_address)
@@ -2569,35 +2603,36 @@ class ManticoreEVM(Manticore):
 
                 if tx.sort == 'CALL':
                     if metadata is not None:
-                        function_id = state.solve_one(tx.data[:4])  # hope there is enough data
+                        calldata = state.solve_one(tx.data)
+                        is_calldata_symbolic = issymbolic(tx.data)
+
+                        function_id = calldata[:4]  # hope there is enough data
                         signature = metadata.get_func_signature(function_id)
                         function_name = metadata.get_func_name(function_id)
                         if signature:
-                            _, arguments = ABI.deserialize(signature, tx.data)
+                            _, arguments = ABI.deserialize(signature, calldata)
                         else:
-                            arguments = (tx.data,)
+                            arguments = (calldata,)
 
                         return_data = None
                         if tx.result == 'RETURN':
                             ret_types = metadata.get_func_return_types(function_id)
-                            return_data = ABI.deserialize(ret_types, tx.return_data)  # function return
+                            return_data = state.solve_one(tx.return_data)
+                            return_values = ABI.deserialize(ret_types, return_data)  # function return
+                            is_return_symbolic = issymbolic(tx.return_data)
 
                         tx_summary.write('\n')
                         tx_summary.write("Function call:\n")
                         tx_summary.write("%s(" % function_name)
-                        tx_summary.write(','.join(map(repr, 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)))
+                        tx_summary.write(','.join(map(repr, arguments)))
+                        tx_summary.write(') -> %s %s\n' % (tx.result, flagged(is_calldata_symbolic)))
 
                         if return_data is not None:
-                            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
+                        is_something_symbolic = is_calldata_symbolic or is_return_symbolic
 
                 tx_summary.write('\n\n')
 
@@ -2682,7 +2717,6 @@ class ManticoreEVM(Manticore):
                 q.put(state_id)
 
         report_workers = []
-
         for _ in range(self._config_procs):
             proc = Process(target=worker_finalize, args=(q,))
             proc.start()
diff --git a/manticore/manticore.py b/manticore/manticore.py
index 0b6e2779..dcc1d375 100644
--- a/manticore/manticore.py
+++ b/manticore/manticore.py
@@ -533,7 +533,7 @@ class Manticore(Eventful):
         # Everything is good add it.
         state.constraints.add(assertion)
 
-    ##########################################################################
+    ############################################################################
     # Some are placeholders Remove FIXME
     # Any platform specific callback should go to a plugin
 
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index dec56190..0d481bd9 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -252,16 +252,19 @@ def concretized_args(**policies):
                 if not issymbolic(args[index]):
                     continue
                 if not policy:
-                    raise ConcretizeStack(index)
+                    policy = 'MINMAX'
+
                 if policy == "ACCOUNTS":
-                    #special handler for EVM only policy
-                    address = args[index]
+                    value = args[index]
                     world = args[0].world
-                    cond = world._constraint_to_accounts(address, ty='both', include_zero=True)
+                    #special handler for EVM only policy
+                    cond = world._constraint_to_accounts(value, ty='both', include_zero=True)
                     world.constraints.add(cond)
                     policy = 'ALL'
+
                 raise ConcretizeStack(index, policy=policy)
             return func(*args, **kwargs)
+        wrapper.__signature__ = inspect.signature(func)
         return wrapper
     return concretizer
 
@@ -371,6 +374,12 @@ class EVM(Eventful):
         self._on_transaction = False  # for @transact
         self._checkpoint_data = None
 
+        # Used calldata size
+        min_size = 0
+        max_size = len(self.data)
+        self._used_calldata_size = 0
+        self._calldata_size = len(self.data)
+
     @property
     def bytecode(self):
         return self._bytecode
@@ -406,6 +415,8 @@ class EVM(Eventful):
         state['logs'] = self.logs
         state['_on_transaction'] = self._on_transaction
         state['_checkpoint_data'] = self._checkpoint_data
+        state['_used_calldata_size'] = self._used_calldata_size
+        state['_calldata_size'] = self._calldata_size
         return state
 
     def __setstate__(self, state):
@@ -425,9 +436,13 @@ class EVM(Eventful):
         self.stack = state['stack']
         self._allocated = state['allocated']
         self.suicides = state['suicides']
+        self._used_calldata_size = state['_used_calldata_size']
+        self._calldata_size = state['_calldata_size']
+
         super().__setstate__(state)
 
-    def _allocate(self, address):
+    def _get_memfee(self, address, size=1):
+        address = self.safe_add(address, size)
         allocated = self.allocated
         GMEMORY = 3
         GQUADRATICMEMDENOM = 512  # 1 gas per 512 quadwords
@@ -438,10 +453,12 @@ class EVM(Eventful):
         new_totalfee = self.safe_mul(new_size, GMEMORY) + Operators.UDIV(self.safe_mul(new_size, new_size), GQUADRATICMEMDENOM)
         memfee = new_totalfee - old_totalfee
         flag = Operators.UGT(new_totalfee, old_totalfee)
-        self._consume(Operators.ITEBV(512, flag, memfee, 0))
+        return Operators.ITEBV(512, flag, memfee, 0)
 
-        address_c = Operators.UDIV(self.safe_add(address, 31), 32) * 32
-        self._allocated = Operators.ITEBV(512, flag, Operators.ZEXTEND(address_c, 512), Operators.ZEXTEND(allocated, 512))
+    def _allocate(self, address):
+        self._consume(self._get_memfee(address))
+        address_c = Operators.ZEXTEND(Operators.UDIV(self.safe_add(address, 31), 32) * 32, 512)
+        self._allocated = Operators.ITEBV(512, address_c > self._allocated, address_c, self.allocated)
 
     @property
     def allocated(self):
@@ -546,33 +563,46 @@ class EVM(Eventful):
             if (fee.size != 512):
                 raise EthereumError("Fees should be 512 bit long")
 
-        self.constraints.add(Operators.UGE(fee, 0))
-        self.constraints.add(Operators.ULE(fee, self._gas))
-
         #FIXME add configurable checks here
-        if config.out_of_gas is not None:
-            if config.out_of_gas == 0:
-                #default to OOG exception if possible
-                if solver.can_be_true(self.constraints, self._gas < fee):
-                    self.constraints.add(Operators.UGT(fee, self.gas))
-                    logger.debug("Not enough gas for instruction")
-                    raise NotEnoughGas()
-            elif config.out_of_gas == 1:
-                #default to enough gas if possible
-                if solver.can_be_true(self.constraints, self._gas > fee):
-                    self.constraints.add(Operators.UGT(self.gas, fee))
+        config.out_of_gas = 3
+
+        # Iff both are concrete values...
+        if not issymbolic(self._gas) and not issymbolic(fee):
+            if self._gas < fee:
+                logger.debug("Not enough gas for instruction")
+                raise NotEnoughGas()
+        else:
+                if config.out_of_gas is None:
+                    # do nothing. gas could go negative.
+                    # memory could be accessed in great offsets
+                    pass
+                elif config.out_of_gas == 0:
+                    #explore only when OOG
+                    if solver.can_be_true(self.constraints, Operators.ULT(self.gas, fee)):
+                        self.constraints.add(Operators.UGT(fee, self.gas))
+                        logger.debug("Not enough gas for instruction")
+                        raise NotEnoughGas()
+                elif config.out_of_gas == 1:
+                    #explore only when there is enough gas if possible
+                    if solver.can_be_true(self.constraints, Operators.UGT(self.gas, fee)):
+                        self.constraints.add(Operators.UGT(self.gas, fee))
+                    else:
+                        logger.debug("Not enough gas for instruction")
+                        raise NotEnoughGas()
                 else:
-                    logger.debug("Not enough gas for instruction")
-                    raise NotEnoughGas()
-            else:
-                #fork on both options
-                if len(solver.get_all_values(self.constraints, self._gas > fee)) == 2:
-                    raise Concretize("Concretice gas fee",
-                                     expression=self._gas > fee,
-                                     setstate=None,
-                                     policy='ALL')
+                    #explore both options / fork
+                    enough_gas_solutions = solver.get_all_values(self.constraints, Operators.UGT(self._gas, fee))
+                    if len(enough_gas_solutions) == 2:
+                        raise Concretize("Concretice gas fee",
+                                         expression=Operators.UGT(self._gas, fee),
+                                         setstate=None,
+                                         policy='ALL')
+                    elif enough_gas_solutions[0] == False:
+                        logger.debug("Not enough gas for instruction")
+                        raise NotEnoughGas()
 
         self._gas -= fee
+        assert issymbolic(self._gas) or self._gas >= 0
 
     def _indemnify(self, fee):
         self._gas += fee
@@ -748,6 +778,31 @@ class EVM(Eventful):
         self.memory.write_BE(offset, value, size)
         for i in range(size):
             self._publish('did_evm_write_memory', offset + i, Operators.EXTRACT(value, (size - i - 1) * 8, 8))
+
+    def safe_add(self, a, b):
+        a = Operators.ZEXTEND(a, 512)
+        b = Operators.ZEXTEND(b, 512)
+        result = a + b
+        '''
+        if solver.can_be_true(self.constraints, Operators.ULT(result, 1 << 256)):
+            self.constraints.add(Operators.ULT(result, 1 << 256))
+        else:
+            raise ValueError("Integer overflow")
+        '''
+        return result
+
+    def safe_mul(self, a, b):
+        a = Operators.ZEXTEND(a, 512)
+        b = Operators.ZEXTEND(b, 512)
+        result = a * b
+        '''
+        if solver.can_be_true(self.constraints, Operators.ULT(result, 1 << 256)):
+            self.constraints.add(Operators.ULT(result, 1 << 256))
+        else:
+            raise ValueError("Integer overflow")
+        '''
+        return result
+
     ############################################################################
     #INSTRUCTIONS
 
@@ -839,11 +894,12 @@ class EVM(Eventful):
         EXP_SUPPLEMENTAL_GAS = 50   # cost of EXP exponent per byte
 
         def nbytes(e):
+            result = 32
             for i in range(32):
-                if e >> (i * 8) == 0:
-                    return i
-            return 32
+                result = Operators.ITEBV(512, Operators.EXTRACT(e, i, 8) == 0, i, result)
+            return result
         self._consume(EXP_SUPPLEMENTAL_GAS * nbytes(exponent))
+
         return pow(base, exponent, TT256)
 
     def SIGNEXTEND(self, size, value):
@@ -914,7 +970,7 @@ class EVM(Eventful):
                 concrete_data.append(simplified.value)
             else:
                 #simplify by solving. probably means that we need to improve simplification
-                solutions = solver.get_all_values(self.constraints, c, 2, silent=True)
+                solutions = solver.get_all_values(self.constraints, simplified, 2, silent=True)
                 if len(solutions) != 1:
                     break
                 concrete_data.append(solutions[0])
@@ -942,7 +998,6 @@ class EVM(Eventful):
             for key, hsh in known_sha3.items():
                 assert not issymbolic(key), "Saved sha3 data,hash pairs should be concrete"
                 cond = key == data
-
                 known_hashes_cond = Operators.OR(cond, known_hashes_cond)
                 value = Operators.ITEBV(256, cond, hsh, value)
             return value
@@ -979,6 +1034,14 @@ class EVM(Eventful):
 
     def CALLDATALOAD(self, offset):
         '''Get input data of current environment'''
+
+        if issymbolic(offset):
+            if solver.can_be_true(self._constraints, offset == self._used_calldata_size):
+                self.constraints.add(offset == self._used_calldata_size)
+            raise ConcretizeStack(1, policy='SAMPLED')
+
+        self._use_calldata(offset + 32)
+
         data_length = len(self.data)
 
         bytes = []
@@ -992,33 +1055,38 @@ class EVM(Eventful):
             bytes.append(c)
         return Operators.CONCAT(256, *bytes)
 
+    def _use_calldata(self, n):
+        assert not issymbolic(n)
+        max_size = len(self.data)
+        min_size = self._used_calldata_size
+        self._used_calldata_size = Operators.ITEBV(256, min_size + n > max_size, max_size, min_size + n)
+
     def CALLDATASIZE(self):
         '''Get size of input data in current environment'''
-        return len(self.data)
+        return self._calldata_size
 
-    def safe_add(self, a, b):
-        a = Operators.ZEXTEND(a, 512)
-        b = Operators.ZEXTEND(b, 512)
-        result = a + b
-        self.constraints.add(Operators.UGE(result, 0))
-        self.constraints.add(Operators.ULT(result, 1 << 256))
-        return result
-
-    def safe_mul(self, a, b):
-        a = Operators.ZEXTEND(a, 512)
-        b = Operators.ZEXTEND(b, 512)
-        result = a * b
-        self.constraints.add(Operators.UGE(result, 0))
-        self.constraints.add(Operators.ULT(result, 1 << 256))
-        return result
-
-    @concretized_args(size='SAMPLED')
     def CALLDATACOPY(self, mem_offset, data_offset, size):
         '''Copy input data in current environment to memory'''
-        GCOPY = 3             # cost to copy one 32 byte word
-        self._consume(self.safe_mul(GCOPY, self.safe_add(size, 31) // 32))
-        self._allocate(self.safe_add(mem_offset, size))
 
+        if issymbolic(size):
+            if solver.can_be_true(self._constraints, size <= len(self.data) + 32):
+                self.constraints.add(size <= len(self.data) + 32)
+            raise ConcretizeStack(3, policy='SAMPLED')
+
+        if issymbolic(data_offset):
+            if solver.can_be_true(self._constraints, data_offset == self._used_calldata_size):
+                self.constraints.add(data_offset == self._used_calldata_size)
+            raise ConcretizeStack(2, policy='SAMPLED')
+
+        GCOPY = 3             # cost to copy one 32 byte word
+        self._use_calldata(data_offset + size)
+        copyfee = self.safe_mul(GCOPY, self.safe_add(size, 31) // 32)
+        memfee = self._get_memfee(mem_offset, size)
+
+        self._consume(copyfee)
+        self._consume(memfee)
+
+        self._allocate(self.safe_add(mem_offset, size))
         for i in range(size):
             try:
                 c = Operators.ITEBV(8, data_offset + i < len(self.data), Operators.ORD(self.data[data_offset + i]), 0)
@@ -1031,6 +1099,7 @@ class EVM(Eventful):
         '''Get size of code running in current environment'''
         return len(self.bytecode)
 
+    @concretized_args(code_offset='SAMPLED', size='SAMPLED')
     def CODECOPY(self, mem_offset, code_offset, size):
         '''Copy code running in current environment to memory'''
 
@@ -1043,21 +1112,20 @@ class EVM(Eventful):
 
         for i in range(max_size):
             if issymbolic(i < size):
-                default = Operators.ITEBV(256, i < size, 0, self._load(mem_offset + i))  # Fixme. unnecessary memory read
+                default = Operators.ITEBV(8, i < size, 0, self._load(mem_offset + i, 1))  # Fixme. unnecessary memory read
             else:
                 if i < size:
                     default = 0
                 else:
-                    default = self._load(mem_offset + i)
+                    default = self._load(mem_offset + i, 1)
 
             if issymbolic(code_offset):
-                value = Operators.ITEBV(256, code_offset + i >= len(self.bytecode), default, self.bytecode[code_offset + i])
+                value = Operators.ITEBV(8, code_offset + i >= len(self.bytecode), default, self.bytecode[code_offset + i])
             else:
                 if code_offset + i >= len(self.bytecode):
                     value = default
                 else:
                     value = self.bytecode[code_offset + i]
-
             self._store(mem_offset + i, value)
         self._publish('did_evm_read_code', code_offset, size)
 
@@ -1281,7 +1349,7 @@ class EVM(Eventful):
                                      data=self.read_buffer(in_offset, in_size),
                                      caller=self.address,
                                      value=value,
-                                     gas=self.gas)
+                                     gas=gas)
         raise StartTx()
 
     @CALLCODE.pos
@@ -1308,7 +1376,7 @@ class EVM(Eventful):
                                      data=self.read_buffer(in_offset, in_size),
                                      caller=self.address,
                                      value=0,
-                                     gas=self.gas)
+                                     gas=gas)
         raise StartTx()
 
     @DELEGATECALL.pos
@@ -1330,7 +1398,7 @@ class EVM(Eventful):
                                      data=self.read_buffer(in_offset, in_size),
                                      caller=self.address,
                                      value=0,
-                                     gas=self.gas)
+                                     gas=gas)
         raise StartTx()
 
     @STATICCALL.pos
@@ -1416,7 +1484,7 @@ class EVM(Eventful):
             result.append('<Symbolic PC> {:s} {}'.format((translate_to_smtlib(pc), pc.taint)))
         else:
             operands_str = self.instruction.has_operand and '0x{:x}'.format(self.instruction.operand) or ''
-            result.append('0x%04x: {:s} {:s} {:s}\n'.format((pc, self.instruction.name, operands_str, self.instruction.description)))
+            result.append('0x{:04x}: {:s} {:s} {:s}\n'.format(pc, self.instruction.name, operands_str, self.instruction.description))
 
         args = {}
         implementation = getattr(self, self.instruction.semantics, None)
@@ -1556,7 +1624,7 @@ class EVMWorld(Platform):
             address = tx.caller
             assert value == 0
 
-        vm = EVM(self._constraints, address, data, caller, value, bytecode, world=self)
+        vm = EVM(self._constraints, address, data, caller, value, bytecode, world=self, gas=gas)
 
         self._publish('will_open_transaction', tx)
         self._callstack.append((tx, self.logs, self.deleted_accounts, copy.copy(self.get_storage(address)), vm))
@@ -1899,7 +1967,7 @@ class EVMWorld(Platform):
 
         return address
 
-    def create_contract(self, price=0, address=None, caller=None, balance=0, init=None):
+    def create_contract(self, price=0, address=None, caller=None, balance=0, init=None, gas=2300):
         '''
         The way that the Solidity compiler expects the constructor arguments to
         be passed is by appending the arguments to the byte code produced by the
@@ -1910,12 +1978,12 @@ class EVMWorld(Platform):
         on the network.
         '''
         address = self.create_account(address)
-        self.start_transaction('CREATE', address, price, init, caller, balance)
+        self.start_transaction('CREATE', address, price, init, caller, balance, gas=gas)
         self._process_pending_transaction()
         return address
 
-    def transaction(self, address, price=0, data='', caller=None, value=0):
-        self.start_transaction('CALL', address, price=price, data=data, caller=caller, value=value)
+    def transaction(self, address, price=0, data='', caller=None, value=0, gas=2300):
+        self.start_transaction('CALL', address, price=price, data=data, caller=caller, value=value, gas=gas)
         self._process_pending_transaction()
 
     def start_transaction(self, sort, address, price=None, data=None, caller=None, value=0, gas=2300):
@@ -2019,7 +2087,7 @@ class EVMWorld(Platform):
 
             if set(enough_balance_solutions) == {True, False}:
                 raise Concretize('Forking on available funds',
-                                 expression=Operators.ULT(src_balance, value),
+                                 expression=enough_balance,
                                  setstate=lambda a, b: None,
                                  policy='ALL')
             failed = set(enough_balance_solutions) == {False}
diff --git a/manticore/utils/helpers.py b/manticore/utils/helpers.py
index a16dca3f..5530afa7 100644
--- a/manticore/utils/helpers.py
+++ b/manticore/utils/helpers.py
@@ -4,6 +4,7 @@ import logging
 import pickle
 import re
 import sys
+import resource
 
 from collections import OrderedDict
 from ..core.smtlib import Expression, BitVecConstant
@@ -129,7 +130,7 @@ class StateSerializer(object):
 
 
 class PickleSerializer(StateSerializer):
-    DEFAULT_RECURSION: int = 0x100000  # 1M
+    DEFAULT_RECURSION: int = 0x10000  # 1M
     MAX_RECURSION: int = 0x1000000  # 16.7M
 
     def __init__(self):
diff --git a/tests/binaries/detectors/delegatecall_not_ok.sol b/tests/binaries/detectors/delegatecall_not_ok.sol
new file mode 100644
index 00000000..4f8abb82
--- /dev/null
+++ b/tests/binaries/detectors/delegatecall_not_ok.sol
@@ -0,0 +1,26 @@
+pragma solidity ^0.4.24;
+/*
+There is a dangerous use of lowlevel instruction delegatecall in the fallback function.
+The address to which the delegatecall tx is sent is controlled by any user of this contract.
+The storage variable `addr` is initialized to `this` and it CAN be modified.
+The function selector of the delegate call is fully controlled by the user
+*/
+
+contract DetectThis {
+  address addr;
+  constructor(){
+     addr = address(this);
+  }
+  function setaddr(address a){
+     addr = a;
+  }
+
+  function default_call(bytes data) public {
+        require(msg.sender == address(this));
+        //do legal stuff on bytes
+  }
+
+  function () public {
+        require(addr.delegatecall(msg.data));
+  }
+}
diff --git a/tests/binaries/detectors/delegatecall_not_ok1.sol b/tests/binaries/detectors/delegatecall_not_ok1.sol
new file mode 100644
index 00000000..fe9a3d8c
--- /dev/null
+++ b/tests/binaries/detectors/delegatecall_not_ok1.sol
@@ -0,0 +1,34 @@
+pragma solidity ^0.4.24;
+/*
+There is a dangerous use of lowlevel instruction delegatecall in the fallback function.
+The target address of the delegatecall hardcoded function selector of the delegate 
+call is fully controlled by the user.
+*/
+
+contract DetectThis {
+  address addr;
+  constructor(){
+     addr = address(this);
+  }
+  function setaddr(address a){
+     addr = a;
+  }
+
+  function default_call(bytes data) public {
+        require(msg.sender == address(this));
+        //do legal stuff on bytes
+  }
+
+  function f() public {
+        require(msg.data.length >=4);
+        uint i;
+        bytes memory new_calldata = new bytes(msg.data.length-4);
+
+        for (i=0; i < msg.data.length-4; i++) {
+            new_calldata[i] = msg.data[i+4];
+        }
+
+        require(address(0x41414141).delegatecall(new_calldata));
+  }
+}
+
diff --git a/tests/binaries/detectors/delegatecall_ok.sol b/tests/binaries/detectors/delegatecall_ok.sol
new file mode 100644
index 00000000..6d6ecccf
--- /dev/null
+++ b/tests/binaries/detectors/delegatecall_ok.sol
@@ -0,0 +1,23 @@
+pragma solidity ^0.4.24;
+/*
+A fair use of delegatecall instruction is inserted by the solidity compiler for
+implementing libraries. This is an ok use of delegatecall.
+*/
+pragma solidity ^0.4.24;
+
+library Lib {
+  
+  struct Data {uint val;}
+
+  function set(Data storage self, uint new_val) public{
+    self.val = new_val;      
+  }
+}
+
+contract DetectThis {
+    Lib.Data public myVal;
+
+    function () public payable{
+        Lib.set(myVal, msg.value);
+    }
+}
diff --git a/tests/binaries/detectors/delegatecall_ok1.sol b/tests/binaries/detectors/delegatecall_ok1.sol
new file mode 100644
index 00000000..5a98dd76
--- /dev/null
+++ b/tests/binaries/detectors/delegatecall_ok1.sol
@@ -0,0 +1,18 @@
+pragma solidity ^0.4.24;
+/*
+There is a fair use of lowlevel instruction delegatecall in the fallback function.
+It is effectivelly a CALL to `default_call` with the full calldata that was givento the fallback function
+*/
+contract DetectThis {
+
+  function default_call(bytes data) public {
+        require(msg.sender == address(this));
+        //do legal stuff on bytes
+  }
+
+  function () public {
+        bool retval = address(this).delegatecall(bytes4(keccak256("default_call(bytes)")), msg.data);
+        require(retval);
+  }
+
+}
diff --git a/tests/binaries/detectors/delegatecall_ok2.sol b/tests/binaries/detectors/delegatecall_ok2.sol
new file mode 100644
index 00000000..e2364d4b
--- /dev/null
+++ b/tests/binaries/detectors/delegatecall_ok2.sol
@@ -0,0 +1,24 @@
+pragma solidity ^0.4.24;
+/*
+There is a fair use of lowlevel instruction delegatecall in the fallback function.
+It is effectivelly a CALL to `this.default_call` with a concrete data.
+The storage variable `addr` is initialized to `this` and can not be modified.
+*/
+
+contract DetectThis {
+  address addr;
+  constructor(){
+        addr = address(this);
+  }
+
+  function default_call(bytes data) public {
+        require(msg.sender == address(this));
+        //do legal stuff on bytes
+  }
+
+  function () public {
+        bool retval = addr.delegatecall(bytes4(keccak256("default_call(bytes)")), "Concrete values!");
+        require(retval);
+  }
+
+}
diff --git a/tests/binaries/detectors/delegatecall_ok3.sol b/tests/binaries/detectors/delegatecall_ok3.sol
new file mode 100644
index 00000000..761340d8
--- /dev/null
+++ b/tests/binaries/detectors/delegatecall_ok3.sol
@@ -0,0 +1,38 @@
+pragma solidity ^0.4.24;
+/*
+There is a dangerous use of lowlevel instruction delegatecall in the fallback function.
+The address to which the delegatecall tx is sent is controlled by any user of this contract.
+The storage variable `addr` is initialized to `this` and it CAN be modified.
+The function selector of the delegate call is fully controlled by the user
+*/
+
+contract DetectThis {
+  address addr;
+  constructor() public{
+     addr = address(this);
+  }
+
+  function default_call(bytes data) public {
+        require(msg.sender == address(this));
+        //do legal stuff on bytes
+  }
+
+  function () public {
+  	require(msg.data.length > 4);
+        uint i;
+        bytes memory new_calldata = new bytes(msg.data.length);
+        bytes4 func_id = bytes4(keccak256("default_call(bytes)"));
+        for (i=0; i < 4; i++) {
+            new_calldata[i] = func_id[i];
+        }
+
+        for (; i < msg.data.length; i++) {
+            new_calldata[i] = msg.data[i];
+        }
+
+      require(address(this).delegatecall(new_calldata));
+
+  }
+}
+
+
diff --git a/tests/eth_detectors.py b/tests/eth_detectors.py
index 31e22346..4ab7815c 100644
--- a/tests/eth_detectors.py
+++ b/tests/eth_detectors.py
@@ -12,8 +12,8 @@ import os
 from manticore.core.smtlib import operators
 from eth_general import make_mock_evm_state
 from manticore.ethereum import ManticoreEVM, DetectInvalid, DetectIntegerOverflow, Detector, NoAliveStates, ABI, \
-    EthereumError, DetectReentrancyAdvanced, DetectUnusedRetVal, DetectSelfdestruct, LoopDepthLimiter, DetectExternalCallAndLeak, \
-    DetectEnvInstruction
+    EthereumError, DetectReentrancySimple, DetectReentrancyAdvanced, DetectUnusedRetVal, DetectSelfdestruct, LoopDepthLimiter, DetectDelegatecall, \
+    DetectEnvInstruction, DetectExternalCallAndLeak, DetectEnvInstruction
 
 import shutil
 
@@ -57,7 +57,7 @@ class EthDetectorTest(unittest.TestCase):
         self.assertEqual(expected_findings, actual_findings)
 
 class EthRetVal(EthDetectorTest):
-    """ https://consensys.net/diligence/evm-analyzer-benchmark-suite/ """
+    """ Detect when a return value of a low level transaction instruction is ignored """
     DETECTOR_CLASS = DetectUnusedRetVal
 
     def test_retval_ok(self):
@@ -180,3 +180,36 @@ class DetectEnvInstruction(EthDetectorTest):
 
 
 
+class EthDelegatecall(EthDetectorTest):
+    """ Test the detecion of funny delegatecalls """
+    DETECTOR_CLASS = DetectDelegatecall
+
+    def test_delegatecall_ok(self):
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, set())
+
+    def test_delegatecall_ok1(self):
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, set())
+
+    def test_delegatecall_ok2(self):
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, set())
+
+    @unittest.skip("Too slow for this modern times")
+    def test_delegatecall_ok3(self):
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, set())
+
+    def test_delegatecall_not_ok(self):
+        self.mevm.register_plugin(LoopDepthLimiter())
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, {(179, 'Delegatecall to user controlled function', False), (179, 'Delegatecall to user controlled address', False)})
+
+    @unittest.skip("Too slow for this modern times")
+    def test_delegatecall_not_ok1(self):
+        self.mevm.register_plugin(LoopDepthLimiter(loop_count_threshold=500))
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, {(179, 'Delegatecall to user controlled function', False)})
+
+