There appears to be a problem involving (potentially) large integers.  The
query

   A<> count >= 2

or even

   A<> false

crashes verifyta on the following system when you ask for a trace (-t 0).   

If the potential range specified for threshold is significantly smaller, a
trace is created with no problems.

==============

urgent chan ch;
int count = 0;
clock clk;

process main ()
{
 int[-2147483648,2147483647] threshold = 0;

 state s1, s2, s3;
 urgent s2, s3;
 init s1;

 trans s1 -> s2 {sync ch?; }, 
       s2 -> s3 {guard 1000 - threshold >= clk; },
          -> s3 {guard 1000 - threshold < clk; };
 }

process startup ()
{

 state s1;
 init s1;

 trans s1 -> s1 {sync ch!; };
 }

system startup, main;

Is it a crash (segfault) or a thrown exception?

On my x86 mac, I'm getting an exception, followed by a segfault (A<> count >=
2) or a double free warning (A<> false).

On other machines (definitely 4.1.0 under linux, possibly 4.0.6 on an older
powerpc mac) it just reports the exception and exits.

=========

% verifyta -t 0 crash.xta crash1.q
Options for the verification:
  Generating some trace
  Search order is breadth first
  Using conservative space optimisation
  Seed is 1225117830
  State space representation uses minimal constraint systems

Verifying property 1 at line 4
 -- Property is NOT satisfied.

 -- Aborted.

EXCEPTION: Cannot generate the trace
zsh: segmentation fault  verifyta -t 0 crash.xta crash1.q

===============

 verifyta -t 0 crash.xta crash2.q
Options for the verification:
  Generating some trace
  Search order is breadth first
  Using conservative space optimisation
  Seed is 1225117954
  State space representation uses minimal constraint systems

Verifying property 1 at line 1
 -- Property is NOT satisfied.

 -- Aborted.

EXCEPTION: Cannot generate the trace
verifyta(802) malloc: *** error for object 0x202130: double free
*** set a breakpoint in malloc_error_break to debug

Revision 4054 fixed the reason of the exception but the exception crash on
MacOS is still not fixed.

Experiments on MacOS X 10.5 generated the exception without the segfault. It
may be related to a specific version of MacOS X. This bug is fixed but if
segfaults occur again when exceptions are thrown please open a new bug.