[YICES-HELP] "distinct" predicate

[Levent Erkok]

Hi all,

Is there a "distinct" predicate supported by Yices's own input
language, similar to that of SMT-Lib? Or is this predicate "compiled
away" when Yices reads SMT-Lib inputs?

Since compiling "distinct" away causes the generation of a quadratic
number of inequations, we were thinking Yices might have a custom
predicate for this purpose. If that is the case, is it possible to
access it from Yices's own input language?

Thanks,

Levent Erkok
Galois Inc.