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

[Michal Moskal]

On 11/4/06, Leonardo de Moura <leonardo at microsoft.com> wrote:
> This translation of the Simplify benchmarks will be probably substituted by a more faithful one. An interesting suggestion was to add types and use the SMT-LIB array theory in the translation instead of mapping everything to integers like I did.

I think using types is going to be hard, because I guess it would be
hard to tell what the type Elem is - you can store arrays, integers
and other objects in arrays. I guess you would need conversion
operators to be inserted here and there. So in the end I think that
mapping everything to Int was a rather clever hack :)

I noticed these benchmarks to use lots of arithmetic, i.e. my solver
spending lots of time in arithmetic reasoning. Definitely more than
Boogie benchmarks and I guess more than ESC benchmarks I was playing
with previously. This might be because of the true_term being integer
messing with things - which is my problem.

Also did the original benchmarks have PATS directives? If so, I guess
they could be copied to SMT format using annotations.

-- 
   Michał