[Termtools] Memory problems
Hensel, Jera
hensel at informatik.rwth-aachen.de
Thu Mar 21 18:55:33 CET 2019
Hi Johannes,
>> Now that runsolver is used again ...
>
> that was a forced decision because benchexec did not work
> http://lists.lri.fr/pipermail/termtools/2019-March/001223.html
Yes, I see the problem.
>> Moreover, there are many timeouts where it should probably be „StarExec error“.
>
> Example?
For example in SRS Standard, ICFP_2010/137809.xml
>> Since for AProVE, the version of 2018 is used (we did not hand in a new version),
>> the results should be as in 2018.
>
> SRS Relative is finished. When restricted to "common benchmarks"
>
> https://termcomp.imn.htwk-leipzig.de/flexible-table/Query%20%5BCommon%5D/30037/33017
>
> all solvers have exactly equal number of YES and NO to last year.
>
> Except for MnM which is hit by the memory problem.
>
> AProVE seems very conservative with memory -
> your run script has java -Xmx14G -Xms14G ...
> while MnM has java -Xms128G -Xmx128G …
We used the same script with benchexec and did not have these problems. The issue was reported here:
https://www.tapatalk.com/groups/starexec/strange-memouts-t106.html
Best regards,
Jera
More information about the Termtools
mailing list