diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py
index f63a5c1de..d970a1f71 100644
--- a/manticore/core/smtlib/expression.py
+++ b/manticore/core/smtlib/expression.py
@@ -40,13 +40,13 @@ def taint(self):
 
 def issymbolic(value) -> bool:
     """
-        Helper to determine whether an object is symbolic (e.g checking
-        if data read from memory is symbolic)
+    Helper to determine whether an object is symbolic (e.g checking
+    if data read from memory is symbolic)
 
-        :param object value: object to check
-        :return: whether `value` is symbolic
-        :rtype: bool
-        """
+    :param object value: object to check
+    :return: whether `value` is symbolic
+    :rtype: bool
+    """
     return isinstance(value, Expression)
 
 
@@ -293,6 +293,9 @@ def __mul__(self, other):
     def __mod__(self, other):
         return BitVecMod(self, self.cast(other))
 
+    def __pow__(self, other):
+        return BitVecPow(self, self.cast(other))
+
     # object.__divmod__(self, other)
     # object.__pow__(self, other[, modulo])
 
@@ -543,6 +546,11 @@ def __init__(self, a, b, *args, **kwargs):
         super().__init__(a.size, a, b, *args, **kwargs)
 
 
+class BitVecPow(BitVecOperation):
+    def __init__(self, a, b, *args, **kwargs):
+        super().__init__(a.size, a, b, *args, **kwargs)
+
+
 class BitVecDiv(BitVecOperation):
     def __init__(self, a, b, *args, **kwargs):
         super().__init__(a.size, a, b, *args, **kwargs)
@@ -676,7 +684,7 @@ class Array(Expression):
     def __init__(
         self, index_bits: int, index_max: Optional[int], value_bits: int, *operands, **kwargs
     ):
-        assert index_bits in (32, 64, 256)
+        assert index_bits in (8, 32, 64, 256)
         assert value_bits in (8, 16, 32, 64, 256)
         assert index_max is None or index_max >= 0 and index_max < 2 ** index_bits
         self._index_bits = index_bits
diff --git a/manticore/core/smtlib/visitors.py b/manticore/core/smtlib/visitors.py
index 2cf7efdb5..e2f844a38 100644
--- a/manticore/core/smtlib/visitors.py
+++ b/manticore/core/smtlib/visitors.py
@@ -930,6 +930,9 @@ def bindings(self):
         ArraySelect: "select",
     }
 
+    def visit_BitVecPow(self, expression, base, exponent):
+        return f"((_ int2bv {expression.size})  ( ^ (bv2int {base}) (bv2int {exponent}) ))"
+
     def visit_BitVecConstant(self, expression):
         assert isinstance(expression, BitVecConstant)
         if expression.size == 1:
diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index b55f10c5b..0305094f1 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -111,43 +111,43 @@ def calculate_coverage(runtime_bytecode, seen):
 
 
 class ManticoreEVM(ManticoreBase):
-    """ Manticore EVM manager
-
-        Usage Ex::
-
-            from manticore.ethereum import ManticoreEVM, ABI
-            m = ManticoreEVM()
-            #And now make the contract account to analyze
-            source_code = '''
-                pragma solidity ^0.4.15;
-                contract AnInt {
-                    uint private i=0;
-                    function set(uint value){
-                        i=value
-                    }
+    """Manticore EVM manager
+
+    Usage Ex::
+
+        from manticore.ethereum import ManticoreEVM, ABI
+        m = ManticoreEVM()
+        #And now make the contract account to analyze
+        source_code = '''
+            pragma solidity ^0.4.15;
+            contract AnInt {
+                uint private i=0;
+                function set(uint value){
+                    i=value
                 }
-            '''
-            #Initialize user and contracts
-            user_account = m.create_account(balance=1000)
-            contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0)
-            contract_account.set(12345, value=100)
-
-            m.finalize()
+            }
+        '''
+        #Initialize user and contracts
+        user_account = m.create_account(balance=1000)
+        contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0)
+        contract_account.set(12345, value=100)
+
+        m.finalize()
     """
 
     def make_symbolic_buffer(self, size, name=None, avoid_collisions=False):
-        """ Creates a symbolic buffer of size bytes to be used in transactions.
-            You can operate on it normally and add constraints to manticore.constraints
-            via manticore.constrain(constraint_expression)
-
-            Example use::
-
-                symbolic_data = m.make_symbolic_buffer(320)
-                m.constrain(symbolic_data[0] == 0x65)
-                m.transaction(caller=attacker_account,
-                                address=contract_account,
-                                data=symbolic_data,
-                                value=100000 )
+        """Creates a symbolic buffer of size bytes to be used in transactions.
+        You can operate on it normally and add constraints to manticore.constraints
+        via manticore.constrain(constraint_expression)
+
+        Example use::
+
+            symbolic_data = m.make_symbolic_buffer(320)
+            m.constrain(symbolic_data[0] == 0x65)
+            m.transaction(caller=attacker_account,
+                            address=contract_account,
+                            data=symbolic_data,
+                            value=100000 )
         """
         if name is None:
             name = "TXBUFFER"
