runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
444 stars 147 forks source link

add command line flag to enable debug info in proof trace #4483

Closed dwightguth closed 3 months ago

dwightguth commented 3 months ago

This PR adds a flag to kompile which propogates the effect of a lower-level flag to llvm-kompile which assists with debugging the proof hints that are created.