bug in wrap around computation corrected

src/Smv.ml

@@ -124,13 +124,13 @@ module Make_SMV_LTL (At : Solver.ATOMIC_PROPOSITION) :
       | Neq -> "!="
 
   (* Generates an SMV signed word consisting of *length_0* 0 on the left and *bw - length_0* 0 after.*)
-  let generate_mask length_0 bw =
+  (*let generate_mask length_0 bw =
     let beg_mask = List.init length_0 (fun _ -> 0) in
     let end_mask = List.init (bw - length_0) (fun _ -> 1) in
     let mask_list = List.append beg_mask end_mask in
     let prefix =  "0sb" ^ (string_of_int bw) ^ "_" in
     prefix ^ (List.fold_left (fun s i -> s ^ (string_of_int i) ) "" mask_list)
-
+  *)
 
     (* From NuXmv documentation, from high to low (excerpt, some precedences are ignored because they are not used)
 

src/Solver.ml

@@ -17,19 +17,20 @@ open Containers
 [@@@warning "-4"]
 [@@@warning "-32"]
 
+
+(* Computes the value of n according to the wrap around semantics *)
+(* the result is betwwen -(2 ^ (bw-1)) and (2 ^ (bw-1) - 1) *)
 let wrap bw n =
   if bw <= 0 then n
   else
     (* maxint = 2 ^ (bw - 1) => wraps at *this* number *)
-    let maxint = Int.(pow 2 (bw - 1)) in
+    let maxint = Int.pow 2 (bw - 1)  in
     let interval_length = 2 * maxint in
     if n >= maxint then ((n + maxint) mod interval_length) - maxint
     else if n < ~-maxint then
-      ((n + maxint) mod interval_length) + interval_length
+      ((n - maxint + 1) mod interval_length) + maxint -1
     else n
 
-let%test _ = wrap 1 0 = 3
-
 (* fragile patterns, lots of them as we short-circuit *)
 
 module type ATOMIC_PROPOSITION = sig