Generate witness only for last window

Author: bryanljx

src/common/trace.cpp

@@ -62,18 +62,22 @@ class Trace {
   friend struct TraceHash;
 
   Trace appendEvent(std::vector<Event> &allEvents, EventIndex idx,
-                    std::unordered_map<EventIndex, EventIndex> &po) {
+                    std::unordered_map<EventIndex, EventIndex> &po,
+                    bool isLastWindow) {
     Trace t(*this);
-    t.prevMmap = t.mmap;
-    t.prevEvents = t.events;
+    if (isLastWindow) {
+      t.prevMmap = t.mmap;
+      t.prevEvents = t.events;
+    }
 
     t.events.erase(idx);
 
     if (po.find(idx) != po.end())
       t.events.insert(po[idx]);
 
     Event &event = allEvents[idx];
-    t.curr = event;
+    if (isLastWindow)
+      t.curr = event;
 
     switch (event.getEventType()) {
     case EventType::Acquire:

src/consistency_checker/verify_sc.cpp

@@ -100,7 +100,8 @@ bool verify_sc(std::vector<Event> &allEvents,
       }
 
       for (auto i : reordering.getExecutableEvents(allEvents, goodWrites)) {
-        Trace nextReordering = reordering.appendEvent(allEvents, i, po);
+        Trace nextReordering =
+            reordering.appendEvent(allEvents, i, po, isLastWindow);
         if (seen.find(nextReordering) == seen.end()) {
           stack.push(nextReordering);
           seen.insert(nextReordering);