uuverifiers
Incorrect handling of bitvector division by zero in epsilon logic (regression in commit 8311b03)
Bitvector division by zero mishandled due to epsilon logic regression in commit 8311b03a6a599242ecd8b567fc958482b508f8b6.
In this commit, the handling of epsilon terms in EPSSearcher2 changed in a way that causes incorrect results for certain bitvector formulas. Specifically, complex epsilon expressions like:
εx. (x \* b ≤ a ∧ x \* b > a - b)
are replaced with constants, which loses semantic information needed to reason correctly about operations like division by zero.
This affects both Princess and some Ostrich versions that include affected Princess builds.
Input SMT-LIB (bug.smt2):
(declare-const BITVEC64_VAR_a (_ BitVec 64)) ( assert ( bvult #x0000000000000000 ( bvand #x1111111111111111 ( bvudiv #x0000000000000000 BITVEC64_VAR_a ) ) ) ) ( check-sat )
Expected output: sat
Actual output (Princess b3e83e1): unsat
Other solvers (e.g., cvc5): sat
Princess generates contradictory constraints like _0 = 0 and _0 = 18446744073709551615, making the formula unsatisfiable when it should be satisfiable.
This may be related to changes around line 222 in src/ap/parser/EquivExpander.scala, though this might not be the exact location.
Thank you for the bug report! This was indeed a problem with the expansion of epsilon expressions that should now be fixed.
