Added generation of proof in the smt backend when the model is unsatisfiable. There are still self-loops in the generated code, which need to be removed