search

runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
36 stars 23 forks source link

kore-proof-trace should print the rules from domains.md, as well #1124

Open dlucanu opened 3 months ago

dlucanu commented 3 months ago

Now, the command

kore-proof-trace --expand-terms --verbose  header hints <k-def>-kompiled/definition.kore

prints only the rules from the <k-def>. To manually analyze the proof hints, it would be helpful to it display the rules from domains.md, as well.