val global_initializers:list initializer_t
val global_initializers:list initializer_t
let global_initializers: list initializer_t =
  [
    { var_id = "a"; iv = InitializerSpecific (ObjectValueAbstract int 0); weakly_consistent = false; } ;
    { var_id = "b"; iv = InitializerSpecific (ObjectValueAbstract int 1); weakly_consistent = false; } ;
    { var_id = "c"; iv = InitializerSpecific (ObjectValueAbstract int 2); weakly_consistent = false; } ;
    { var_id = "d"; iv = InitializerSpecific (ObjectValueAbstract int 3); weakly_consistent = false; } ;
    { var_id = "e"; iv = InitializerArbitrary (ObjectTDAbstract int); weakly_consistent = false; } ;
    { var_id = "f"; iv = InitializerSpecific (ObjectValueAbstract int 1); weakly_consistent = false; } ;
    { var_id = "g"; iv = InitializerSpecific (ObjectValueAbstract int 1); weakly_consistent = false; } ;
    { var_id = "h"; iv = InitializerSpecific (ObjectValueAbstract int 0); weakly_consistent = false; }
  ]
module MyHProg

open Armada.Action
open Armada.Base
open Armada.BinaryOp
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Type
open Spec.Behavior
open Spec.Ubool

/// level MyHProg
/// {
///   ghost var a: int := 0;
///   ghost var b: int := 1;
///   ghost var c: int := 2;
///   ghost var d: int := 3;
///   ghost var e: int;
///   ghost var f: int := 1;
///   ghost var g: int := 1;
///   ghost var h: int := 0;
///
///   method main ()
///   {
///     ghost var x: int := 0;
///
///     e := g;  // This is the only statement differing from level MyLProg
///     atomic {
///       a := c;
///       d := b;
///       e := e;
///     }
///     f := f / f;
///   }
/// }
/
Spec.Ubool.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.BinaryOp.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
MyHProg.fst
Prims.list Armada.Init.initializer_t
Prims.Cons Armada.Init.initializer_t Armada.Init.Mkinitializer_t Armada.Init.InitializerSpecific Armada.Type.ObjectValueAbstract Prims.int Armada.Init.InitializerArbitrary Armada.Type.ObjectTDAbstract Prims.Nil
let global_initializers:list initializer_t =
  
[
  { var_id = "a"; iv = InitializerSpecific (ObjectValueAbstract int 0); weakly_consistent = false };
  { var_id = "b"; iv = InitializerSpecific (ObjectValueAbstract int 1); weakly_consistent = false };
  { var_id = "c"; iv = InitializerSpecific (ObjectValueAbstract int 2); weakly_consistent = false };
  { var_id = "d"; iv = InitializerSpecific (ObjectValueAbstract int 3); weakly_consistent = false };
  { var_id = "e"; iv = InitializerArbitrary (ObjectTDAbstract int); weakly_consistent = false };
  { var_id = "f"; iv = InitializerSpecific (ObjectValueAbstract int 1); weakly_consistent = false };
  { var_id = "g"; iv = InitializerSpecific (ObjectValueAbstract int 1); weakly_consistent = false };
  { var_id = "h"; iv = InitializerSpecific (ObjectValueAbstract int 0); weakly_consistent = false }
]