Use Lumberjack for crux output of messages, exceptions, CruxSimulation, and ProvedGoals.

[kquick]

This also standardizes the output for various front-ends, ergo the changes in the golden test results, which are all just wording and formatting changes, nothing substantive.

The general approach here is to move the formatting of output into the LogAction provided by lumberjack. In the core code, anything which should be output or logged is done via a call with the original, structured object. The LogActions are usually created at initialization time and different LogActions can be used for different configurations (e.g. if Crux is outputting to something like an IDE, it could use a LogAction that emits JSON-formatted messages instead of the colorized, human readable messages that the default loggers emit). By passing the structure object to the output routine, more decisions can be made on how to handle the output.

[RyanGlScott]

Assuming CI passes, LGTM.

[atomb]

This is excellent. I love having more consistent output from all of the Crux instantiations. I don't see any changes to the crux-mir test output files, though. Do they still go through?

[kquick]

This is excellent. I love having more consistent output from all of the Crux instantiations. I don't see any changes to the crux-mir test output files, though. Do they still go through?

Thanks!

Not all of crux-mir is passing yet; I don't have the right configuration to run them locally, so I'm patching them up based on CI results and will get them green before I merge.

[robdockins]

Seems like a good improvement to me!

[spernsteiner]

I looked at the crux-mir .good files and they all look good to me. The "test foo::bar: FAILED" lines are all unchanged, so it still matches the cargo test output.

Is it intentional that crux-mir now prints every counterexample twice (once under foo::bar counterexamples and again under final results)? If so, that's fine, I just wanted to check in case it's a bug.