In this technical report the symbolic execution engine ’Mulib’ will be outlined in its architecture, main algorithms, and design decisions. Mulib employs a rather new approach of program transformation (see Section 2) and thus, technical details on the implementation of such a system are thought to be insightful. Mulib first and foremost implements the runtime semantics of the Constraint-Logic Object-Oriented  programming (CLOOP) language Muli [18]. Muli employs symbolic execution [11] as a technique to, e.g., solve constraint-satisfaction problems and generate test cases [19, 55].