It looks like the following model does not work as expected when using verifyta.
It works ok in the GUI simulator. I have a global state variable (my_state)
which is a structure that contains another structure as its member. This member
structure in turn is another structure which contains an array of yet another
structure. I try to add an element to this array member thru a function. 
Basically I am expecting the state to be as follows after I call the init_func(). 

my_state.astruct_set.members[0].handle=2 

This is true when I run the GUI simulator. But when I run verifyta as follows

verifyta -N -d -t 1 verify_ta_test.xta verify_ta_test.q

I get the following in the trace 

State:
( P0.S1 )
my_state.astruct_set.members[0].handle=0 .....
my_state.astruct_set.currsize=0...
Transitions:
  P0.S1->P0.S0 { 1, tau, i := init_func() }

State:
( P0.S0 )
my_state.astruct_set.members[0].handle=3 .....
my_state.astruct_set.currsize=0...

Note that the value of the handle member is 3 rather than 2
and the value of the currsize member is still 0 rather than 1.

verify_ta_test.xta
===================

typedef struct
{
  int handle;
} AStruct;

typedef struct
{
  AStruct members[5];
  int currsize;
} AStruct_Set;

typedef struct 
{
  AStruct_Set astruct_set;
} My_State;

My_State my_state;

int add_to_set(AStruct_Set& set, AStruct astruct)
{
  set.members[set.currsize] = astruct;
  ++(set.currsize);
  return 0;
}

AStruct astruct = {2};

int init_func()
{
  add_to_set(my_state.astruct_set, astruct);
  return 0;
}


process P0() {
int i;state Final, S0, S1;
init S1;
trans S0 -> Final {  },
S1 -> S0 { assign i = init_func();  };
}
//Insert process assignments.

//Edit system definition.
system P0;

verify_test_ta.q
================
E<> P0.Final