[smt] negative BitVectorLit value

[ekiwi]

I was just going through the uclid.smt patches that I have lying around and I found one that might be interesting to the broader community.
It deals with a negative value in the BitVectorLit class [src].
The way the current serialization code is written is not compatible with value < 0:

override def toString = "(_ bv" + value.toString + " " + width.toString +")"

If value is negative this yields an invalid SMTLib expression.

My quick way of fixing this was to add an assert:

  Utils.assert(value >= 0, s"Value $value is negative. Negative BitVector literals are not supported.")

Another way of dealing with this would be to take the bits of the two complements integer and turn those into a string which would also yield a valid SMTLib expression.

As an example: BitVectorLit(-2, 3).toString could yield #b110 or alternatively (_ bv6 3).

[pramodsu]

Thanks for pointing this out, Kevin.

Could you make a pull request on the private repo? I'll merge and push the change over here.

[ekiwi]

Could you make a pull request on the private repo? I'll merge and push the change over here.

I can make a pull request for the quick-fix, i.e., using the assertion. If you are interested in allowing negative values and then converting them to bits using two's complement, I could also try to implement that, it will just take a bit more time.
Let me know what you prefer.

Just FYI: I think some of my prior uclid.smt patches might be missing from your private fork.

[pramodsu]

Please do make the PR for the quick-fix. If you have time to make the full fix, that would be great as well.

Unfortunately, the public and private repos don't share history so it is possible we lost patches submitted only to the public repo. Can you point me to the patches and I will redo them in the private repo?

Thanks!

[ekiwi]

Fixed in the private repo.