anchor.diff:          ///     Test cases for checking unification.
           /// </summary>
           static member Unifies =
  -            [ TestCaseData(("unlock_V1", "unlock_V0"))
  +            [ TestCaseData(("unlock_V001", "unlock_V000"))
                   .Returns(
                       Some <|
                       { Nodes =
                             Map.ofList
  -                              [ ("unlock_V0",
  +                              [ ("unlock_V000",
                                    (Mandatory <|
                                     Multiset.singleton
                                        (gfunc BTrue "holdLock" [] ),
                                     EntryExit)) ]
                         Edges =
                             Map.ofList
  -                              [ ("unlock_C0",
  -                                 edge "unlock_V0"
  +                              [ ("unlock_C000",
  +                                 edge "unlock_V000"
                                         [ command "!I++"
                                                 [ Int "serving" ]
                                                 [ SMExpr.Int (siBefore "serving") ]]
  -                                      "unlock_V0" ) ] } )
  +                                      "unlock_V000" ) ] } )
                   .SetName("unify C1 into C0 on the ticket lock 'unlock'")
  -              TestCaseData(("unlock_V0", "unlock_V1"))
  +              TestCaseData(("unlock_V000", "unlock_V001"))
                   .Returns(
                       Some <|
                       { Nodes =
                             Map.ofList
  -                              [ ("unlock_V1", (Mandatory <| Multiset.empty,
  +                              [ ("unlock_V001", (Mandatory <| Multiset.empty,
                                                  EntryExit)) ]
                         Edges =
                             Map.ofList
  -                              [ ("unlock_C0",
  -                                 edge "unlock_V1"
  +                              [ ("unlock_C000",
  +                                 edge "unlock_V001"
                                         [ command "!I++"
                                                 [ Int "serving" ] 
                                                 [ SMExpr.Int (siBefore "serving") ]]
  -                                      "unlock_V1" ) ] } )
  +                                      "unlock_V001" ) ] } )
                   .SetName("unify C0 into C1 on the ticket lock 'unlock'")
  -              TestCaseData(("unlock_V0", "unlock_V2"))
  +              TestCaseData(("unlock_V000", "unlock_V002"))
                   .Returns(None)
                   .SetName("unifying into non-existent nodes fails")
  -              TestCaseData(("unlock_V2", "unlock_V0"))
  +              TestCaseData(("unlock_V002", "unlock_V000"))
                   .Returns(None)
                   .SetName("unifying non-existent nodes fails")
  -              TestCaseData(("unlock_V0", "unlock_V0"))
  +              TestCaseData(("unlock_V000", "unlock_V000"))
                   .Returns(Some Studies.ticketLockUnlockSubgraph)
                   .SetName("unifying a node onto itself does nothing") ]
   
  
positive.code:                                              Typed.Int (siBefore "ticket")]] },
                             Set.empty,
                             Entry)))
                          ("lock_V1",
                           (Mandatory <| Multiset.singleton (gHoldTick BTrue),
                            Set.singleton
                                { Name = "lock_C4"
                                  Dest = "lock_V3"
                                  Command = [] },
                            Set.singleton
                                { Name = "lock_C0"
                                  Src = "lock_V0"
                                  Command =
                                      [ command "!ILoad++"
                                             [ Int "t"; Int "ticket"; ]
                                             [ Typed.Int (siBefore "t")
                                               Typed.Int (siBefore "ticket") ]] },
                            Normal ))
                          ("lock_V2",
                           (Mandatory <| Multiset.singleton (gHoldLock BTrue),
                            Set.empty,
                            Set.singleton
                                { Name = "lock_C3"
                                  Src = "lock_V4"
                                  Command =
                                      [ command "Assume" []
                                             [ Typed.Bool
                                                   (iEq (siBefore "s")
                                                        (siBefore "t")) ]] },
                             Exit))
                          ("lock_V3",
                           (Mandatory <| Multiset.singleton (gHoldTick BTrue),
                            Set.singleton
                                { Name = "lock_C1"
                                  Dest = "lock_V4"
                                  Command =
                                      [ command "!ILoad" 
                                             [ Int "s" ]
                                             [ Typed.Int (siBefore "serving") ]] },
                            Set.ofList
                                [ { Name = "lock_C2"
                                    Src = "lock_V4"
                                    Command =
                                        [ command "Assume" []
                                               [ Typed.Bool
                                                     (BNot (iEq (siBefore "s")
                                                                (siBefore "t"))) ]] }
                                  { Name = "lock_C4"
                                    Src = "lock_V1"
                                    Command = [] } ],
                             Normal))
                          ("lock_V4",
                           (Mandatory <|
                            Multiset.ofFlatList
                                [ gHoldLock (iEq (siVar "s") (siVar "t"))
                                  gHoldTick (BNot (iEq (siVar "s") (siVar "t"))) ],
                            Set.ofList
                                [ { Name = "lock_C2"
                                    Dest = "lock_V3"
                                    Command =
                                        [ command "Assume" []
                                               [ Typed.Bool
                                                     (BNot (iEq (siBefore "s")
                                                                (siBefore "t"))) ]] }
                                  { Name = "lock_C3"
                                    Dest = "lock_V2"
                                    Command =
                                        [ command "Assume" []
                                               [ Typed.Bool
                                                     (iEq (siBefore "s")
                                                          (siBefore "t")) ]] } ],
                            Set.singleton
                                { Name = "lock_C1"
                                  Src = "lock_V3"
                                  Command =
                                      [ command "!ILoad"
                                             [ Int "s" ]
  
negative.code:             { Name = "unlock"
                Contents =
                    Map.ofList
                        [ ("unlock_V000",
                           (Mandatory <|
                            Multiset.singleton
                                    (gfunc BTrue "holdLock" [] ),
                            Set.singleton
                                { Name = "unlock_C000"
                                  Dest = "unlock_V001"
                                  Command =
                                      [ command "!I++" 
                                             [ Int "serving" ]
                                             [ Typed.Int (siBefore "serving") ]] },
                            Set.empty,
                            Entry))
                          ("unlock_V001",
                           (Mandatory <| Multiset.empty,
                            Set.empty,
                            Set.singleton
                                { Name = "unlock_C000"
                                  Src = "unlock_V000"
                                  Command =
                                      [ command "!I++"
                                             [ Int "serving" ]
  