disable proof hint generation during call to get_exit_code (#1153)

Previously, the get_exit_code call would emit events into the proof
trace. This is not actually part of the proof of execution though, so we
should omit these events.

---------

Co-authored-by: rv-jenkins <[email protected]>

Author: dwightguth

runtime/util/finish_rewriting.cpp

@@ -68,9 +68,12 @@ void init_outputs(char const *output_filename) {
     write_configuration_to_proof_trace(proof_writer, subject, false);
   }
 
+  bool was_proof_output = proof_output;
+  proof_output = false;
+
   auto exit_code = error ? 113 : get_exit_code(subject);
 
-  if (proof_output) {
+  if (was_proof_output) {
     w->end_of_trace();
   }
 

test/output/exit-cell/exec0.output-cell.proof.out.diff

@@ -26,7 +26,3 @@ rule: 144 3
   Var'Unds'Gen0 = kore[\dv{SortInt{}}("1")]
   VarI = kore[\dv{SortInt{}}("0")]
 config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(dotk{}()),Lbl'-LT-'status-code'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))]
-rule: 189 3
-  Var'Unds'Gen0 = kore[Lbl'-LT-'k'-GT-'{}(dotk{}())]
-  Var'Unds'Gen1 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
-  VarExit = kore[\dv{SortInt{}}("0")]