@@ -163,19 +163,19 @@ def make_symbolic_buffer(self, size, name=None, avoid_collisions=False):
         )
 
     def make_symbolic_value(self, nbits=256, name=None):
-        """ Creates a symbolic value, normally a uint256, to be used in transactions.
-            You can operate on it normally and add constraints to manticore.constraints
-            via manticore.constrain(constraint_expression)
+        """Creates a symbolic value, normally a uint256, to be used in transactions.
+        You can operate on it normally and add constraints to manticore.constraints
+        via manticore.constrain(constraint_expression)
 
-            Example use::
+        Example use::
 
-                symbolic_value = m.make_symbolic_value()
-                m.constrain(symbolic_value > 100)
-                m.constrain(symbolic_value < 1000)
-                m.transaction(caller=attacker_account,
-                                address=contract_account,
-                                data=data,
-                                value=symbolic_value )
+            symbolic_value = m.make_symbolic_value()
+            m.constrain(symbolic_value > 100)
+            m.constrain(symbolic_value < 1000)
+            m.transaction(caller=attacker_account,
+                            address=contract_account,
+                            data=data,
+                            value=symbolic_value )
 
         """
         avoid_collisions = False
@@ -319,16 +319,16 @@ def _compile_through_crytic_compile(filename, contract_name, libraries, crytic_c
 
     @staticmethod
     def _compile(source_code, contract_name, libraries=None, crytic_compile_args=None):
-        """ Compile a Solidity contract, used internally
-
-            :param source_code: solidity source
-            :type source_code: string (filename, directory, etherscan address) or a file handle
-            :param contract_name: a string with the name of the contract to analyze
-            :param libraries: an itemizable of pairs (library_name, address)
-            :param crytic_compile_args: crytic compile options (https://github.com/crytic/crytic-compile/wiki/Configuration)
-            :type crytic_compile_args: dict
-            :return: name, source_code, bytecode, srcmap, srcmap_runtime, hashes
-            :return: name, source_code, bytecode, runtime, srcmap, srcmap_runtime, hashes, abi, warnings
+        """Compile a Solidity contract, used internally
+
+        :param source_code: solidity source
+        :type source_code: string (filename, directory, etherscan address) or a file handle
+        :param contract_name: a string with the name of the contract to analyze
+        :param libraries: an itemizable of pairs (library_name, address)
+        :param crytic_compile_args: crytic compile options (https://github.com/crytic/crytic-compile/wiki/Configuration)
+        :type crytic_compile_args: dict
+        :return: name, source_code, bytecode, srcmap, srcmap_runtime, hashes
+        :return: name, source_code, bytecode, runtime, srcmap, srcmap_runtime, hashes, abi, warnings
         """
 
         crytic_compile_args = dict() if crytic_compile_args is None else crytic_compile_args
@@ -336,10 +336,13 @@ def _compile(source_code, contract_name, libraries=None, crytic_compile_args=Non
         if isinstance(source_code, io.IOBase):
             source_code = source_code.name
 
-        if (isinstance(source_code, str) and
-                not is_supported(source_code) and
-                # Until https://github.com/crytic/crytic-compile/issues/103 is implemented
-                "ignore_compile" not in crytic_compile_args):
+        if (
+            isinstance(source_code, str)
+            and not is_supported(source_code)
+            and
+            # Until https://github.com/crytic/crytic-compile/issues/103 is implemented
+            "ignore_compile" not in crytic_compile_args
+        ):
             with tempfile.NamedTemporaryFile("w+", suffix=".sol") as temp:
                 temp.write(source_code)
                 temp.flush()
@@ -489,7 +492,7 @@ def human_transactions(self, state_id=None):
 
     def make_symbolic_arguments(self, types):
         """
-            Build a reasonable set of symbolic arguments matching the types list
+        Build a reasonable set of symbolic arguments matching the types list
         """
         from . import abitypes
 
@@ -542,24 +545,24 @@ def solidity_create_contract(
         gas=None,
         compile_args=None,
     ):
-        """ Creates a solidity contract and library dependencies
-
-            :param source_code: solidity source code
-            :type source_code: string (filename, directory, etherscan address) or a file handle
-            :param owner: owner account (will be default caller in any transactions)
-            :type owner: int or EVMAccount
-            :param contract_name: Name of the contract to analyze (optional if there is a single one in the source code)
-            :type contract_name: str
-            :param balance: balance to be transferred on creation
-            :type balance: int or BitVecVariable
-            :param address: the address for the new contract (optional)
-            :type address: int or EVMAccount
-            :param tuple args: constructor arguments
-            :param compile_args: crytic compile options #FIXME(https://github.com/crytic/crytic-compile/wiki/Configuration)
-            :type compile_args: dict
-            :param gas: gas budget for each contract creation needed (may be more than one if several related contracts defined in the solidity source)
-            :type gas: int
-            :rtype: EVMAccount
+        """Creates a solidity contract and library dependencies
+
+        :param source_code: solidity source code
+        :type source_code: string (filename, directory, etherscan address) or a file handle
+        :param owner: owner account (will be default caller in any transactions)
+        :type owner: int or EVMAccount
+        :param contract_name: Name of the contract to analyze (optional if there is a single one in the source code)
+        :type contract_name: str
+        :param balance: balance to be transferred on creation
+        :type balance: int or BitVecVariable
+        :param address: the address for the new contract (optional)
+        :type address: int or EVMAccount
+        :param tuple args: constructor arguments
+        :param compile_args: crytic compile options #FIXME(https://github.com/crytic/crytic-compile/wiki/Configuration)
+        :type compile_args: dict
+        :param gas: gas budget for each contract creation needed (may be more than one if several related contracts defined in the solidity source)
+        :type gas: int
+        :rtype: EVMAccount
         """
         if compile_args is None:
             compile_args = dict()
@@ -665,17 +668,17 @@ def get_nonce(self, address):
             return next(iter(nonces))
 
     def create_contract(self, owner, balance=0, address=None, init=None, name=None, gas=None):
-        """ Creates a contract
-
-            :param owner: owner account (will be default caller in any transactions)
-            :type owner: int or EVMAccount
-            :param balance: balance to be transferred on creation
-            :type balance: int or BitVecVariable
-            :param int address: the address for the new contract (optional)
-            :param str init: initializing evm bytecode and arguments
-            :param str name: a unique name for reference
-            :param gas: gas budget for the creation/initialization of the contract
-            :rtype: EVMAccount
+        """Creates a contract
+
+        :param owner: owner account (will be default caller in any transactions)
+        :type owner: int or EVMAccount
+        :param balance: balance to be transferred on creation
+        :type balance: int or BitVecVariable
+        :param int address: the address for the new contract (optional)
+        :param str init: initializing evm bytecode and arguments
+        :param str name: a unique name for reference
+        :param gas: gas budget for the creation/initialization of the contract
+        :rtype: EVMAccount
         """
         if not self.count_ready_states():
             raise NoAliveStates
@@ -751,34 +754,34 @@ def end_block(self):
             world.end_block()
 
     def transaction(self, caller, address, value, data, gas=None, price=1):
-        """ Issue a symbolic transaction in all running states
-
-            :param caller: the address of the account sending the transaction
-            :type caller: int or EVMAccount
-            :param address: the address of the contract to call
-            :type address: int or EVMAccount
-            :param value: balance to be transfered on creation
-            :type value: int or BitVecVariable
-            :param data: initial data
-            :param gas: gas budget
-            :param price: gas unit price
-            :raises NoAliveStates: if there are no alive states to execute
+        """Issue a symbolic transaction in all running states
+
+        :param caller: the address of the account sending the transaction
+        :type caller: int or EVMAccount
+        :param address: the address of the contract to call
+        :type address: int or EVMAccount
+        :param value: balance to be transfered on creation
+        :type value: int or BitVecVariable
+        :param data: initial data
+        :param gas: gas budget
+        :param price: gas unit price
+        :raises NoAliveStates: if there are no alive states to execute
         """
         self._transaction(
             "CALL", caller, value=value, address=address, data=data, gas=gas, price=price
         )
 
     def create_account(self, balance=0, address=None, code=None, name=None, nonce=None):
-        """ Low level creates an account. This won't generate a transaction.
-
-            :param balance: balance to be set on creation (optional)
-            :type balance: int or BitVecVariable
-            :param address: the address for the new account (optional)
-            :type address: int
-            :param code: the runtime code for the new account (None means normal account), str or bytes (optional)
-            :param nonce: force a specific nonce
-            :param name: a global account name eg. for use as reference in the reports (optional)
-            :return: an EVMAccount
+        """Low level creates an account. This won't generate a transaction.
+
+        :param balance: balance to be set on creation (optional)
+        :type balance: int or BitVecVariable
+        :param address: the address for the new account (optional)
+        :type address: int
+        :param code: the runtime code for the new account (None means normal account), str or bytes (optional)
+        :param nonce: force a specific nonce
+        :param name: a global account name eg. for use as reference in the reports (optional)
+        :return: an EVMAccount
         """
         # Need at least one state where to apply this
         if not self.count_ready_states():
@@ -874,17 +877,17 @@ def _migrate_tx_expressions(self, state, caller, address, value, data, gas, pric
         return caller, address, value, data, gas, price
 
     def _transaction(self, sort, caller, value=0, address=None, data=None, gas=None, price=1):
-        """ Initiates a transaction
-
-            :param caller: caller account
-            :type caller: int or EVMAccount
-            :param int address: the address for the transaction (optional)
-            :param value: value to be transferred
-            :param price: the price of gas for this transaction.
-            :type value: int or BitVecVariable
-            :param str data: initializing evm bytecode and arguments or transaction call data
-            :param gas: gas budget for current transaction
-            :rtype: EVMAccount
+        """Initiates a transaction
+
+        :param caller: caller account
+        :type caller: int or EVMAccount
+        :param int address: the address for the transaction (optional)
+        :param value: value to be transferred
+        :param price: the price of gas for this transaction.
+        :type value: int or BitVecVariable
+        :param str data: initializing evm bytecode and arguments or transaction call data
+        :param gas: gas budget for current transaction
+        :rtype: EVMAccount
         """
         if gas is None:
             gas = consts.defaultgas
@@ -991,13 +994,13 @@ def preconstraint_for_call_transaction(
         value: Optional[Union[int, Expression]] = None,
         contract_metadata: Optional[SolidityMetadata] = None,
     ):
-        """ Returns a constraint that excludes combinations of value and data that would cause an exception in the EVM
-            contract dispatcher.
+        """Returns a constraint that excludes combinations of value and data that would cause an exception in the EVM
+        contract dispatcher.
 
-            :param address: address of the contract to call
-            :param value: balance to be transferred (optional)
-            :param data: symbolic transaction data
-            :param contract_metadata: SolidityMetadata for the contract (optional)
+        :param address: address of the contract to call
+        :param value: balance to be transferred (optional)
+        :param data: symbolic transaction data
+        :param contract_metadata: SolidityMetadata for the contract (optional)
         """
         if isinstance(address, EVMAccount):
             address = int(address)
@@ -1265,8 +1268,8 @@ def _on_unsound_symbolication(self, state, func, data, result):
         result.append(value)
 
     def fix_unsound_symbolication_fake(self, state):
-        """ This method goes through all the applied symbolic functions and tries
-            to find a concrete matching set of pairs
+        """This method goes through all the applied symbolic functions and tries
+        to find a concrete matching set of pairs
         """
 
         def make_cond(state, table):
@@ -1284,8 +1287,8 @@ def make_cond(state, table):
         return state.can_be_true(True)
 
     def fix_unsound_symbolication_sound(self, state):
-        """ This method goes through all the applied symbolic functions and tries
-            to find a concrete matching set of pairs
+        """This method goes through all the applied symbolic functions and tries
+        to find a concrete matching set of pairs
         """
 
         def concretize_known_pairs(state, symbolic_pairs, known_pairs):
@@ -1302,7 +1305,7 @@ def concretize_known_pairs(state, symbolic_pairs, known_pairs):
                     return
 
         def match(state, func, symbolic_pairs, concrete_pairs, start=None):
-            """ Tries to find a concrete match for the symbolic pairs. It uses
+            """Tries to find a concrete match for the symbolic pairs. It uses
             concrete_pairs (and potentially extends it with solved pairs) until
             a matching set of concrete pairs is found, or fail.
 
@@ -1419,9 +1422,9 @@ def fix_unsound_symbolication(self, state):
         return state.context["soundcheck"]
 
     def _terminate_state_callback(self, state, e):
-        """ INTERNAL USE
-            Every time a state finishes executing the last transaction, we save it in
-            our private list
+        """INTERNAL USE
+        Every time a state finishes executing the last transaction, we save it in
+        our private list
         """
         if isinstance(e, AbandonState):
             # do nothing
@@ -1478,8 +1481,8 @@ def _did_evm_execute_instruction_callback(self, state, instruction, arguments, r
         )
 
     def get_metadata(self, address) -> Optional[SolidityMetadata]:
-        """ Gets the solidity metadata for address.
-            This is available only if address is a contract created from solidity
+        """Gets the solidity metadata for address.
+        This is available only if address is a contract created from solidity
         """
         return self.metadata.get(address)
 
@@ -1844,9 +1847,9 @@ def worker_finalize(q):
         self.remove_all()
 
     def global_coverage(self, account):
-        """ Returns code coverage for the contract on `account_address`.
-            This sums up all the visited code lines from any of the explored
-            states.
+        """Returns code coverage for the contract on `account_address`.
+        This sums up all the visited code lines from any of the explored
+        states.
         """
         account_address = int(account)
         runtime_bytecode = None
diff --git a/manticore/ethereum/verifier.py b/manticore/ethereum/verifier.py
index 57c96d5d0..8c8c0543a 100644
--- a/manticore/ethereum/verifier.py
+++ b/manticore/ethereum/verifier.py
@@ -58,7 +58,7 @@ def manticore_verifier(
     outputspace_url=None,
     timeout=100,
 ):
-    """ Verify solidity properties
+    """Verify solidity properties
     The results are dumped to stdout and to the workspace folder.
 
         $manticore-verifier property.sol  --contract TestToken --smt.solver yices --maxt 4
@@ -101,10 +101,64 @@ def manticore_verifier(
     :param timeout: timeout in seconds
     :return:
     """
+
+    def check_properties():
+        m.take_snapshot()  # make a copy of all ready states
+
+        # And now explore all properties (and only the properties)
+        filter_no_crytic.disable()  # Allow crytic_porperties
+        filter_out_human_constants.disable()  # Allow them to be marked as constants
+        filter_only_crytic.enable()  # Exclude all methods that are not property checks
+        symbolic_data = m.make_symbolic_buffer(4 + 32 * 2)
+        m.transaction(caller=checker_account, address=contract_account, value=0, data=symbolic_data)
+
+        for state in m.all_states:
+            world = state.platform
+            tx = world.human_transactions[-1]
+            md = m.get_metadata(tx.address)
+            """
+            A is _broken_ if:
+                 * is normal property
+                 * RETURN False
+               OR:
+                 * property name ends witth 'revert'
+                 * does not REVERT
+            Property is considered to _pass_ otherwise
+            """
+            N = constrain_to_known_func_ids(state)
+            for func_id in map(bytes, state.solve_n(tx.data[:4], nsolves=N)):
+                func_name = md.get_abi(func_id)["name"]
+                if not func_name.endswith("revert"):
+                    # Property does not ends in "revert"
+                    # It must RETURN a 1
+                    if tx.return_value == 1:
+                        # TODO: test when property STOPs
+                        return_data = ABI.deserialize("bool", tx.return_data)
+                        testcase = m.generate_testcase(
+                            state,
+                            f"property {md.get_func_name(func_id)} is broken",
+                            only_if=AND(tx.data[:4] == func_id, return_data == 0),
+                        )
+                        if testcase:
+                            properties[func_name].append(testcase.num)
+                else:
+                    # property name ends in "revert" so it MUST revert
+                    if tx.result != "REVERT":
+                        testcase = m.generate_testcase(
+                            state,
+                            f"Some property is broken did not reverted.(MUST REVERTED)",
+                            only_if=tx.data[:4] == func_id,
+                        )
+                        if testcase:
+                            properties[func_name].append(testcase.num)
+
+        m.clear_terminated_states()  # no interest in reverted states for now!
+        m.goto_snapshot()  # GO back to whatever we ahd before checking the properties
+
     # Termination condition
     # Exploration will stop when some of the following happens:
     # * MAXTX human transaction sent
-    # * Code coverage is greater than MAXCOV meassured on target contract
+    # * Global code coverage is greater than MAXCOV meassured on target contract
     # * No more coverage was gained in the last transaction
     # * At least MAXFAIL different properties where found to be breakable. (1 for fail fast)
 
@@ -189,8 +243,8 @@ def manticore_verifier(
     print(
         f"""# Exploration will stop when some of the following happens:
 # * {MAXTX} human transaction sent
-# * Code coverage is greater than {MAXCOV}% meassured on target contract
-# * No more coverage was gained in the last transaction
+# * Global code coverage is greater than {MAXCOV}% meassured on target contract
+# * No more global coverage was gained in the last transaction
 # * At least {MAXFAIL} different properties where found to be breakable. (1 for fail fast)
 # * {timeout} seconds pass"""
     )
@@ -199,6 +253,8 @@ def manticore_verifier(
         f"Transactions done: {tx_num}. States: {m.count_ready_states()}, RT Coverage: {0.00}%, "
         f"Failing properties: 0/{len(properties)}"
     )
+
+    check_properties()  # check the porperties at the initial state
     with m.kill_timeout(timeout=timeout):
         while not m.is_killed():
             # check if we found a way to break more than MAXFAIL properties
@@ -234,97 +290,7 @@ def manticore_verifier(
                 print("Cancelled or timeout.")
                 break
 
-            # Explore all methods but the "crytic_" properties
-            # Note: you may be tempted to get all valid function ids/hashes from the
-            #  metadata and to constrain the first 4 bytes of the calldata here.
-            #  This wont work because we also want to prevent the contract to call
-            #  crytic added methods as internal transactions
-            filter_no_crytic.enable()  # filter out crytic_porperties
-            filter_out_human_constants.enable()  # Exclude constant methods
-            filter_only_crytic.disable()  # Exclude all methods that are not property checks
-
-            symbolic_data = m.make_symbolic_buffer(320)
-            symbolic_value = m.make_symbolic_value()
-            caller_account = m.make_symbolic_value(160)
-            args = tuple((caller_account == address_i for address_i in user_accounts))
-
-            m.constrain(OR(*args, False))
-            m.transaction(
-                caller=caller_account,
-                address=contract_account,
-                value=symbolic_value,
-                data=symbolic_data,
-            )
-
-            # check if timeout was requested during the previous transaction
-            if m.is_killed():
-                print("Cancelled or timeout.")
-                break
-
-            m.clear_terminated_states()  # no interest in reverted states
-            m.take_snapshot()  # make a copy of all ready states
-            print(
-                f"Transactions done: {tx_num}. States: {m.count_ready_states()}, "
-                f"RT Coverage: {m.global_coverage(contract_account):3.2f}%, "
-                f"Failing properties: {broken_properties}/{len(properties)}"
-            )
-
-            # check if timeout was requested while we were taking the snapshot
-            if m.is_killed():
-                print("Cancelled or timeout.")
-                break
-
-            # And now explore all properties (and only the properties)
-            filter_no_crytic.disable()  # Allow crytic_porperties
-            filter_out_human_constants.disable()  # Allow them to be marked as constants
-            filter_only_crytic.enable()  # Exclude all methods that are not property checks
-            symbolic_data = m.make_symbolic_buffer(4)
-            m.transaction(
-                caller=checker_account, address=contract_account, value=0, data=symbolic_data
-            )
-
-            for state in m.all_states:
-                world = state.platform
-                tx = world.human_transactions[-1]
-                md = m.get_metadata(tx.address)
-                """
-                A is _broken_ if:
-                     * is normal property
-                     * RETURN False
-                   OR:
-                     * property name ends with 'revert'
-                     * does not REVERT
-                Property is considered to _pass_ otherwise
-                """
-                N = constrain_to_known_func_ids(state)
-                for func_id in map(bytes, state.solve_n(tx.data[:4], nsolves=N)):
-                    func_name = md.get_abi(func_id)["name"]
-                    if not func_name.endswith("revert"):
-                        # Property does not ends in "revert"
-                        # It must RETURN a 1
-                        if tx.return_value == 1:
-                            # TODO: test when property STOPs
-                            return_data = ABI.deserialize("bool", tx.return_data)
-                            testcase = m.generate_testcase(
-                                state,
-                                f"property {md.get_func_name(func_id)} is broken",
-                                only_if=AND(tx.data[:4] == func_id, return_data == 0),
-                            )
-                            if testcase:
-                                properties[func_name].append(testcase.num)
-                    else:
-                        # property name ends in "revert" so it MUST revert
-                        if tx.result != "REVERT":
-                            testcase = m.generate_testcase(
-                                state,
-                                f"Some property is broken did not reverted.(MUST REVERTED)",
-                                only_if=tx.data[:4] == func_id,
-                            )
-                            if testcase:
-                                properties[func_name].append(testcase.num)
-
-            m.clear_terminated_states()  # no interest in reverted states for now!
-            m.goto_snapshot()
+            check_properties()
         else:
             print("Cancelled or timeout.")
 
@@ -366,7 +332,11 @@ def main():
     cryticparser.init(parser)
 
     parser.add_argument(
-        "source_code", type=str, nargs="*", default=[], help="Contract source code",
+        "source_code",
+        type=str,
+        nargs="*",
+        default=[],
+        help="Contract source code",
     )
     parser.add_argument(
         "-v", action="count", default=0, help="Specify verbosity level from -v to -vvvv"
@@ -387,7 +357,9 @@ def main():
         help="Show program version information",
     )
     parser.add_argument(
-        "--propconfig", type=str, help="Solidity property accounts config file (.yml)",
+        "--propconfig",
+        type=str,
+        help="Solidity property accounts config file (.yml)",
     )
     eth_flags = parser.add_argument_group("Ethereum flags")
 
@@ -500,5 +472,5 @@ def main():
         psender=psender,
         timeout=args.timeout,
         propre=args.propre,
-        compile_args=vars(parsed)
+        compile_args=vars(parsed),
     )
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index cac72fbc4..dc07e1e02 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -57,6 +57,25 @@
 DEFAULT_FORK = "istanbul"
 
 
+def globalexp(data):
+    if issymbolic(data):
+        return None
+    base = 0
+    for c in data[:32]:
+        base += base << 8 + c
+    exp = 0
+    for c in data[32:]:
+        exp += exp << 8 + c
+
+    if exp == 0:
+        return 1
+
+    if base == 0:
+        return 0
+
+    return base ** exp
+
+
 def globalsha3(data):
     if issymbolic(data):
         return None
@@ -67,6 +86,12 @@ def globalfakesha3(data):
     return None
 
 
+consts.add(
+    "symbolicexp",
+    default=False,
+    description="If enabled treat EXP as a source of symbolic imprecision",
+)
+
 consts.add(
     "oog",
     default="complete",
@@ -103,7 +128,9 @@ def globalfakesha3(data):
     description="Max calldata size to explore in each CALLDATACOPY. Iff size in a calldata related instruction are symbolic it will be constrained to be less than this constant. -1 means free(only use when gas is being tracked)",
 )
 consts.add(
-    "ignore_balance", default=False, description="Do not try to solve symbolic balances",
+    "ignore_balance",
+    default=False,
+    description="Do not try to solve symbolic balances",
 )
 
 
@@ -1299,6 +1326,7 @@ def setstate(state, value):
 
             raise Concretize("Symbolic PC", expression=expression, setstate=setstate, policy="ALL")
         try:
+            print(self)
             self._check_jmpdest()
             last_pc, last_gas, instruction, arguments, fee, allocated = self._checkpoint()
             result = self._handler(*arguments)
@@ -1527,7 +1555,6 @@ def nbytes(e):
 
         return EXP_SUPPLEMENTAL_GAS * nbytes(exponent)
 
-    @concretized_args(base="SAMPLED", exponent="SAMPLED")
     def EXP(self, base, exponent):
         """
         Exponential operation
@@ -1537,13 +1564,26 @@ def EXP(self, base, exponent):
         :param exponent: exponent value, concretized with sampled values
         :return: BitVec* EXP result
         """
-        if exponent == 0:
-            return 1
-
-        if base == 0:
-            return 0
+        if const.symbolicexp:
+            if issymbolic(base) or issymbolic(exponent):
+                data = self.constraints.new_array(index_bits=8, value_bits=8, index_max=64)
+                data = data.write_BE(0, base, 32)
+                data = data.write_BE(32, exponent, 32)
+            else:
+                data = bytearray()
+                for i in reversed(range(256, 8)):
+                    b += data.append((base >> i) & 0xFF)
+                for i in reversed(range(256, 8)):
+                    b += data.append((exponent >> i) & 0xFF)
 
-        return pow(base, exponent, TT256)
+            return self.world.symbolic_function(globalexp, data)
+        else:
+            result = 1
+            for i in range(256):
+                result = Operators.ITEBV(256, exponent & 1 == 1, base * result, result)
+                base = base * base
+                exponent = exponent >> 1
+            return result
 
     def SIGNEXTEND(self, size, value):
         """Extend length of two's complement signed integer"""
@@ -1626,9 +1666,9 @@ def SHA3_gas(self, start, size):
     @concretized_args(size="ALL")
     def SHA3(self, start, size):
         """Compute Keccak-256 hash
-            If the size is symbolic the potential solutions will be sampled as
-            defined by the default policy and the analysis will be forked.
-            The `size` can be considered concrete in this handler.
+        If the size is symbolic the potential solutions will be sampled as
+        defined by the default policy and the analysis will be forked.
+        The `size` can be considered concrete in this handler.
 
         """
         data = self.read_buffer(start, size)
@@ -1694,8 +1734,8 @@ def CALLDATALOAD(self, offset):
         return Operators.CONCAT(256, *bytes)
 
     def _use_calldata(self, offset, size):
-        """ To improve reporting we maintain how much of the calldata is actually
-        used. CALLDATACOPY and CALLDATA LOAD update this limit accordingly """
+        """To improve reporting we maintain how much of the calldata is actually
+        used. CALLDATACOPY and CALLDATA LOAD update this limit accordingly"""
         self._used_calldata_size = Operators.ITEBV(
             256, size != 0, self._used_calldata_size + offset + size, self._used_calldata_size
         )
@@ -2465,6 +2505,7 @@ def symbolic_function(self, func, data):
         Get an unsound symbolication for function `func`
 
         """
+        # TODO(felipe): Generalize data to a tuple of expresisons
         data = self.try_simplify_to_constant(data)
         try:
             result = []
diff --git a/tests/ethereum/test_exp.py b/tests/ethereum/test_exp.py
new file mode 100644
index 000000000..bc0f6b05b
--- /dev/null
+++ b/tests/ethereum/test_exp.py
@@ -0,0 +1,370 @@
+"""
+File name is purposefully not test_* to run this test separately.
+"""
+
+import inspect
+import unittest
+
+import os
+import shutil
+from manticore.platforms.evm import EVMWorld
+from manticore.core.smtlib import operators, ConstraintSet
+from manticore.ethereum import ManticoreEVM
+from manticore.ethereum.plugins import KeepOnlyIfStorageChanges
+from manticore.utils import config
+
+consts = config.get_group("core")
+consts.mprocessing = consts.mprocessing.single
+
+config.get_group("smt").solver = 'yices'
+THIS_DIR = os.path.dirname(os.path.abspath(__file__))
+
+
+class EthSha3TestSymbolicate(unittest.TestCase):
+    def setUp(self):
+        evm_consts = config.get_group("evm")
+        evm_consts.sha3 = evm_consts.sha3.symbolicate
+
+        self.mevm = ManticoreEVM()
+        self.worksp = self.mevm.workspace
+
+    def tearDown(self):
+        self.mevm = None
+        shutil.rmtree(self.worksp)
+
+    def ManticoreEVM(self):
+        return self.mevm
+
+    def test_example1(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint base, uint exponent) payable public{
+                if (base ** exponent == 0x12341234){
+                    emit Log("Found a bug");
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=10000000, name="owner")
+        attacker = m.create_account(balance=10000000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        xbase = m.make_symbolic_value()
+        xexponent = m.make_symbolic_value()
+        contract.foo(x, xbase, xexponent)
+
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 0)  # log is not reachable
+        self.assertEqual(m.count_all_states(), 1)
+
+    def test_example2(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint x, uint base, uint exponent) payable public{
+                if (x == base ** exponent){
+                    emit Log("Found a bug");
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=10000000, name="owner")
+        attacker = m.create_account(balance=10000000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x = m.make_symbolic_value()
+        xbase = m.make_symbolic_value()
+        xexponent = m.make_symbolic_value()
+        contract.foo(x, xbase, xexponent)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)  # log is reachable
+        self.assertEqual(m.count_all_states(), 2)
+
+    def test_example3(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint xbase, uint xexponent, uint ybase, uint yexponent) payable public{
+                if (xbase ** xexponent == ybase ** yexponent){
+                    emit Log("Found a bug");
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=10000000, name="owner")
+        attacker = m.create_account(balance=10000000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        xbase = m.make_symbolic_value()
+        xexponent = m.make_symbolic_value()
+        ybase = m.make_symbolic_value()
+        yexponent = m.make_symbolic_value()
+        contract.foo(xbase, xexponent, ybase, yexponent)
+
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)
+        # x == y #log
+        # x != y
+        self.assertEqual(m.count_all_states(), 2)
+
+    def test_example4(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint xbase, uint xexponent, uint ybase, uint yexponent) payable public{
+                if (xbase ** xexponent == ybase ** yexponent){
+                    if (xbase != 10) {
+                        emit Log("Found a bug"); //Reachable 
+                    }
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=10000000, name="owner")
+        attacker = m.create_account(balance=10000000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        xbase = m.make_symbolic_value()
+        xexponent = m.make_symbolic_value()
+        ybase = m.make_symbolic_value()
+        yexponent = m.make_symbolic_value()
+        contract.foo(xbase, xexponent, ybase, yexponent)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)  # log is reachable
+
+        # x==10 && y == 10
+        # x==C  && y == C && C != 10   #log
+        # x != y
+        self.assertEqual(m.count_all_states(), 3)
+
+    def test_example5(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint xbase, uint xexponent, uint ybase, uint yexponent) payable public{
+                if (xbase ** xexponent == ybase ** yexponent){
+                    if (xbase != 10 && xexponent == 10 && ybase != 10 && yexponent == 10) {
+                        emit Log("Found a bug"); //Reachable 
+                    }
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=10000000, name="owner")
+        attacker = m.create_account(balance=10000000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x = m.make_symbolic_value()
+        xbase = m.make_symbolic_value()
+        xexponent = m.make_symbolic_value()
+        ybase = m.make_symbolic_value()
+        yexponent = m.make_symbolic_value()
+        contract.foo(x, xbase, xexponent, ybase, yexponent)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)  # log is reachable
+        # x==10 && y == 10
+        # x==C  && y == C && C != 10 #log
+        # x != y
+        self.assertEqual(m.count_all_states(), 3)
+
+    def test_example6(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint x, uint base, uint exponent) payable public{
+                if (x == uint256(sha3(base, exponent))){
+                    if(base == 10 && exponent == 10){
+                        emit Log("Found a bug");
+                    }
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=10000000, name="owner")
+        attacker = m.create_account(balance=10000000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x = m.make_symbolic_value()
+        xbase = m.make_symbolic_value()
+        xexponent = m.make_symbolic_value()
+        contract.foo(x, xbase, xexponent)
+ 
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)  # log is reachable
+
+        # x==sha3(10) && y == 10
+        # x==sha3(C) && y == C  && C!=10
+        # x==sha3(C)  && y != C
+        self.assertEqual(m.count_all_states(), 3)
+
+    def test_example7(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint xbase, uint xexponent, uint ybase, uint yexponent) payable public{
+                if (xbase ** xexponent == ybase ** yexponent){
+                    if (xbase == 10 && xexponent == 10) {
+                        emit Log("Found a bug"); //Reachable 
+                    }
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=10000000, name="owner")
+        attacker = m.create_account(balance=10000000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        xbase = m.make_symbolic_value()
+        xexponent = m.make_symbolic_value()
+        ybase = m.make_symbolic_value()
+        yexponent = m.make_symbolic_value()
+        contract.foo(xbase, xexponent, ybase, yexponent)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)  # log is reachable
+
+        # x==y && x == 10
+        # x==y && x != 10
+        # x!=y
+        self.assertEqual(m.count_all_states(), 3)
+
+    def test_example8(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint xbase, uint xexponent, uint ybase, uint yexponent) payable public{
+                if (xbase ** xexponent == ybase ** yexponent){
+                    if (xbase == 10 && xexponent == 10) {
+                        emit Log("Found a bug"); //Reachable 
+                    }
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=10000000, name="owner")
+        attacker = m.create_account(balance=10000000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        xbase = m.make_symbolic_value()
+        xexponent = m.make_symbolic_value()
+        ybase = m.make_symbolic_value()
+        yexponent = m.make_symbolic_value()
+        contract.foo(xbase, xexponent, ybase, yexponent)
+ 
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)  # log is reachable
+
+        # x==y && x == 10
+        # x==y && x != 10
+        # x!=y
+        self.assertEqual(m.count_all_states(), 3)
+
+
+    def test_essence2(self):
+        source_code = """
+        contract I_Choose_Not_To_Run {
+            event Log(string);
+            function foo(uint base, uint exponent) public {
+
+            if( (45**5)**5 == (base ** exponent) **exponent )
+
+                {
+                    emit Log("bug");
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=10000000, name="owner")
+        attacker = m.create_account(balance=10000000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        xbase = m.make_symbolic_value()
+        xexponent = m.make_symbolic_value()
+        contract.foo(xbase, xexponent)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+
+            m.generate_testcase(st)
+            found += len(st.platform.logs)
+        self.assertEqual(found, 1)  # log is reachable
+        self.assertEqual(m.count_all_states(), 2)
+
+
+if __name__ == "__main__":
+    unittest.main()