[SMT-LIB] BitVectors32

[Christoph M. Wintersteiger]

Hi!

On Thu, 2006-12-28 at 16:33 -0500, Clark Barrett wrote:
> Theory predicates are supposed take arguments of equal size.  Are you
> suggesting something different?


> I'm not sure what you mean by this.  The semantics of SMT-LIB do *NOT* allow a
> term of sort BitVec[1] to be used where a formula is expected.  So in what way
> are variables of sort BitVec[1] implicitly assumed to be Boolean?

I'm so sorry I even brought this up - of course both problems were bugs
in my typechecker here. Sometimes holidays can really change how you
look at your code; next time I'll spend more time on looking on my own
stuff before complaining.

About
> What would be the difference between bveq and "="?

I've been thinking that it might be nice to have a version that adjusts
bitvector sizes, so that the smaller one gets filled up with zeros from
the left. 

Christoph.