From d1200cb579d82216d680193c8fdd0146101f77e0 Mon Sep 17 00:00:00 2001
From: Etienne Renault <renault@lrde.epita.fr>
Date: Mon, 16 Jul 2018 07:14:58 +0000
Subject: [PATCH] swarming: bug fix

This is an important bug fix. When swarming
is activated, some multiplication is performed
to find a successor. This multiplication could,
eventually, overflow... Using larger types solves
the problem.

* spot/ltsmin/spins_kripke.hh,
spot/ltsmin/spins_kripke.hxx: here.
---
 spot/ltsmin/spins_kripke.hh  |  3 +++
 spot/ltsmin/spins_kripke.hxx | 11 +++++++++--
 2 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/spot/ltsmin/spins_kripke.hh b/spot/ltsmin/spins_kripke.hh
index c7bbec95e..ea3eec47b 100644
--- a/spot/ltsmin/spins_kripke.hh
+++ b/spot/ltsmin/spins_kripke.hh
@@ -149,6 +149,9 @@ namespace spot
     cube condition() const;
 
   private:
+    /// Compute the real index in the successor vector
+    unsigned compute_index() const;
+
     std::vector<cspins_state> successors_;
     unsigned int current_;
     cube cond_;
diff --git a/spot/ltsmin/spins_kripke.hxx b/spot/ltsmin/spins_kripke.hxx
index 928d767b7..ff6457654 100644
--- a/spot/ltsmin/spins_kripke.hxx
+++ b/spot/ltsmin/spins_kripke.hxx
@@ -203,8 +203,15 @@ namespace spot
   {
     if (SPOT_UNLIKELY(!tid_))
       return successors_[current_];
-    return  successors_[(((current_+1)*primes[tid_])
-                         % ((int)successors_.size()))];
+    return   successors_[compute_index()];
+  }
+
+  unsigned cspins_iterator::compute_index() const
+  {
+    unsigned long long c = current_ + 1;
+    unsigned long long p = primes[tid_];
+    unsigned long long s = successors_.size();
+    return (unsigned)  ((c*p) % s);
   }
 
   cube cspins_iterator::condition() const