diff --git a/lib/CryptolTC.z3 b/lib/CryptolTC.z3
index 7d873694..f48923f1 100644
--- a/lib/CryptolTC.z3
+++ b/lib/CryptolTC.z3
@@ -293,15 +293,19 @@
 )
 
 (define-fun cryCeilDiv ((x InfNat) (y InfNat)) InfNat
-  (ite (or (isErr x) (isErr y) (not (isFin x)) (not (isFin y))) cryErr
-  (ite (= (value y) 0) cryErr (cryNat (- (div (- (value x)) (value y)))))
-  )
+  (ite (or (isErr x) (isErr y) (not (isFin y))) cryErr
+  (ite (= (value y) 0) cryErr
+  (ite (not (isFin x)) cryInf
+    (cryNat (- (div (- (value x)) (value y))))
+  )))
 )
 
 (define-fun cryCeilMod ((x InfNat) (y InfNat)) InfNat
-  (ite (or (isErr x) (isErr y) (not (isFin x)) (not (isFin y))) cryErr
-  (ite (= (value y) 0) cryErr (cryNat (mod (- (value x)) (value y))))
-  )
+  (ite (or (isErr x) (isErr y) (not (isFin y))) cryErr
+  (ite (= (value y) 0) cryErr
+  (ite (not (isFin x)) (cryNat 0)
+    (cryNat (mod (- (value x)) (value y)))
+  )))
 )
 
 (define-fun cryLenFromThenTo ((x InfNat) (y InfNat) (z InfNat)) InfNat