[SMT-LIB] A few general SMTLIB questions

[Morgan Deters]

> I was told by another source that QF_ABV was a renaming of QF_AUFBV, but was confusing and was dropped.
> Just use QF_AUFBV.

Maybe I can clear this up.  QF_AUFBV and QF_ABV are both specified by
SMT-LIB (with and without uninterpreted functions).

Historically, only QF_AUFBV was available, so benchmarks using arrays
and bitvectors had to be categorized under QF_AUFBV, even though they
did not use uninterpreted functions.  When QF_ABV was specified, all
these benchmarks moved from QF_AUFBV to QF_ABV.

So the _logic_ QF_AUFBV was not renamed, but it appeared to do so from
the benchmark library perspective, since all of its benchmarks moved
to a different logic.

Morgan
-- 
Morgan Deters
Postdoctoral Research Scientist
Courant Institute of Mathematical Sciences
251 Mercer St., New York, NY 10012
mdeters at cs.nyu.edu - http://cs.nyu.edu/~mdeters/