From a2b36e77bd061ef16e987352163a97ee12e796dd Mon Sep 17 00:00:00 2001
From: Martin Suda <sudam@cs.man.ac.uk>
Date: Tue, 26 Sep 2017 18:26:07 +0200
Subject: [PATCH] szs comments include if relevant

---
 CASC/CASCMode.cpp      |  5 +++++
 CASC/PortfolioMode.cpp | 17 +++++------------
 Shell/UIHelper.cpp     |  6 +++++-
 Shell/UIHelper.hpp     |  2 +-
 4 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/CASC/CASCMode.cpp b/CASC/CASCMode.cpp
index 0f88dfee10..4caa529db5 100644
--- a/CASC/CASCMode.cpp
+++ b/CASC/CASCMode.cpp
@@ -252,6 +252,11 @@ bool CASCMode::runSlice(Options& opt)
   return false;
 }
 
+
+
+
+
+
 /**
  * Do the theorem proving in a forked-off process
  */
diff --git a/CASC/PortfolioMode.cpp b/CASC/PortfolioMode.cpp
index a3a1e54451..505b91affb 100644
--- a/CASC/PortfolioMode.cpp
+++ b/CASC/PortfolioMode.cpp
@@ -182,13 +182,6 @@ static unsigned milliToDeci(unsigned timeInMiliseconds) {
   return timeInMiliseconds/100;
 }
 
-static ostream& lineOutput()
-{
-  CALL("PortfolioMode static lineOutput");
-  addCommentSignForSZS(env.out());
-  return env.out() << "(" << getpid() << ',' << (env.timer->elapsedMilliseconds()/100)/10.0 << ") ";
-}
-
 /**
  * Run a schedule.
  * Return true if a proof was found, otherwise return false.
@@ -238,8 +231,8 @@ bool PortfolioMode::runSchedule(Schedule& schedule, int terminationTime)
 
       /*
       env.beginOutput();
-      lineOutput() << "Slices left: " << slices << endl;
-      lineOutput() << "Processes available: " << processesLeft << endl;
+      addCommentSignForSZS(env.out()) << "Slices left: " << slices << endl;
+      addCommentSignForSZS(env.out()) << "Processes available: " << processesLeft << endl;
       env.endOutput();
       */
 
@@ -287,7 +280,7 @@ bool PortfolioMode::runSchedule(Schedule& schedule, int terminationTime)
 
       if (outputAllowed()) {
         env.beginOutput();
-        lineOutput() << "spawned child "<< childId << " with time: " << sliceTime << " (total remaining time " << remainingTime << ")" << endl;
+        addCommentSignForSZS(env.out()) << "spawned child "<< childId << " with time: " << sliceTime << " (total remaining time " << remainingTime << ")" << endl;
         env.endOutput();
       }
 
@@ -421,7 +414,7 @@ void PortfolioMode::runSlice(Options& strategyOpt)
 
   if (outputAllowed()) {
     env.beginOutput();
-    lineOutput() << opt.testId() << " on " << opt.problemName() << endl;
+    addCommentSignForSZS(env.out()) << opt.testId() << " on " << opt.problemName() << endl;
     env.endOutput();
   }
 
@@ -462,7 +455,7 @@ void PortfolioMode::runSlice(Options& strategyOpt)
     /*
     if (!resultValue) {
       env.beginOutput();
-      lineOutput() << " found a proof after proof output" << endl;
+      addCommentSignForSZS(env.out()) << " found a proof after proof output" << endl;
       env.endOutput();
     }
     */
diff --git a/Shell/UIHelper.cpp b/Shell/UIHelper.cpp
index 93a00bda48..c69cdf1f96 100644
--- a/Shell/UIHelper.cpp
+++ b/Shell/UIHelper.cpp
@@ -101,11 +101,15 @@ bool szsOutputMode() {
   return (Lib::env.options && Lib::env.options->outputMode() == Shell::Options::Output::SZS);
 }
 
-void addCommentSignForSZS(ostream& out)
+ostream& addCommentSignForSZS(ostream& out)
 {
   if (szsOutputMode()) {
     out << "% ";
+    if (Lib::env.options && Lib::env.options->multicore() != 1) {
+      out << "(" << getpid() << ")";
+    }
   }
+  return out;
 }
 
 bool UIHelper::s_haveConjecture=false;
diff --git a/Shell/UIHelper.hpp b/Shell/UIHelper.hpp
index 6cc452e483..8577cb44ff 100644
--- a/Shell/UIHelper.hpp
+++ b/Shell/UIHelper.hpp
@@ -17,7 +17,7 @@ using namespace Lib;
 using namespace Kernel;
 
 bool szsOutputMode();
-void addCommentSignForSZS(ostream&);
+ostream& addCommentSignForSZS(ostream&);
 void reportSpiderFail();
 void reportSpiderStatus(char status);
 bool outputAllowed(bool debug=false);