Code with require tends to produce tons of paths that are reverting and are not necessarily interesting for the users. It would be nice to have a mode where Manticore would discard these paths automatically.

This mode should be added to --quick-mode.

A naive plugin implementation (thanks @feliam) is:

    def will_evm_execute_instruction_callback(self, state, instruction, arguments):
        world = state.platform
        if state.platform.current_transaction.sort != 'CREATE':
            if instruction.semantics == "JUMPI":
                potential_revert = world.current_vm.read_code(world.current_vm.pc + 4)
                if potential_revert[0].size == 8 and potential_revert[0].value == 0xfd:
                    state.constrain(arguments[1] == True)

This assumes that the REVERT is 4 offset after the JUMPI. It was tested with solidity 0.5.12, and it might not work with other compiler versions. It does not work for require(cond, text).

The real implementation should check the latest instruction of each basic blocks to know if the branch is to be discarded.