The examples are from the domain of bit-precise software verification
and were generated by our SMT solver Boolector.  They are all UNSAT and 
belong to the category APPLICATIONS. The examples represent verification 
instances for the following kind of algorithms:

countbits: count 1-bits
icbrt: compute integer cube root
isqrt: compute integer square root
maxand, maxor, maxxor: propagate maximum bound through logical operator
minand, minor, minxor: propagate minimum bound through logical operator
maxxororand, minandmaxor, minxorminand: equivalence check of bound propagation
mulhs: compute high-order half of bit-vector multiplication (Mult High Signed)
smulo: compute signed bit-vector multiplication overflow


Contributor:   Robert Brummayer
Email:         robert.brummayer@gmail.com
