When running the appended model using verifyta -t2 todavid.xml, verifyta shows the error: EXCEPTION: Clock valuation The model is found at: http://www.cs.aau.dk/~kyrke/download/uppaal-verifyta-error.tar.gz
Fixed in rev. 4335.