[SMT-LIB] simplify test suite and boogie benchmarks in AUFLIA logic

[Michal Moskal]

Hi,

A while ago I have posted a proposal for a logic for ESC-like software
verifiers. There was little answer, so I figured that as an
intermediate step, I could translate the Simplify test suite and
Boogie benchmarks to the existing AUFLIA logic, by treating everything
as Int.

This is exactly what the current translation (available in SMT LIB) of
the Simplify test suite benchmarks does. The translation doesn't make
use of the builtin arrays, but instead defines its own. We have to
either do this, or define some kind of casting functions (which I
proposed in the emails sent in January).

The main differences between my translation and the currently available are:
- all 2300-something front end test suite benchmarks are translated
(smt lib currently has around 900), I'll be trying to filter out the
ones that require non-linear reasoning and flag them
- small Simplify suite benchmarks are translated - they seem to be much harder
- Boogie benchmarks (from Spec# website) are translated
- I use the native (distinct x y z) predicate instead of (= x (+
dist_1 0)), (= y (+ dist_1 1)), (= z (+ dist_1 2))
- the triggers are preserved:
 (PATS t1 (MPAT t2 t3) t4) => :pat { t1 } :pat { t2 t3 } :pat { t4 }
 (NOPATS t1 t2) => :nopat { t1 } :nopat { t2 }
It would be great if the scrambler would know about it.

The benchmarks can be found here:
 http://nemerle.org/~malekith/smt/benchmarks/
in particular:
 http://nemerle.org/~malekith/smt/benchmarks/boogie-AUFLIA-2007.04.27.tar.bz2
 http://nemerle.org/~malekith/smt/benchmarks/simplify_benchmarks-AUFLIA-2007.04.27.tar.bz2

For boogie, there are three directories: valid, invalid and
non-linear. Valid contains benchmarks that are supposed (by the
authors) to be unsat (and are actually proven unsat by my prover).
Invalid contains test cases that are supposed to be sat. Non-linear
contains testcases that make use of non-linear terms.

Simplify front end test suite benchmarks are all supposed to be valid,
but the following ones:

javafe.ast.Identifier.003.smt
javafe.ast.Identifier.010.smt
javafe.parser.TokenQueue.006.smt
javafe.util.LocationManagerCorrelatedReader.001.smt
javafe.ast.Identifier.008.smt
javafe.parser.TokenQueue.008.smt

contain non-linear terms. The last two don't require the non-linear
terms to be proven valid.

Simplify small suite benchmarks are also supposed to be all valid, I'm
currently testing for linearity.

I hope these benchmarks cases will make into 2007 smt comp.

Cheers!
   Michał