val optional_pc_matches_optional_pc_index
      (pcs: array_t pc_t)
      (optional_pc: option pc_t)
      (optional_index: option nat)
    : GTot bool
val optional_pc_matches_optional_pc_index
      (pcs: array_t pc_t)
      (optional_pc: option pc_t)
      (optional_index: option nat)
    : GTot bool
let optional_pc_matches_optional_pc_index
  (pcs: array_t pc_t)
  (optional_pc: option pc_t)
  (optional_index: option nat)
  : GTot bool =
  match optional_pc, optional_index with
  | None, None -> true
  | Some pc, Some n -> pc_matches_pc_index pcs pc n
  | _, _ -> false
module Strategies.PCIndices

open Armada.Action
open Armada.Base
open Armada.Statement
open Spec.Ubool
open Util.ImmutableArray
open Util.List
open Util.Relation

type statement_pc_indices_t = {
  start_pc_index: option nat;
  end_pc_index: option nat;
  create_thread_initial_pc_index: option nat;
  method_call_return_pc_index: option nat;
}

let pc_matches_pc_index
  (pcs: array_t pc_t)
  (pc: pc_t)
  (n: nat)
  : GTot bool =
  n < array_len pcs && pc = array_index pcs n
/
Util.Relation.fst.checked Util.List.fst.checked Util.ImmutableArray.fsti.checked Spec.Ubool.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Statement.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.PCIndices.fst

    pcs: Util.ImmutableArray.array_t Armada.Base.pc_t ->
    optional_pc: FStar.Pervasives.Native.option Armada.Base.pc_t ->
    optional_index: FStar.Pervasives.Native.option Prims.nat
  -> Prims.GTot Prims.bool
Util.ImmutableArray.array_t Armada.Base.pc_t FStar.Pervasives.Native.option Prims.nat FStar.Pervasives.Native.Mktuple2 Strategies.PCIndices.pc_matches_pc_index Prims.bool
let optional_pc_matches_optional_pc_index
      (pcs: array_t pc_t)
      (optional_pc: option pc_t)
      (optional_index: option nat)
    : GTot bool =
  
match optional_pc, optional_index with
| None, None -> true
| Some pc, Some n -> pc_matches_pc_index pcs pc n
| _, _ -> false