Z3 in infinite loop when using mod with variable divisor

[amigalemming]

This code sends Z3 (4.8.17) to an infinite loop:

import Prelude hiding (even)

{-@
even ::
   n : Integer ->
   {m : Bool | m = (n mod 2 = 0)}
@-}
even :: Integer -> Bool
even n = mod n 2 == 0

{-@
divTwoPow ::
   nn : {n : Integer | n>0} ->
   {m : Integer | m>0 && m mod 2 = 1 && m <= nn && nn mod m = 0}
@-}
divTwoPow :: Integer -> Integer
divTwoPow n =
   if even n then divTwoPow (div n 2) else n

Is this an Z3 issue or an Liquid Haskell issue?

[AlecsFerra]

Can reproduce on develop with z3 4.13.3 - 64 bit, indeed by running z3 manually on the generated .smt file it ends up in an infinite loop, sounds like a z3 bug.

[amigalemming]

Reported here: Z3Prover/z3#7464

I tried to check the SMT file using CVC5. After removing the smt_map definitions, CVC5 can parse the file but also goes to an infinite loop while accepting the SMT file without the modulo condition.

I try to assist Z3 with this manual proof:

{-@ type Positive = {n : Integer | n > 0} @-}
{-@ type OddNatural = {n : Positive | n mod 2 = 1} @-}
type Positive = Integer
type OddNatural = Integer

{-@
theorem ::
  a : {Positive | a mod 2 = 0} ->
  b : {OddNatural | (div a 2) mod b = 0} ->
  {a mod b = 0}
@-}
theorem :: Positive -> OddNatural -> Proof
theorem a b =
   let a2 = div a 2 in
   (mod a2 b == 0)
      === (a2 == div a2 b * b)
      === (a == (2*div a2 b) * b) -- ? (mod a 2 == 0)
      === (mod a b == 0)
      *** QED

Z3 accepts the proof, although it requires more time than I expected.

But when I try to apply the theorem, Z3 goes into an infinite loop, again:

{-@
divTwoPowMod :: n : Positive -> {n mod (divTwoPow n) = 0}
@-}
divTwoPowMod :: Positive -> Proof
divTwoPowMod n =
   case mod n 2 of
      0 -> theorem n (divTwoPow (div n 2)) ? divTwoPowMod (div n 2)
      _ -> mod n n == 0 *** QED

[amigalemming]

It seems that Z3 and CVC5 have not passed the totality check. :-)

[AlecsFerra]

Maybe is not an infinite loop really but is just going to take ages to prove.