> The attached stp formula produces the following error:
> Fatal Error: BVConstEvaluator:division by zero error
Thanks for the bug report.
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