val my_lprog_main_start_pc_index : Prims.int
let my_lprog_main_start_pc_index = 0
module MyRegularToAtomicRefinement

open Armada.Action
open Armada.Base
open Armada.BinaryOp
open Armada.Expression
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Type
open FStar.Tactics.V2
open MyAtomicLProg
open MyLProg
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.Atomic
open Strategies.PCIndices
open Strategies.RegularToAtomic
open Strategies.RegularToAtomic.Armada
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.ImmutableArray
open Util.Nth
open Util.Range

// This is all the PCs in the program.

let my_lpcs: array_t pc_t = list_to_array [ "main.0"; "main.1"; "main.2"; "main.3"; "main.4"; "main.5" ]

// The start PC is "main.0", which is the 0th element of the my_lpcs array.
/
Util.Range.fsti.checked Util.Nth.fst.checked Util.ImmutableArray.fsti.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.RegularToAtomic.Armada.fsti.checked Strategies.RegularToAtomic.fsti.checked Strategies.PCIndices.fst.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked MyLProg.fst.checked MyAtomicLProg.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Expression.fst.checked Armada.BinaryOp.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
MyRegularToAtomicRefinement.fst
Prims.int
let my_lprog_main_start_pc_index =
  
0