add k annotations for k-induction in contracts

offline_tests/DRAGON_1.lus

offline_tests/DRAGON_10.lus

offline_tests/DRAGON_10_e1_3587_e3_2749.lus

offline_tests/DRAGON_10_e1_998.lus

offline_tests/DRAGON_10_e2_2785_e3_1744.lus

offline_tests/DRAGON_10_e2_402.lus

offline_tests/DRAGON_10_e3_144_e5_2046.lus

offline_tests/DRAGON_10_e3_3429.lus

offline_tests/DRAGON_1_e1_5070.lus

offline_tests/DRAGON_1_e2_1997.lus

offline_tests/DRAGON_2.lus

offline_tests/DRAGON_2_e1_2316.lus

offline_tests/DRAGON_2_e2_3183_e1_2644.lus

offline_tests/DRAGON_2_e2_3183_e2_3580.lus

offline_tests/DRAGON_2_e2_3183_e3_5972.lus

offline_tests/DRAGON_2_e2_4481.lus

offline_tests/DRAGON_2_e7_25_e8_3171.lus

offline_tests/DRAGON_3.lus

offline_tests/DRAGON_3_e1_4783.lus

offline_tests/DRAGON_3_e1_4783_e1_3755.lus