[Termtools] Memory problems

Johannes Waldmann johannes.waldmann at htwk-leipzig.de
Thu Mar 21 18:38:50 CET 2019


Hi Jera,


> 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


> Moreover, there are many timeouts where it should probably be „StarExec error“. 

Example?


> 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  ...


- Johannes.


More information about the Termtools mailing list