Verification commands generate too much repetitive output

[brianhuffman]

When running the bike_r2 proofs from s2n, I get lots of output from saw. Some of it looks like this:

[22:31:53.033] Verifying BIKE1_L1_R2_gf2x_mul_1x1 ...
[22:31:53.034] Simulating BIKE1_L1_R2_gf2x_mul_1x1 ...
[22:31:53.074] Checking proof obligations BIKE1_L1_R2_gf2x_mul_1x1 ...
Calling Yices to check sat
Running check sat
Calling Yices to check sat
Running check sat
Calling Yices to check sat
Running check sat
Calling Yices to check sat
Running check sat

This is followed by many more copies of the last two lines, all identical. These should probably be suppressed at the default verbosity setting. And if we print them, these messages would be more useful if they were numbered, like 1/23, 2/23, ... 23/23. (We know how many SAW proof goals there are, after all; printing the current goal number with the total number would make this into a useful progress indicator for long-running proofs.)

Here's another repetitive bit:

[22:31:53.353] Verifying BIKE1_L1_R2_gf2x_mod_mul ...
[22:31:53.391] Simulating BIKE1_L1_R2_gf2x_mod_mul ...
[22:31:53.391] Registering overrides for `BIKE1_L1_R2_gf2x_mul_1x1`
[22:31:53.391]   variant `Symbol "BIKE1_L1_R2_gf2x_mul_1x1"`
[22:31:53.404] Matching 1 overrides of  BIKE1_L1_R2_gf2x_mul_1x1 ...
[22:31:53.405] Branching on 1 override variants of BIKE1_L1_R2_gf2x_mul_1x1 ...
[22:31:53.406] Applied override! BIKE1_L1_R2_gf2x_mul_1x1
[22:31:53.406] Matching 1 overrides of  BIKE1_L1_R2_gf2x_mul_1x1 ...
[22:31:53.407] Branching on 1 override variants of BIKE1_L1_R2_gf2x_mul_1x1 ...
[22:31:53.407] Applied override! BIKE1_L1_R2_gf2x_mul_1x1

The last three lines are then repeated several hundred more times.

We should not be generating such large amounts of repetitive output, at least not at the default verbosity setting. Applying an override is not so notable that it deserves to be called out with an exclamation point every time it happens (unless the user asks for more verbosity). Instead, after symbolic simulation we should print a summary showing how many times each override was used.

[atomb]

Although it wouldn't help in logs, we could use ANSI control codes to replace certain status update lines in place as we go (in addition to the numbers @brianhuffman suggested).

[RyanGlScott]

The "Calling Yices to check sat" and "Running check sat" bits in particular arise from what4. This is because we print out all log messages from what4, regardless of their verbosity:

https://github.com/GaloisInc/saw-script/blob/6bb79b63f9d5812d999834b8142534aab64bc2ec/src/SAWScript/Prover/What4.hs#L202-L205

Note that the first argument to logger is an Int representing the verbosity. The "Calling Yices to check sat" and "Running check sat" have a verbosity of 2, so we could tweak logger to only print out logs with a matching SAW verbosity level if we wanted to.