2 files changed, 8 insertions, 1 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 9ed2202fe..1434cf6c7 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -28,6 +28,7 @@
 #include "decision/options.h"
 #include "util/lemma_input_channel.h"
 #include "util/lemma_output_channel.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace prop {
@@ -170,11 +171,11 @@ SatLiteral TheoryProxy::getNextReplayDecision() {
     Expr e = options::replayStream()->nextExpr();
     if(!e.isNull()) { // we get null node when out of decisions to replay
       // convert & return
+      ++d_replayedDecisions;
       return d_cnfStream->getLiteral(e);
     }
   }
 #endif /* CVC4_REPLAY */
-  //FIXME!
   return undefSatLiteral;
 }
 
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 96332217e..5fa133122 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -71,6 +71,12 @@ class TheoryProxy {
    */
   std::hash_set<Node, NodeHashFunction> d_shared;
 
+  /**
+   * Statistic: the number of replayed decisions (via --replay).
+   */
+  KEEP_STATISTIC(IntStat, d_replayedDecisions,
+                 "prop::theoryproxy::replayedDecisions", 0);
+
 public:
   TheoryProxy(PropEngine* propEngine,
               TheoryEngine* theoryEngine,