`bvsnego` or `bvnego`

[LeventErkok]

Since the overflow predicates aren't quite formalized in SMTLib yet, perhaps this is a non-issue.

The best source I can find defining these predicates is an email to the mailing list: https://cs.nyu.edu/pipermail/smt-lib/2015/000954.html

This document stipulates bvsnego for checking overflow of signed-unary-negation. Looks like z3 implemented this with the name bvnego.

Is this discrepancy intended?

[LeventErkok]

@aehyvari Based on the commit history, I think you're the right one to answer this..

[aehyvari]

Hi @LeventErkok I'll have a closer look at what you reported when I'm at the keyboard. Meanwhile, here's a more recent thread on the topic https://groups.google.com/u/1/g/smt-lib/c/J4D99wT0aKI

[LeventErkok]

Ah, indeed that newer thread stipulates bvnego. But that seems inconsistent: We also don't have bvudivo, but the signed-version is called bvsdivo (not bvdivo).

Perhaps it's best to contact the SMTLib folks to make sure they're aware of this discrepancy.

[LeventErkok]

@aehyvari I sent a note to the SMTLib mailing list: https://groups.google.com/u/0/g/smt-lib/c/J4D99wT0aKI

[LeventErkok]

Clark responded:

Here's the rationale for the current naming scheme.

If there's an existing bv operator that can overflow in exactly one way, we just add "o" to the name of the operator. This is the case for bvneg and bvsdiv. If an operator can overflow in more than one way, then we add "u" or "s" to disambiguate it, which is why we have bvuaddo and bvsaddo, etc.

I do see your point, but on the other hand, we don't have a bvsneg operator, and bvneg can only overflow in one way, so in that sense, I think it's better to just stick with bvnego.

-Clark

I think this is confusing, but at least there's some rationale behind it.

Closing the ticket as a no-op.