[K-Bug] kprove --color modify the order of output when failing

[Robertorosmaninho]

What component is the issue in?

Front-End

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

v6.0.96-0-g35348949c6

Operating System

Linux

K Definitions (If Possible)

This behavior was observed on the imp-haskell test.

Steps to Reproduce

Add --color on to KPROVE_FLAGS on the test Makefile.

Expected Results

1. From krpove's help message:

kprove --help
Usage: kprove [options] <file>
  Options:
...
    --color
      Use colors in output. Default is on.
      Possible Values: [OFF, ON, EXTENDED]

Given that the color should be ON as default, the test shouldn't fail, but it does fail. So the actual behavior isn't aligned with the help's message. One of them should be fixed.

2. The use of --color shouldn't affect the order of the failing output.

[Robertorosmaninho]

See #3642 comments and reviews.

[radumereuta]

We can change the pretty printer in the llvm-backend to check the output w/o colors.
When we convert the collection items into a string, make sure the color flag is off.
@gtrepta can you check if you can include it in runtimeverification/llvm-backend#836

[gtrepta]

It doesn't look like kprove is using the kprint command for output. I also tested the output manually with kprint and the ordering doesn't change between colors being on and off.

Instead, kprove is using the KPrint class in org.kframework.unparser. Still investigating...