;;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"