[SMT-COMP] SMT-COMP 2016: Incorrect Answers (Unknown Track)

[Tung Vu Xuan]

Hi,

I am the developer of raSAT.


> > More interestingly, raSAT seems to be printing unsat on timeouts
> > (which is a bit worrying considering that this didn't show up in the
> > main competition).
>
> It actually showed up also in the main track: see
> http://smtcomp.sourceforge.net/2016/results-QF_NIA.shtml
>
> The raSAT developer is aware of the issue.
>

This dues to the behavior of the shell script which is used for wrapping
raSAT 0.3. When being killed, the script stops the current command and
continues to execute the remaining commands which include printing "unsat".
In raSAT 0.4, we changed the script language to Python due to the demand of
parallelism, and the script works as expected in terms of stopping
immediately when being killed.

For this reason, when analyzing the unknown benchmarks, I think we can
safely ignore the "unsat" answers on timeouts of raSAT 0.3.

Best,
Tung.