The Symbiotic tool is able to prune programs in LLVM, i.e. remove their instructions that do not affect the (non-)fulfillment of the given specification. This pruning can greatly simplify the subsequent verification of programs. Some verification tools expect C programs as input and therefore need to translate the pruned program back to C before processing it. One translator from LLVM to C is called llvm2c. Currently, this tool produces C programs that make heavy use of the goto statement. The goal of this thesis is to improve llvm2c so that it produces programs with control structures like for or while instead of goto. The thesis will provide a survey of existing tools for translating LLVM to C (in particular rellic and llvm-cbe). The thesis will also include experimental evaluation, in particular a comparison of the number of goto statements in programs produced by the original and modified llvm2c as well as by rellic and llvm-cbe tools on benchmarks from SV-COMP. Since some verification tools can take the advantage of for or while loops (e.g., to compute invariants or predicates for abstraction), this paper will also investigate the effect of implemented enhancements in llvm2c on the performance of an appropriately chosen verification tool.