[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