[Termtools] competition results - some comments

Fabian Emmes emmes at cs.rwth-aachen.de
Fri Jan 29 13:38:16 CET 2010


Dear Simon,

On 29. Jan, 11:58, Simon Bailey wrote:
> fabian,
>
> On 29 Jan 2010, at 11:40, Fabian Emmes wrote:
>> On 29. Jan, 11:25, Simon Bailey wrote:
>>> jboss at termcomp$ echo $PATH
>>> /usr/kerberos/bin:/usr/local/bin:/bin:/usr/bin
>>> [...]
>>> jboss at termcomp$ which minisat-core
>>> /usr/local/bin/minisat-core
>>> jboss at termcomp$ minisat-core
>>> This is MiniSat 2.0 beta
>>> [...]
>>
>> looks like we missed the binary by a single character... AProVE-COLOR
>> expects MiniSat2.0 as "minisat2core", not "minisat-core". Could you
>> create an appropriate symlink, please?
>
>
> i can do this. however, carsten otto stated in an email date 18/Dec/08 @ 
> 13:10 that "minisat2core is a stripped down version of minisat2"(*). is 
> the minisat2core required by aprove _really_ the same as minisat-core 
> from the minisat archive?
>
> ((*) see http://lists.lri.fr/pipermail/termtools/2008-December/000714.html)
>
> please clarify. if there is no functional difference, i see no problem  
> with adding the symlink.

Yes, this binary is built from the same source as the one we submitted
in the non-COLOR versions of AProVE. So it will most probably give
similar results. Although we would prefer if you could use the
minisat2core binary from one of the other AProVE zips (since we did all
our tests with this version), it would also be sufficient, if you just
created a symlink to the mentioned minisat-core binary.

Best regards,
Fabian
-- 
Fabian Emmes           mailto:emmes at informatik.rwth-aachen.de
LuFG Informatik 2      http://verify.rwth-aachen.de/emmes/
RWTH Aachen            phone: +49 241 80-21241
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 197 bytes
Desc: Digital signature
Url : http://lists.lri.fr/pipermail/termtools/attachments/20100129/5d75f0f5/attachment.pgp 


More information about the Termtools mailing list