-no_gc -profile -flat_check se c -require_check se c -ensure_check se c -invariant_check se c -loop_check se c -all_check