Hi, can you try to run your programm under the control of strace and see if it is hanging anywhere? I.e. strace -f ./smtrat_2 ... Kind Regards, H.-J. Schnitzer On 2/28/19 11:49 AM, Gereon Kremer wrote:
Hi,
I observe a weird behaviour when using different paths to a binary and an input file. As we know $HOME and $WORK resolve to /home/.../ and /work/... though /home/ and /work/ are symlinks to /rwthfs/rz/cluster/... So it should not make a difference, right?
I have a (statically linked) binary that behaves in a certain way (that I want to debug...) If I call it with the canonical paths I get:
% time /rwthfs/rz/cluster/home/gk809425/smtrat_aklima/build/smtrat_2 /rwthfs/rz/cluster/work/gk809425/benchmarks/QF_NRA/hycomp/ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_4.smt2 (error "expected sat, but returned unsat") /rwthfs/rz/cluster/home/gk809425/smtrat_aklima/build/smtrat_2 64.78s user 0.14s system 99% cpu 1:05.08 total
So it terminates after about 65 seconds. (repeatably)
Now I use the non-canonical paths: % pwd /home/gk809425/smtrat_aklima/build % time ./smtrat_2 $WORK/benchmarks/QF_NRA/hycomp/ball_count_2d_hill.01.seq_lazy_linear_enc_lemmas_global_4.smt2
Which does not terminate for more than four minutes... Also it is CPU-bound, so it does not seem to wait for IO.
Just to be sure: those commands were executed in the same session, so it is the same environment in terms of loaded modules, env variables, etc.
Can anyone guess what is going on here?
Best, Gereon
_______________________________________________ claix18-slurm-pilot mailing list -- claix18-slurm-pilot@lists.rwth-aachen.de To unsubscribe send an email to claix18-slurm-pilot-leave@lists.rwth-aachen.de
-- Hans-Juergen Schnitzer IT Center Abteilung: Systeme und Betrieb RWTH Aachen University Seffenter Weg 23 52074 Aachen Tel: + 49 241 80-28719 Fax: + 49 241 80-628719 schnitzer@itc.rwth-aachen.de www.itc.rwth-aachen.de