[SBV] tests/T41.hs:9:1 Proving "f", using Z3. [Z3] Q.E.D. [SBV] tests/T41.hs:13:1 Proving "g", using Z3. [Z3] Falsifiable. Counter-example: x = -1 :: Int64 y = 0 :: Int64