[SMT-LIB] :status unknown AUFLIA benchmarks

Michal Moskal michal.moskal at gmail.com
Wed Nov 15 17:27:52 EST 2006


On 11/15/06, Clark Barrett <barrett at cs.nyu.edu> wrote:
> At the time these benchmarks were added to the library, no tool parsimg smt-lib
> format could prove these unsat.  I plan to revisit these with updated tools in
> the near future.
>
> Is your tool available?  I like to get confirmation from more than one tool
> whenever possible.

Yes, at the SVN server linked from: http://nemerle.org/~malekith/smt/en.html

If there are problems with compilation the current .NET/mono binaries
are available at: http://nemerle.org/teefam/files/fx7.tgz , in the
same directory there are also mono binaries.

I've applied modification to the benchmark changing the (DISTINCT ...)
encoding used to a real (distinct ...) term. I'm not sure if this is
very important. I attach the script to do that (I think I missed that
in my initial email about it).

-- 
   Michał
-------------- next part --------------
A non-text attachment was scrubbed...
Name: fix-distinct
Type: application/octet-stream
Size: 189 bytes
Desc: not available
Url : /pipermail/smt-lib/attachments/20061116/a4cdaca3/fix-distinct.obj


More information about the SMT-LIB mailing list