Bug in SBVDIV introduced in r1423

[Khoo Yit Phang]

Hi,

There seems to be a bug in SBVDIV that was introduced in SVN r1423. The following two CVC queries should be equivalent, but they return different results:

X : BITVECTOR(2);
ASSERT(X = 0b01);
QUERY(NOT(SBVDIV(2,X,0b11) = 0b11));
Valid.

QUERY(NOT(SBVDIV(2,0b01,0b11) = 0b11));
Invalid.

In my testing, it seems to only occur when the left operand is a variable.

Yit
January 4, 2012

[Trevor Hansen]

Hello Yit,

Thanks for the bug report. I've fixed it in revision 1471.

In revision 1423, I introduced the rewrite rule SBVDIV(X,-1) => UMINUS(-1), instead of SBVDIV(X,-1) => UMINUS(X).

Automated testing should have found this, so there is some problem with that too.

Everyone using between 1423 and 1470 (inclusive) should upgrade.

Thanks and sorry for all the trouble.

Trev.

---

From: Khoo Yit Phang <kho...@cs.umd.edu>
To: stp-users <stp-...@googlegroups.com>
Cc: Khoo Yit Phang <kho...@cs.umd.edu>
Sent: Thursday, 5 January 2012 9:01 AM
Subject: Bug in SBVDIV introduced in r1423