[SMT-LIB] Bool as alias for BitVec[1]

[Clark Barrett]

> I will submit a thm prover (Spear) that handles only modular arithmetic
> (the translator can also chew some UIFs, but you can't push it too far).

OK, well that is one compelling reason to split off the UF's.

> About benchmarks: I've started the generation process. It is not a
> problem to generate an extremely large number of benchmarks, the problem
> is to generate hard ones --- Spear solves 99% of them in a couple of seconds.
> Anyways, I will certainly be able to provide you with enough hard benchmarks
> to open QF_BV64 category.

Great!

> > > - replace mod by rem
> >
> > :)
> 
> Heh, look, it's like saying: our logic supports operator PLUS, but since
> it initially seemed to us to be MINUS, we are calling it MINUS.
> Later, when we figured out the difference, we still decided to keep
> calling it MINUS, no matter what. :-)

I respectfully disagree.  The "%" operator is called the modulus operator in C.
"mod" may mean different things in other languages or contexts, but using
"bvmod" for an operator whose semantics are the same as the C *modulus* operator
certainly makes sense in benchmarks derived from C programs (of which we have
many).  So you can justly accuse us of being C-centric in our nomenclature, but
saying it is outright wrong is overstating the issue.

In any case, I hope we can agree to disagree on this and focus on other more
useful discussion points.

> Please do consider using a larger set - excitement of incoming results
> is great, but a large set of diverse benchmarks will do even more for the
> field.

If you look at the rules (see www.smtcomp.org/rules.pdf), you will see that we
do try very hard to get a diverse set of benchmarks.  That said, we will
consider whether we can use a larger set.

-Clark