session partial_sort_Why3_ide = NTP4Verif +
theories
  "partial_sort_Why3_ide_VCpartial_sort_assign_exit_part5_goal15"
  "partial_sort_Why3_ide_VCpartial_sort_post_reorder_goal2"
  "partial_sort_Why3_ide_VCpartial_sort_assert_rte_unsigned_overflow_goal13"
  "partial_sort_Why3_ide_VCpartial_sort_stmt_post_4_goal22"
  "partial_sort_Why3_ide_VCpartial_sort_loop_inv_lower_established_goal5"
  "partial_sort_Why3_ide_VCpartial_sort_loop_inv_reorder_preserved_goal6"
  "partial_sort_Why3_ide_VCpartial_sort_assert_rte_mem_access_goal11"
  "partial_sort_Why3_ide_VCpartial_sort_post_sorted_goal0"
  "partial_sort_Why3_ide_VCpartial_sort_stmt_post_5_goal24"
  "partial_sort_Why3_ide_VCpartial_sort_loop_inv_bound_preserved_goal3"
  "partial_sort_Why3_ide_VCpartial_sort_post_partition_goal1"
  "partial_sort_Why3_ide_VCpartial_sort_loop_inv_lower_preserved_goal4"
  "partial_sort_Why3_ide_VCpartial_sort_call_swap_pre_2_goal18"
  "partial_sort_Why3_ide_VCpartial_sort_assert_rte_mem_access_2_goal12"
  "partial_sort_Why3_ide_VCpartial_sort_call_swap_pre_goal17"
  "partial_sort_Why3_ide_VCpartial_sort_loop_inv_upper_preserved_goal9"
  "partial_sort_Why3_ide_VCpartial_sort_loop_inv_unchanged_preserved_goal7"
  "partial_sort_Why3_ide_VCpartial_sort_call_push_heap_pre_heap_goal19"
  "partial_sort_Why3_ide_VCpartial_sort_loop_assign_part4_goal14"
  "partial_sort_Why3_ide_VCpartial_sort_stmt_post_goal25"
  "partial_sort_Why3_ide_VCpartial_sort_call_make_heap_pre_valid_goal16"
  "partial_sort_Why3_ide_VCpartial_sort_stmt_post_lower_goal23"
  "partial_sort_Why3_ide_VCpartial_sort_loop_inv_upper_established_goal10"
  "partial_sort_Why3_ide_VCpartial_sort_stmt_post_2_goal20"
  "partial_sort_Why3_ide_VCpartial_sort_stmt_post_3_goal21"
  "partial_sort_Why3_ide_VCpartial_sort_loop_inv_unchanged_established_goal8"
