[SMT-LIB] :status unknown AUFLIA benchmarks

[Michal Moskal]

On 11/14/06, Paulo J. Matos <pocm at soton.ac.uk> wrote:
> 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?

Only as far as I believe my prover. For quite some time I haven't find
any soundness bugs, but of course there can be some. This is why I'm
asking, if any other prover also said the benchmarks were unsat.

> Can you prove them?

As in ,,generate some kind of formal proof''? I guess not.

-- 
   Michał