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

[Michal Moskal]

On 11/5/06, Michal Moskal <michal.moskal at gmail.com> wrote:
> 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.

It seems the problems are related. For example take the axiom:

 (FORALL (n)
  (PATS (intShiftL 1 n))
  (IMPLIES
   (AND (<= 0 n) (< n 31))
   (<= 1 (intShiftL 1 n))))

It is translated without (PATS ...), which causes the automatic
trigger selection mechanism to select all of (intShiftL 1 n), (<= 0 n)
and (< n 31) as triggers, which of course causes lots of junk
instances to be generated and passed to arithmetic module.

-- 
   Michał