Make example trace output optional via --save-runs

[thpani]

We introduced example trace output in #1838. As described in #2039 and #2019, this creates a unexpected performance bottleneck if the SMT call for constructing the trace takes a long time.

Oddly enough, writing the trace was made optional for simulate via the --save-runs flag (defaulting to false) in #1838, but always enabled for check.

With this PR, we lift --save-runs to check, making example trace output optional also for check.

We also make some UX improvements that

• fix the case where the last symbolic run of simulate was output twice,
• add log output around the example trace output, and
• adjust example output log levels from ERROR to INFO.

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality
• Entries added to ./unreleased/ for any new functionality

Fixes #2039

[codecov-commenter]

Codecov Report

Merging #2047 (f5d0dba) into main (e15a836) will decrease coverage by 0.00%.
The diff coverage is 50.00%.

@@            Coverage Diff             @@
##             main    #2047      +/-   ##
==========================================
- Coverage   77.73%   77.72%   -0.01%     
==========================================
  Files         420      420              
  Lines       12847    12846       -1     
  Branches      577      588      +11     
==========================================
- Hits         9986     9985       -1     
  Misses       2861     2861              

Impacted Files	Coverage Δ
...at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala	0.00% <0.00%> (ø)
...forsyte/apalache/tla/tooling/opt/SimulateCmd.scala	0.00% <ø> (ø)
...ache/tla/bmcmt/DumpFilesModelCheckerListener.scala	0.00% <ø> (ø)
...t/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala	85.14% <100.00%> (-1.15%)	⬇️
...apalache/tla/bmcmt/search/ModelCheckerParams.scala	94.44% <100.00%> (ø)
...he/io/annotations/parser/CommentPreprocessor.scala	96.70% <0.00%> (+1.09%)	⬆️

📣 Codecov can now indicate which changes are the most critical in Pull Requests. Learn more

[thpani]

Had to do some wiring in f3a5b2b.
I find it weird that this is wired in via tuning options, but we can fix that in a follow-up PR: #2054