Single-path symex must not fail an invariant when verification succeeds

Single-path symex takes a best-effort approach to produce a proof by
using the symex equation of that path that was last visited. This,
however, failed an invariant when trying to access the equation that had
already been popped from the worklist. Leave the last equation in place
to avoid this problem.

Author: tautschnig

regression/cbmc/Address_of1/test.desc

@@ -1,8 +1,12 @@
 CORE
 main.c
-
+--stop-on-fail
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+Adding "--stop-on-fail" should not make a difference for successful
+verification, but previously caused an invariant failure when running CBMC with
+"--paths."

src/goto-checker/single_path_symex_checker.cpp

@@ -75,6 +75,10 @@ operator()(propertiest &properties)
         return result;
     }
 
+    // leave the last worklist item in place for the benefit of output_proof
+    if(worklist->size() == 1)
+      break;
+
     worklist->pop();
   }
 
@@ -83,7 +87,7 @@ operator()(propertiest &properties)
 
   final_update_properties(properties, result.updated_properties);
 
-  // Worklist is empty: we are done.
+  // Worklist just has the last element left: we are done.
   return result;
 }
 
@@ -182,6 +186,8 @@ void single_path_symex_checkert::output_error_witness(
 void single_path_symex_checkert::output_proof()
 {
   // This is incorrect, but the best we can do at the moment.
+  // operator()(propertiest &properties) leaves in place the last worklist item
+  // just for this purpose.
   const path_storaget::patht &resume = worklist->peek();
   output_graphml(resume.equation, ns, options);
 }