Hello, I used MRMC on a DTMC model to check a bounded until formula. Depending on the chosen time bounds and error_bound setting, it segfaulted on several occasions. MRMC Version 1.4.1 built from source OS: Debian/testing on amd64 GCC: gcc version 4.4.3 20100108 (prerelease) (Debian 4.4.2-9) Nevertheless it works well on 32 Bit OpenBSD -current with gcc 3.3.5 Is this behavior to be expected on 64 bit systems? Or is it maybe a gcc issue? Sorry if I missed something, but I did not find information about this on the webpage. best regards Matthias -- __________________________________________________________ ___ __ __ Dipl. Inf. Matthias Guedemann / __\/ _\ /__\ Computer Systems in Engineering / / \ \ /_\ Otto-von-Guericke Universitaet Magdeburg / /___ _\ \//__ Tel.: 0391 / 67-19359 \____/ \__/\__/ __________________________________________________________