[SMT-LIB] Bug fix for bvsmod in QF_BV logic

Clark Barrett barrett at cs.nyu.edu
Tue Jun 14 18:23:42 EDT 2011

Previous message: [SMT-LIB] New SMT-LIB release for SMT-COMP 2011 -- (multi-query) application track benchmakrs
Next message: [SMT-LIB] Call for participation: SMT 2011
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

I have updated the definition of bvsmod in the QF_BV logic.  The definition
was incorrect for the case when the divisor is negative and the dividend is
a multiple of the divisor.  Thanks to Bruno Dutertre for finding this bug.

-Clark

Previous message: [SMT-LIB] New SMT-LIB release for SMT-COMP 2011 -- (multi-query) application track benchmakrs
Next message: [SMT-LIB] Call for participation: SMT 2011
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the SMT-LIB mailing list