Add more tips on how to debug Kontrol proofs

[palinatolmach]

We should add some suggestions on how the user can try to debug the failing/crashing proof in Kontrol, which can include tips on how to

• increase SMT solver timeout (--smt-timeout N, in ms)
• change SMT solver tactics (--smt-tactic '(check-sat-using qfnra-nlsat)' or --smt-tactic '(check-sat-using smt)'
• detect overflows and ignore them using assumptions or unchecked {} blocks`, e.g., for

{ true #Equals notBool #lookup ( ?STORAGE:Map , 2 ) <=Int chop ( #lookup ( ?STORAGE:Map , 2 ) +Int 1 ) }