[SMT-LIB] (distinct ...) in AUFLIA/simplify benchmarks

[Michal Moskal]

Hi,

I (and I guess not only I :-) have noticed that you use the following
encoding for (DISTINCT ...) Simplify opertor:

(and (= t1 (+ c 1)) (= t2 (+ c 2)) ...)

which is quite strange for me, as smt-lib format also provides
(distinct ...) operator.

I guess this is not in line with ,,catch benchmarks as they are in the
wild'' principle. It causes performance problems in my prover [1], and
it (at least) used to cause problems in Zap.

I attach a perl script that can be run on all AUFLIA/simplify
benchmarks to fix the problem. It would be great if you could apply it
on official smt-lib.

[1] http://nemerle.org/~malekith/smt/en.html

-- 
   Michał