For certain queries the results are unstable (i.e. "Property is satisfied.",
"Property is not satisfied." and Unexpected server crash/segmentation fault).

This is best reproducible with "Reuse" turned off, all other options are at
their default (Produced with UPPAAL 4.0.8 (rev. 4276), March 2009).

The queries that produce these unstable results are:
nodes(1).UpdateEnergy --> nodes(1).hasValidRoute()
nodes(2).UpdateEnergy --> nodes(2).hasValidRoute()
nodes(3).UpdateEnergy --> nodes(3).hasValidRoute()
nodes(4).UpdateEnergy --> nodes(4).hasValidRoute()

Created an attachment (id=222) [details]
Models

Simple model of a wireless sensor network:

"Environment" produce energy for the nodes.
"BaseStation" collects all packages routed to sink.
"Node" produce packages through the "Application" and route packages through
the network. Nodes also model a dynamic routing protocol which modify the
routes based on available energy in neighbouring nodes.

The system consists of one base station, four nodes and an environment. The
nodes are positioned as following (0 is the base station):

0 - 1 - 2 - 3
        |
        4

the lines represent radio connections (synchronisations). The nodes uses
channels for routing packages and broadcast channels for updating information
about neighbours.

Created an attachment (id=223) [details]
The queries for the model

The interesting queries are:

nodes(1).UpdateEnergy --> nodes(1).hasValidRoute()
nodes(2).UpdateEnergy --> nodes(2).hasValidRoute()
nodes(3).UpdateEnergy --> nodes(3).hasValidRoute()
nodes(4).UpdateEnergy --> nodes(4).hasValidRoute()

which give a new result for each verification with the stable release 4.0.8

When trying to reproduce the bug with the latest developer version (UPPAAL
4.1.1 (rev. 4276), March 2009) the server crashes/segfaults every time.

Using the command line verifyta produce the same results as through the GUI
(for both the stable release and the developer version respectively).

i.e.: 
(Academic) UPPAAL 4.0.8 (rev. 4276), March 2009
Copyright (c) 1995 - 2009, Uppsala University and Aalborg University.
All rights reserved.
Compiled with g++-4.3.3 -Wall -DNDEBUG -O3 -ffloat-store -fgcse-las -fgcse-lm
-fgcse-sm -ftree-loop-linear -funswitch-loops -ftree-loop-im -fivopts
-ftree-vectorize -ftracer -march=pentiumpro -DLIBXML_STATIC   
-DBOOST_DISABLE_THREADS
Free for academic and non-commercial use only.

produce either of:
 -- Property is satisfied.
 -- Property is NOT satisfied.
segmentation fault

-------------------
(Academic) UPPAAL 4.1.1 (rev. 4276), March 2009
Copyright (c) 1995 - 2009, Uppsala University and Aalborg University.
All rights reserved.
Compiled with g++-4.3.3 -Wall -DNDEBUG -O3 -ffloat-store -fgcse-las -fgcse-lm
-fgcse-sm -ftree-loop-linear -funswitch-loops -ftree-loop-im -fivopts
-ftree-vectorize -ftracer -march=pentiumpro -DLIBXML_STATIC
-DENABLE_ROBUST_REACHABILITY -DENABLE_CSS_MERGE    -DBOOST_DISABLE_THREADS
Free for academic and non-commercial use only.

constantly produce segmentation fault.

By the way: when I wrote all other options are at their default, i mean that I
use:
Search order: Breath first
State space reduction: Conservative
State space representation: DBM
Diagnostic trace: None
Extrapolation: Automatic
Hash table size: 16M
Reuse: Off

This is true for all the tested versions.

The problem has been identified although no fix is currently available.

Avoid using sub-expressions in queries of the form name(index).call(arg)
where "name" is a process name (of a process set), "index" some index (constant
or not), "call" a function name local to the process, and "arg" its
arguments. Other references like locations or variables are fine. Just
avoid calling local functions for the time being.

Fixed in rev. 4370 (trunk) and rev. 4372 (4.0.9).