From 702d4388cf877dc3eef52205852f5f3b2c18b491 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Magnus=20L=C3=A5ng?= <magnus.lang@it.uu.se>
Date: Tue, 27 Mar 2018 16:02:00 +0200
Subject: [PATCH] TSOTraceBuilder: Record the point of replay

This will allow the is_replaying() predicate to return the right thing,
allowing the non-determinism checking to work with Optimal-DPOR.
---
 src/TSOTraceBuilder.cpp | 4 +++-
 src/TSOTraceBuilder.h   | 5 +++++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/TSOTraceBuilder.cpp b/src/TSOTraceBuilder.cpp
index a1cf962c8..cc1b1d061 100644
--- a/src/TSOTraceBuilder.cpp
+++ b/src/TSOTraceBuilder.cpp
@@ -32,6 +32,7 @@ TSOTraceBuilder::TSOTraceBuilder(const Configuration &conf) : TSOPSOTraceBuilder
   replay = false;
   last_full_memory_conflict = -1;
   last_md = 0;
+  replay_point = 0;
 }
 
 TSOTraceBuilder::~TSOTraceBuilder(){
@@ -161,7 +162,7 @@ void TSOTraceBuilder::mark_unavailable(int proc, int aux){
 }
 
 bool TSOTraceBuilder::is_replaying() const {
-  return replay;
+  return prefix_idx < replay_point;
 }
 
 void TSOTraceBuilder::cancel_replay(){
@@ -232,6 +233,7 @@ bool TSOTraceBuilder::reset(){
     /* No more branching is possible. */
     return false;
   }
+  replay_point = i;
 
   /* Setup the new Event at prefix[i] */
   {
diff --git a/src/TSOTraceBuilder.h b/src/TSOTraceBuilder.h
index 0409f0d6d..1e82c4fe5 100644
--- a/src/TSOTraceBuilder.h
+++ b/src/TSOTraceBuilder.h
@@ -358,6 +358,11 @@ class TSOTraceBuilder : public TSOPSOTraceBuilder{
    */
   bool replay;
 
+  /* The number of events that were or are going to be replayed in the
+   * current computation.
+   */
+  int replay_point;
+
   /* The latest value passed to this->metadata(). */
   const llvm::MDNode *last_md;