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

[Domagoj Babic]

Hi,

Encoding some software verification benchmarks to Yices and new
SMT modular arithmetic format without UIFs, I ran into a type inconsistency:

BitVec[1] is type-incompatible with bool, which is weird, at best.

Since current QF_UFBV32 logic does not allow BitVec[1] type, I assumed
that this is just a cosmetic modification, but Clarke B. pointed out that
this modification would require changes in the underlying logic.

Questions:
1) Is it possible to modify the underlying bitvector logic to fix this
inconsistency?
Example:
:extrafuns ((a b c BitVec[1]))
:extrafuns ((d BitVec[2]))
:assumption (= a (= (bvxor b c) bv0))
:assumption (= d (concat b c))

2) I'm still not clear about bit-vector sizes. The benchmarks I have generated
so far use up to 64-bits, so I added
:notes { maxbits 64 }
which specifies the maximum number of bits required to do all the computation
to solve the benchmark. Any other suggestions?

3) I just noticed that the new operators that were recently proposed suggest
bv(s)mod instead of bv(s)rem. That should be fixed.


If all three suggestions are accepted, I can make the benchmarks available
today...

Regards,
             Domagoj Babic