The attached stp formula produces the following error:

   Fatal Error: BVConstEvaluator:division by zero error

There is division in the formula, but the divisor is symbolic, and
does not have to be zero.  I think it is a bug.

Thanks,

Ed

divzerobug.stp < 1K Download

Hi Edward,

STP's implementation of division in the CVC language is to not allow
division by zero. That is, STP produces an error if a division by zero
occurs in the counter-example.  I don't know what the semantics should be
for the language. In the CVC3 user guide  (
http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html ), when x is a real,  
they evaluate x/0 to zero. So maybe we should do the same for bit-vectors,
I've not changed the semantics for division by zero because I don't know if
anyone relies on the current semantics.

For input in the SMT-LIB1 and SMT-LIB2 languages, STP breaks with the
official semantics and defines x/0 as 1, and x%0 as x.

If these semantics don't seem right to you, let me know what you think they
should be,

Best,

Trevor.

I think these semantics are okay; there does not seem to be a "right"
semantics for this.  However, maybe the error message should specify
that division by zero is an error in the semantics.   I was expecting
smtlib/cvc3 semantics for division, so when I saw the BVConstEvaluator
message, I thought it was a bug, rather than a semantics decision.

Thanks,
Edward