For code using bvExtract to get a single bit on a signed value (SInt64 say), we produce a signed-1-bit value. But the C-compiler doesn't support this. (It does support 1-bit unsigned bit-vectors; though I suspect that might be wrong too; probably a relic from the days when 1-bit bit vector was used to model booleans?
Either we should just not support 1-bit bit-vectors (signed or unsigned) in the C code generator; or make sure it both works.
For code using bvExtract to get a single bit on a signed value (SInt64 say), we produce a signed-1-bit value. But the C-compiler doesn't support this. (It does support 1-bit unsigned bit-vectors; though I suspect that might be wrong too; probably a relic from the days when 1-bit bit vector was used to model booleans?
Either we should just not support 1-bit bit-vectors (signed or unsigned) in the C code generator; or make sure it both works.