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