LEC: the verdict names the miter log this run wrote

src/bin/KeplerFormal.cpp

@@ -2918,7 +2918,8 @@ static int KeplerFormalMainImpl(
         if (equivalent) {
           SPDLOG_INFO("No difference was found.");
         } else {
-          SPDLOG_INFO("Difference was found. Please refer to the log(miter_log_x.txt) for details.");
+          SPDLOG_INFO("Difference was found. Please refer to the log({}) for details.",
+                    KEPLER_FORMAL::MiterStrategy::getActualLogFileName());
           // LCOV_EXCL_STOP
         }
 	      // LCOV_EXCL_START
@@ -3405,10 +3406,11 @@ static int KeplerFormalMainImpl(
         // LCOV_EXCL_START
         } else {
           allScopesEquivalent = false;
-          SPDLOG_INFO("Difference was found for scope: {} , {}. Please refer to the log(miter_log_x.txt) for details.",  // LCOV_EXCL_LINE
+          SPDLOG_INFO("Difference was found for scope: {} , {}. Please refer to the log({}) for details.",  // LCOV_EXCL_LINE
           // LCOV_EXCL_STOP
                       scopes.first->getName().getString(),
-                      scopes.second->getName().getString());
+                      scopes.second->getName().getString(),
+                      KEPLER_FORMAL::MiterStrategy::getActualLogFileName());
         }
       // LCOV_EXCL_START
       } catch (const std::exception& e) {
@@ -3460,7 +3462,8 @@ static int KeplerFormalMainImpl(
       if (equivalent) {
         SPDLOG_INFO("No difference was found.");
       } else {
-        SPDLOG_INFO("Difference was found. Please refer to the log(miter_log_x.txt) for details.");
+        SPDLOG_INFO("Difference was found. Please refer to the log({}) for details.",
+                    KEPLER_FORMAL::MiterStrategy::getActualLogFileName());
         // LCOV_EXCL_STOP
       }
     // LCOV_EXCL_START

test/strategies/miter/MiterTests.cpp

@@ -9,6 +9,7 @@
 #include <filesystem>
 #include <fstream>
 #include <functional>
+#include <regex>
 #include <set>
 #include <sstream>
 #include <string>
@@ -3209,6 +3210,78 @@ static int run_kepler_cli_with_args(const std::vector<std::string>& args) {
 #endif
 }
 
+// A scratch directory per test, and a shell run of kepler-formal in it with
+// stdout and stderr kept: the subprocess form of a CLI test.
+static std::filesystem::path cliScratchDir(const std::string& name) {
+  const auto dir = std::filesystem::temp_directory_path() /
+                   ("kepler_cli_" + name + "_" +
+                    std::to_string(std::chrono::steady_clock::now()
+                                       .time_since_epoch()
+                                       .count()));
+  std::filesystem::create_directories(dir);
+  return dir;
+}
+
+static void writeText(const std::filesystem::path& path, const std::string& text) {
+  std::ofstream out(path);
+  out << text;
+}
+
+static std::string readText(const std::filesystem::path& path) {
+  std::ifstream in(path);
+  std::stringstream text;
+  text << in.rdbuf();
+  return text.str();
+}
+
+// AND2, NAND2 and INV, enough for an equivalent pair the miter cannot hash
+// away: AND2 against NAND2 into INV.
+static const char* kTinyLiberty =
+    "library(tiny) {\n"
+    "  cell(AND2) {\n"
+    "    pin(A) { direction : input; }\n"
+    "    pin(B) { direction : input; }\n"
+    "    pin(Y) { direction : output; function : \"(A&B)\"; }\n"
+    "  }\n"
+    "  cell(NAND2) {\n"
+    "    pin(A) { direction : input; }\n"
+    "    pin(B) { direction : input; }\n"
+    "    pin(Y) { direction : output; function : \"!(A&B)\"; }\n"
+    "  }\n"
+    "  cell(INV) {\n"
+    "    pin(A) { direction : input; }\n"
+    "    pin(Y) { direction : output; function : \"!A\"; }\n"
+    "  }\n"
+    "}\n";
+
+// Runs kepler-formal in `dir`; its output goes to `dir`/kepler.out.
+static int runKeplerIn(const std::filesystem::path& dir,
+                       const std::vector<std::string>& args) {
+  std::string cmd = "cd '" + dir.string() + "' && '" + std::string(KEPLER_BIN) + "'";
+  for (const auto& a : args) {
+    cmd += " '" + a + "'";
+  }
+  cmd += " > kepler.out 2>&1";
+  const int rc = std::system(cmd.c_str());
+  return (rc != -1 && WIFEXITED(rc)) ? WEXITSTATUS(rc) : EXIT_FAILURE;
+}
+
+TEST(KeplerCliSubprocessTests, LecDifferenceNamesTheMiterLogItWrote) {
+  // The verdict points at the miter's log by the name this run gave it.
+  const auto dir = cliScratchDir("lec_log_name");
+  writeText(dir / "same.v", "module top(input a, output y);\n  assign y = a;\nendmodule\n");
+  writeText(dir / "zero.v", "module top(input a, output y);\n  assign y = 1'b0;\nendmodule\n");
+  runKeplerIn(dir, {"-verilog", "same.v", "zero.v"});
+  const auto out = readText(dir / "kepler.out");
+  std::smatch m;
+  ASSERT_TRUE(std::regex_search(
+      out, m, std::regex("Difference was found\\. Please refer to the log\\(([^)]+)\\)")))
+      << out;
+  ASSERT_TRUE(std::filesystem::exists(dir / m[1].str())) << m[1].str();
+  EXPECT_NE(readText(dir / m[1].str()).find("Building miter"), std::string::npos);
+  std::filesystem::remove_all(dir);
+}
+
 TEST(KeplerCliSubprocessTests, BinaryExists) {
   std::filesystem::path p(KEPLER_BIN);
   bool exists = std::filesystem::exists(p);