1 2 3 4 5 6 7
;;The files of proof-obligations are: ;;Invariant0.smt ;;Initialization1.smt ;;Operation2.smt ;;Operation3.smt;; If you want to prove it then execute the "switch1.sh"