Address review

src/lib/reasoners/intervals.ml

@@ -632,16 +632,22 @@ module Int = struct
     trace1 "lognot" u @@ map_strict_dec ZEuclideanType.lognot u
 
   let bvudiv ~size:sz u1 u2 =
-    (* [bvudiv] is euclidean division where division by zero is -1 *)
+    (* [bvudiv] is euclidean division where division by zero is -1 (as an
+       integer of width [sz], so 2^sz - 1) *)
     let mone = Z.extract Z.minus_one 0 sz in
     ediv ~div0:(Interval.of_bounds (Closed mone) (Closed mone)) u1 u2
 
   let bvurem u1 u2 =
+    (* In the following, [x] is the implicit variable associated with [u1] and
+       [y] the implicit variable associated with [u2]. *)
     of_set_nonempty @@
     map_to_set (fun i2 ->
         if ZEuclideanType.equal i2.ub ZEuclideanType.zero then
           (* [y] is always zero -> identity *)
           map_to_set interval_set u1
+        else if ZEuclideanType.compare i2.ub ZEuclideanType.zero < 0 then
+          (* Safety check -- bvurem only makes sense if [u2] is nonnegative. *)
+          invalid_arg "bvurem"
         else
           map_to_set (fun i1 ->
               if ZEuclideanType.compare i1.ub i2.lb < 0 then