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

[Michal Moskal]

On 5/2/07, Clark Barrett <barrett at cs.nyu.edu> wrote:
>  The first occurrence of distinct is fine.  It labels
> a set of symbolic constants as distinct.  The second occurrence, however, is
> stating that a set of integers are distinct.  This is implied by the underlying
> theory and as such, this is the sort of assumption we don't want too have to
> include in SMT-LIB.  Do you have any objection to removing these instances of
> distinct?  I can do it on my end unless you don't mind another round...

I've put updated tarball with no distinct-integers stuff, here:
http://nemerle.org/~malekith/smt/benchmarks/simplify_benchmarks-AUFLIA-2007.05.03.tar.bz2

The boogie benchmarks do not contain it.

-- 
   Michał