Fix RNG for seed = 0. (#1459)

The default value for the seed for CVC4's RNG is 0. However, xorshift* requires a non-zero seed, else it generates only zero values. This fixes and prevents this behavior by resetting a given zero seed to ~0.

2 files changed, 4 insertions, 5 deletions

diff --git a/src/util/random.cpp b/src/util/random.cpp
index aca7756ae..d10fb2eec 100644
--- a/src/util/random.cpp
+++ b/src/util/random.cpp
@@ -31,8 +31,7 @@ uint64_t Random::rand()
   d_state ^= d_state >> 12;
   d_state ^= d_state << 25;
   d_state ^= d_state >> 27;
-  d_state *= uint64_t{2685821657736338717};
-  return d_state;
+  return d_state * uint64_t{2685821657736338717};
 }
 
 uint64_t Random::pick(uint64_t from, uint64_t to)
diff --git a/src/util/random.h b/src/util/random.h
index 9083c63e4..1e837642e 100644
--- a/src/util/random.h
+++ b/src/util/random.h
@@ -28,7 +28,7 @@ namespace CVC4 {
 class Random
 {
  public:
-  Random(uint64_t seed) : d_seed(seed), d_state(seed) {}
+  Random(uint64_t seed) { setSeed(seed); }
 
   /* Get current RNG (singleton).  */
   static Random& getRandom()
@@ -40,8 +40,8 @@ class Random
   /* Set seed of Random.  */
   void setSeed(uint64_t seed)
   {
-    d_seed = seed;
-    d_state = seed;
+    d_seed = seed == 0 ? ~seed : seed;
+    d_state = d_seed;
   }
 
   /* Next random uint64_t number. */