[smt] negative BitVectorLit value about uclid HOT 4 CLOSED

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.

from uclid.

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.

from uclid.

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!

from uclid.

Fixed in the private repo.

from uclid.