[SMT-LIB] status of LRA benchmarks

[Jochen Eisinger]

Hi,

I just ran the tool LIRA on the LRA division from SMTCOMP'09 and got one
"unsound" result: scholl-smt08/RNDPRE/RNDPRE_4_18.smt. My tool
classifies this benchmark as "unsat", but it's listed as "sat".

The formula looks like this:

:formula
(forall (?x1 Real)
  (exists (?x2 Real)
    (forall (?x3 Real)
      (exists (?x4 Real)
        (and
          (and (cons ?x1 ?x2 ?x3 ?x4) (cons ?x1 ?x2 ?x3 ?x4))
          (and (cons ?x1 ?x2 ?x3) (cons ?x1 ?x3)))))))

I replaced the constraints by (cons ...) with the list of variables
occuring in this constraint

since ?x4 doesn't occur in the 2nd branch of the top (and), we can pull
it in. The forall ?x3 can be distributed over the top (and), and on the
2nd branch also over the next (and), so we have a leave like

(forall (?x3 Real) (cons ?x1 ?x2 ?x3))

which equals to false, and therefore, the whole instance equals false.

Did I make a mistake there? How did you classify the LRA benchmarks?

best
-- jochen