This function returns up to `n` possible solutions for expression `expr`.

        :param expr: expression (an AST) to evaluate
        :param n: number of results to return
        :param solver: a solver object, native to the backend, to assist in
                       the evaluation (for example, a z3.Solver)
        :param extra_constraints: extra constraints (as ASTs) to add to the solver for this solve
        :param model_callback:      a function that will be executed with recovered models (if any)
        :return:              A sequence of up to n results (backend objects)

def eval(self, expr, n, extra_constraints=(), solver=None, model_callback=None):
        """
        This function returns up to `n` possible solutions for expression `expr`.

        :param expr: expression (an AST) to evaluate
        :param n: number of results to return
        :param solver: a solver object, native to the backend, to assist in
                       the evaluation (for example, a z3.Solver)
        :param extra_constraints: extra constraints (as ASTs) to add to the solver for this solve
        :param model_callback:      a function that will be executed with recovered models (if any)
        :return:              A sequence of up to n results (backend objects)
        """
        if self._solver_required and solver is None:
            raise BackendError("%s requires a solver for evaluation" % self.__class__.__name__)

        results = self._eval(
            self.convert(expr), n, extra_constraints=self.convert_list(extra_constraints),
            solver=solver, model_callback=model_callback
        )

        results = list(results)
        if type(expr) is not BV:
            return results

        size = expr.length
        for i in range(len(results)):
            results[i] &= (1 << size) - 1 # convert it back to unsigned

        # solver is done, terminate process
        solver.terminate()

        return results