[SMT-LIB] a couple of logic issues

[Leonardo de Moura]

Clark,

> You are right.  Sorry.  I meant 0-ary predicates (i.e. Boolean  
> variables).  The
> question is whether we should *always* allow additional Boolean  
> variables or
> only in some logics.

I think we should. Boolean variables are very useful, and all SMT  
solvers
seem to support them. If we disallow them, then we will be forced to  
create
"fake" integer constraints to "represent" boolean variables.

Leonardo