[SMT-LIB] :status unknown AUFLIA benchmarks

[Paulo J. Matos]

On 11/14/06, Michal Moskal <michal.moskal at gmail.com> wrote:
> Hi,
>
> there are 19 benchmarks in the AUFLIA tarball are marked "unknown". My
> prover says there are all unsat (and rather easy except for
> AUFLIA/simplify/javafe.PrintSpec.12.smt).
>
> I wonder how was the status determined? Can anyone confirm the unsat status?
>

My guess is that they are quantified formulas to which nobody has
proved a given result to be correct. Are you sure your unsat results
are correct? Can you prove them?

Regards,

Paulo Matos

> --
>    Michał
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>
>


-- 
Paulo Jorge Matos - pocm at soton.ac.uk
http://www.personal.soton.ac.uk/pocm
PhD Student @ ECS
University of Southampton, UK