bv_decide failure

[leodemoura]

The following example fails, but it should work.

import Std.Tactic.BVDecide

theorem bv_decide_split_if_example (x0 : BitVec 64) :
 BitVec.zeroExtend 32
      (BitVec.zeroExtend 33 (BitVec.zeroExtend 32 x0) +
        (BitVec.zeroExtend 33 (BitVec.replicate 32 (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 x0))) &&&
            0xfffffffe#33 |||
          BitVec.zeroExtend 33 ((BitVec.zeroExtend 32 x0).rotateRight 31) &&& 0xffffffff#33 &&& 0x1#33)) ^^^
    (BitVec.replicate 32 (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 x0)) &&& 0xfffffffe#32 |||
      (BitVec.zeroExtend 32 x0).rotateRight 31 &&& 0xffffffff#32 &&& 0x1#32) =
  if (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 x0) == 0x0#1) = true then BitVec.zeroExtend 32 x0
  else 0x0#32 - BitVec.zeroExtend 32 x0 := by
  bv_decide

Users are forced to manually split the if-then-else. That is, the following one works.

import Std.Tactic.BVDecide

theorem bv_decide_split_if_example (x0 : BitVec 64) :
 BitVec.zeroExtend 32
      (BitVec.zeroExtend 33 (BitVec.zeroExtend 32 x0) +
        (BitVec.zeroExtend 33 (BitVec.replicate 32 (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 x0))) &&&
            0xfffffffe#33 |||
          BitVec.zeroExtend 33 ((BitVec.zeroExtend 32 x0).rotateRight 31) &&& 0xffffffff#33 &&& 0x1#33)) ^^^
    (BitVec.replicate 32 (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 x0)) &&& 0xfffffffe#32 |||
      (BitVec.zeroExtend 32 x0).rotateRight 31 &&& 0xffffffff#32 &&& 0x1#32) =
  if (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 x0) == 0x0#1) = true then BitVec.zeroExtend 32 x0
  else 0x0#32 - BitVec.zeroExtend 32 x0 := by
  split <;> bv_decide

[hargoniX]

Totally forgot about this particular issue, this feature has been implemented a while back.