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

[tautschnig]

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.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #6650 (4c2c27d) into develop (b630cc5) will increase coverage by 0.00%.
The diff coverage is 80.00%.

@@           Coverage Diff            @@
##           develop    #6650   +/-   ##
========================================
  Coverage    76.73%   76.73%           
========================================
  Files         1579     1579           
  Lines       181994   182008   +14     
========================================
+ Hits        139650   139671   +21     
+ Misses       42344    42337    -7     

Impacted Files	Coverage Δ
...rc/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp	76.98% <33.33%> (ø)
src/goto-checker/single_path_symex_checker.cpp	85.89% <100.00%> (+5.37%)	⬆️
src/goto-programs/remove_vector.cpp	96.68% <100.00%> (+0.11%)	⬆️
src/ansi-c/c_expr.h	100.00% <0.00%> (ø)
src/goto-checker/multi_path_symex_checker.cpp	95.65% <0.00%> (+4.34%)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 770d791...4c2c27d. Read the comment docs.