diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs index b1bc4ee6..9726767d 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs @@ -125,18 +125,18 @@ propInterval varInts prop = catMaybes -- k >= width x , do (l,r) <- pIsGeq prop x <- tIsVar =<< pIsWidth r - let int = typeInterval varInts l - -- record the exact upper bound when it produces values within 128 -- bits - ub = case iUpper int of + let ub = case iIsExact (typeInterval varInts l) of Just (Nat val) | val < 128 -> Just (Nat (2 ^ val - 1)) | otherwise -> Nothing - _ -> iUpper int + upper -> upper return (x, Interval { iLower = Nat 0, iUpper = ub }) + ] + -------------------------------------------------------------------------------- data Interval = Interval