From 73ee2dea656c76513d74300569e06a8cd92fde1e Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sat, 29 Nov 2025 18:15:00 +0100
Subject: [PATCH 01/43] yaml support

---
 CMakeLists.txt           |   4 +
 example/test_config.yaml |  11 ++
 src/bin/KeplerFormal.cpp | 233 ++++++++++++++++++++++++++++-----------
 3 files changed, 186 insertions(+), 62 deletions(-)
 create mode 100644 example/test_config.yaml

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 68dbc8f2..61d4a51b 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -27,6 +27,8 @@ include(CTest)
 add_subdirectory(test)
 
 find_package(TBB REQUIRED)
+find_package(yaml-cpp REQUIRED)
+find_package(spdlog REQUIRED)
 
 # if you’re using find_package(TBB), ensure it picked up Homebrew’s install
 
@@ -37,4 +39,6 @@ target_include_directories(formal_structures
 )
 target_link_libraries(formal_structures
   PRIVATE TBB::tbb
+  yaml-cpp::yaml-cpp
+  spdlog::spdlog
 )
diff --git a/example/test_config.yaml b/example/test_config.yaml
new file mode 100644
index 00000000..ba6e8fb5
--- /dev/null
+++ b/example/test_config.yaml
@@ -0,0 +1,11 @@
+# tinyrocket_config.yaml
+format: naja_if
+input_paths:
+  - tinyrocket_naja.if
+  - tinyrocket_naja_edited.if
+liberty_files:
+  - NangateOpenCellLibrary_typical.lib
+  - fakeram45_1024x32.lib
+  - fakeram45_64x32.lib
+log_level: info
+
diff --git a/src/bin/KeplerFormal.cpp b/src/bin/KeplerFormal.cpp
index a870b4c1..42e03dcd 100644
--- a/src/bin/KeplerFormal.cpp
+++ b/src/bin/KeplerFormal.cpp
@@ -5,8 +5,14 @@
 #include <cstdlib>
 #include <string>
 #include <vector>
+#include <iostream>
+#include <optional>
 
 #include <spdlog/spdlog.h>
+#include <spdlog/sinks/stdout_color_sinks.h>
+
+#include <yaml-cpp/yaml.h>
+
 #include "NajaPerf.h"
 
 // Naja interfaces
@@ -18,130 +24,235 @@
 #include "SNLVRLDumper.h"
 #include "SNLUtils.h"
 
+static void print_usage(const char* prog) {
+  std::printf(
+      "Usage: %s [--config <file>] | <-naja_if/-verilog> <netlist1> <netlist2> "
+      "[<liberty-file>...]\n",
+      prog);
+}
+
+static std::vector<std::string> yamlToVector(const YAML::Node& node) {
+  std::vector<std::string> out;
+  if (!node) return out;
+  if (!node.IsSequence()) return out;
+  for (const auto& n : node) {
+    if (n.IsScalar()) out.emplace_back(n.as<std::string>());
+  }
+  return out;
+}
+
 int main(int argc, char** argv) {
   using namespace std::chrono;
   enum class FormatType { VERILOG, SNL };
 
+  // Default values
   FormatType inputFormatType = FormatType::VERILOG;
+  std::vector<std::string> inputPaths;
+  std::vector<std::string> libertyFiles;
+  std::string logLevel = "info";
 
-  // Help print when --help or -h is provided
-  if (argc < 3 || (std::string(argv[1]) == "--help") ||
-      (std::string(argv[1]) == "-h")) {
-    printf(
-        "Usage: kepler_formal <-naja_if/-verilog> <netlist1> <netlist2> "
-        "[<liberty-file>...]\n");
+  // Basic argument sanity
+  if (argc < 2) {
+    print_usage(argv[0]);
     return EXIT_SUCCESS;
   }
 
-  // --------------------------------------------------------------------------
-  // 1. Parse command‐line arguments into inputPaths (requires exactly 2 paths)
-  // --------------------------------------------------------------------------
-  // if (argc != 3) {
-  //   SPDLOG_CRITICAL("Usage: {} <naja-if-dir-1> <naja-if-dir-2>", argv[0]);
-  //   return EXIT_FAILURE;
-  // }
-  printf("KEPLER FORMAL: Run.\n");
-
-  size_t inputPathsIndex = 2;
-  size_t inputLibraryIndex = 4;
-
-  std::string formatType = argv[1];
-
-  if (formatType == "-naja_if") {
-    inputFormatType = FormatType::SNL;
-  } else if (formatType == "-verilog") {
-    inputFormatType = FormatType::VERILOG;
-  } else {
-    SPDLOG_CRITICAL("Unrecognized input format type: {}", formatType);
+  // Check for config mode (--config or -c). If present, YAML takes precedence.
+  bool usedConfig = false;
+  for (int i = 1; i < argc; ++i) {
+    std::string a = argv[i];
+    if (a == "--config" || a == "-c") {
+      if (i + 1 >= argc) {
+        SPDLOG_CRITICAL("Missing config file after {}", a);
+        return EXIT_FAILURE;
+      }
+      const std::string cfgPath = argv[i + 1];
+      try {
+        YAML::Node cfg = YAML::LoadFile(cfgPath);
+
+        // format
+        if (cfg["format"] && cfg["format"].IsScalar()) {
+          std::string fmt = cfg["format"].as<std::string>();
+          if (fmt == "naja_if" || fmt == "naja-if" || fmt == "snl")
+            inputFormatType = FormatType::SNL;
+          else if (fmt == "verilog" || fmt == "v")
+            inputFormatType = FormatType::VERILOG;
+          else {
+            SPDLOG_CRITICAL("Unrecognized format in config: {}", fmt);
+            return EXIT_FAILURE;
+          }
+        }
+
+        // input_paths
+        inputPaths = yamlToVector(cfg["input_paths"]);
+
+        // liberty_files
+        libertyFiles = yamlToVector(cfg["liberty_files"]);
+
+        // log level
+        if (cfg["log_level"] && cfg["log_level"].IsScalar()) {
+          logLevel = cfg["log_level"].as<std::string>();
+        }
+
+        usedConfig = true;
+      } catch (const std::exception& e) {
+        SPDLOG_CRITICAL("Failed to parse config {}: {}", cfgPath, e.what());
+        return EXIT_FAILURE;
+      }
+      break;
+    }
+  }
+
+  // If not using config, fall back to original CLI parsing
+  if (!usedConfig) {
+    if (argc < 4 || (std::string(argv[1]) == "--help") ||
+        (std::string(argv[1]) == "-h")) {
+      print_usage(argv[0]);
+      return EXIT_SUCCESS;
+    }
+
+    std::string formatType = argv[1];
+    if (formatType == "-naja_if" || formatType == "-naja-if") {
+      inputFormatType = FormatType::SNL;
+    } else if (formatType == "-verilog") {
+      inputFormatType = FormatType::VERILOG;
+    } else {
+      SPDLOG_CRITICAL("Unrecognized input format type: {}", formatType);
+      return EXIT_FAILURE;
+    }
+
+    // collect paths and liberty files from argv
+    for (int i = 2; i < argc; ++i) inputPaths.emplace_back(argv[i]);
+
+    // If user provided more than two paths, treat the rest as liberty files
+    if (inputPaths.size() > 2) {
+      for (size_t i = 2; i < inputPaths.size(); ++i)
+        libertyFiles.push_back(inputPaths[i]);
+    }
+  }
+
+  // Basic validation
+  if (inputPaths.size() < 2) {
+    SPDLOG_CRITICAL("Need two input netlist paths; got {}", inputPaths.size());
+    print_usage(argv[0]);
     return EXIT_FAILURE;
   }
 
-  std::vector<std::string> inputPaths;
-  for (int i = inputPathsIndex; i < argc; ++i) {
-    inputPaths.emplace_back(argv[i]);
+  // Configure logging level
+  auto console = spdlog::stdout_color_mt("console");
+  if (logLevel == "debug")
+    spdlog::set_level(spdlog::level::debug);
+  else if (logLevel == "info")
+    spdlog::set_level(spdlog::level::info);
+  else if (logLevel == "warn")
+    spdlog::set_level(spdlog::level::warn);
+  else if (logLevel == "error")
+    spdlog::set_level(spdlog::level::err);
+  else if (logLevel == "critical")
+    spdlog::set_level(spdlog::level::critical);
+  else
+    spdlog::set_level(spdlog::level::info);
+
+  std::printf("KEPLER FORMAL: Run.\n");
+  std::printf("Input format: %s\n", (inputFormatType == FormatType::SNL) ? "SNL" : "VERILOG");
+  std::printf("Netlist 1: %s\n", inputPaths[0].c_str());
+  std::printf("Netlist 2: %s\n", inputPaths[1].c_str());
+  if (!libertyFiles.empty()) {
+    for (const auto& lf : libertyFiles) std::printf("Liberty: %s\n", lf.c_str());
   }
-  printf("number of library files: %zu\n", inputPaths.size() - 2);
 
   // --------------------------------------------------------------------------
-  // 2. Load two netlists via Cap’n Proto
+  // 2. Load two netlists via Cap’n Proto (or via VRL constructor)
   // --------------------------------------------------------------------------
-  // naja::NajaPerf::Scope scope("Parsing SNL format");
-  // const auto t0 = steady_clock::now();
-  // Load liberty
   NLUniverse::create();
   NLDB* db0 = nullptr;
   bool primitivesAreLoaded = false;
-  if (inputPaths.size() > 2) {
+
+  if (!libertyFiles.empty()) {
     db0 = NLDB::create(NLUniverse::get());
     auto primitivesLibrary =
         NLLibrary::create(db0, NLLibrary::Type::Primitives, NLName("PRIMS"));
     SNLLibertyConstructor constructor(primitivesLibrary);
-    for (size_t i = inputLibraryIndex; i < argc; ++i) {
-      printf("Loading liberty file: %s\n", argv[i]);
-      constructor.construct(argv[i]);
+    for (const auto& lf : libertyFiles) {
+      std::printf("Loading liberty file: %s\n", lf.c_str());
+      constructor.construct(lf.c_str());
     }
     primitivesAreLoaded = true;
   }
+
   if (inputFormatType == FormatType::VERILOG) {
     auto designLibrary = NLLibrary::create(db0, NLName("DESIGN"));
     SNLVRLConstructor constructor(designLibrary);
-    constructor.construct(argv[inputPathsIndex]);
+    constructor.construct(inputPaths[0].c_str());
     auto top = SNLUtils::findTop(designLibrary);
     if (top) {
       db0->setTopDesign(top);
-      SPDLOG_INFO("Found top design: " + top->getString());
+      SPDLOG_INFO("Found top design: {}", top->getString());
     } else {
       SPDLOG_ERROR("No top design was found after parsing verilog");
     }
-  } else if (inputFormatType == FormatType::SNL) {
-    printf("Loading SNL file: %s\n", argv[inputPathsIndex]);
-    db0 = SNLCapnP::load(argv[inputPathsIndex], primitivesAreLoaded);
-  } else {
-    SPDLOG_CRITICAL("Unrecognized input format type: {}", formatType);
-    return EXIT_FAILURE;
+  } else {  // SNL
+    std::printf("Loading SNL file: %s\n", inputPaths[0].c_str());
+    db0 = SNLCapnP::load(inputPaths[0].c_str(), primitivesAreLoaded);
+    if (!db0) {
+      SPDLOG_CRITICAL("Failed to load SNL file: {}", inputPaths[0]);
+      return EXIT_FAILURE;
+    }
   }
 
   // get db0 top
   auto top0 = db0->getTopDesign();
+  if (!top0) {
+    SPDLOG_CRITICAL("Top design not set for first netlist");
+    return EXIT_FAILURE;
+  }
   db0->setID(2);  // Increment ID to avoid conflicts
+
   NLDB* db1 = nullptr;
 
-  // Increment ID to avoid conflicts
-  if (inputPaths.size() > 2) {
+  // Prepare second DB and primitives if needed
+  if (!libertyFiles.empty()) {
     db1 = NLDB::create(NLUniverse::get());
     db1->setID(1);
     auto primitivesLibrary =
         NLLibrary::create(db1, NLLibrary::Type::Primitives, NLName("PRIMS"));
     SNLLibertyConstructor constructor(primitivesLibrary);
-    for (size_t i = inputLibraryIndex; i < argc; ++i) {
-      constructor.construct(argv[i]);
+    for (const auto& lf : libertyFiles) {
+      constructor.construct(lf.c_str());
     }
   }
+
   if (inputFormatType == FormatType::VERILOG) {
     auto designLibrary = NLLibrary::create(db1, NLName("DESIGN"));
     SNLVRLConstructor constructor(designLibrary);
-    constructor.construct(argv[inputPathsIndex + 1]);
+    constructor.construct(inputPaths[1].c_str());
     auto top = SNLUtils::findTop(designLibrary);
     if (top) {
       db1->setTopDesign(top);
-      SPDLOG_INFO("Found top design: " + top->getString());
+      SPDLOG_INFO("Found top design: {}", top->getString());
     } else {
       SPDLOG_ERROR("No top design was found after parsing verilog");
     }
-  } else if (inputFormatType == FormatType::SNL) {
-    printf("Loading SNL file: %s\n", argv[inputPathsIndex + 1]);
-    db1 = SNLCapnP::load(argv[inputPathsIndex + 1], primitivesAreLoaded);
-  } else {
-    SPDLOG_CRITICAL("Unrecognized input format type: {}", formatType);
-    return EXIT_FAILURE;
+  } else {  // SNL
+    std::printf("Loading SNL file: %s\n", inputPaths[1].c_str());
+    db1 = SNLCapnP::load(inputPaths[1].c_str(), primitivesAreLoaded);
+    if (!db1) {
+      SPDLOG_CRITICAL("Failed to load SNL file: {}", inputPaths[1]);
+      return EXIT_FAILURE;
+    }
   }
+
   // get db1 top
   auto top1 = db1->getTopDesign();
+  if (!top1) {
+    SPDLOG_CRITICAL("Top design not set for second netlist");
+    return EXIT_FAILURE;
+  }
 
   // --------------------------------------------------------------------------
   // 4. Hand off to the rest of the editing/analysis workflow
   // --------------------------------------------------------------------------
-  /*try {
+  try {
     KEPLER_FORMAL::MiterStrategy MiterS(top0, top1);
     if (MiterS.run()) {
       SPDLOG_INFO("Miter strategy succeeded: outputs are identical.");
@@ -151,9 +262,7 @@ int main(int argc, char** argv) {
   } catch (const std::exception& e) {
     SPDLOG_ERROR("Workflow failed: {}", e.what());
     return EXIT_FAILURE;
-  }*/
-  KEPLER_FORMAL::MiterStrategy MiterS(top0, top1);
-  MiterS.run();
+  }
 
   return EXIT_SUCCESS;
 }

From 8ba52c3c88abf10af433bb00ada276a43f74e1fd Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sat, 29 Nov 2025 18:16:07 +0100
Subject: [PATCH 02/43] update testing

---
 .github/workflows/regress.yml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index 0fd5e7df..93800149 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -51,12 +51,7 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal -naja_if \
-          ./example/tinyrocket_naja.if \
-          ./example/tinyrocket_naja.if \
-          ./example/NangateOpenCellLibrary_typical.lib \
-          ./example/fakeram45_1024x32.lib \
-          ./example/fakeram45_64x32.lib 
+        ./build/src/bin/kepler_formal ./test_config.yaml
     
     - name: Run on verilog
       working-directory: ${{github.workspace}}

From 5d3d95797a3e643f6c549c41efa86b1736c6dc88 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sat, 29 Nov 2025 18:16:38 +0100
Subject: [PATCH 03/43] update testing

---
 .github/workflows/regress.yml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index 93800149..ed7d2d98 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -51,7 +51,12 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal ./test_config.yaml
+        ./build/src/bin/kepler_formal -naja_if \
+          ./example/tinyrocket_naja.if \
+          ./example/tinyrocket_naja.if \
+          ./example/NangateOpenCellLibrary_typical.lib \
+          ./example/fakeram45_1024x32.lib \
+          ./example/fakeram45_64x32.lib 
     
     - name: Run on verilog
       working-directory: ${{github.workspace}}
@@ -77,12 +82,7 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal -naja_if \
-          ./example/tinyrocket_naja.if \
-          ./example/tinyrocket_naja_edited.if \
-          ./example/NangateOpenCellLibrary_typical.lib \
-          ./example/fakeram45_1024x32.lib \
-          ./example/fakeram45_64x32.lib 
+        ./build/src/bin/kepler_formal ./test_config.yaml
     
     - name: Run on verilog edited
       working-directory: ${{github.workspace}}

From b3fcd18f4365ddf3ae57b2b4256d89fbe5e5827d Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sat, 29 Nov 2025 18:26:22 +0100
Subject: [PATCH 04/43] yaml dep

---
 .github/workflows/c-cpp.yml   | 2 +-
 .github/workflows/macOS.yml   | 2 +-
 .github/workflows/regress.yml | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml
index 4ff4a098..27952288 100644
--- a/.github/workflows/c-cpp.yml
+++ b/.github/workflows/c-cpp.yml
@@ -29,7 +29,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -yq libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
+      run: sudo apt-get update && sudo apt-get install -yq libyaml-cpp-dev libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
       
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
diff --git a/.github/workflows/macOS.yml b/.github/workflows/macOS.yml
index 78c2887f..c4cdcff8 100644
--- a/.github/workflows/macOS.yml
+++ b/.github/workflows/macOS.yml
@@ -27,7 +27,7 @@ jobs:
       run: git submodule update --init --recursive
     # install dependencies
     - name: Install dependencies
-      run: brew install cmake doxygen capnp tbb bison flex boost
+      run: brew install cmake doxygen capnp tbb bison flex boost libyaml-cpp-dev
     - name: set env variable
       run: |
         echo "/usr/local/opt/flex/bin" >> $GITHUB_PATH; echo "/usr/local/opt/bison/bin" >> $GITHUB_PATH;
diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index ed7d2d98..1dd1800e 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -30,7 +30,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -yq libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
+      run: sudo apt-get update && sudo apt-get install -yq libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp-dev
       
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20

From f27fe6e30f11d9eb2eedec40b4e4111b14e06eb9 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sat, 29 Nov 2025 18:41:26 +0100
Subject: [PATCH 05/43] spdlog dep

---
 .github/workflows/c-cpp.yml   | 2 +-
 .github/workflows/macOS.yml   | 2 +-
 .github/workflows/regress.yml | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml
index 27952288..e37195a4 100644
--- a/.github/workflows/c-cpp.yml
+++ b/.github/workflows/c-cpp.yml
@@ -29,7 +29,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -yq libyaml-cpp-dev libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
+      run: sudo apt-get update && sudo apt-get install -yq libspdlog-dev libyaml-cpp-dev libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
       
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
diff --git a/.github/workflows/macOS.yml b/.github/workflows/macOS.yml
index c4cdcff8..82113e35 100644
--- a/.github/workflows/macOS.yml
+++ b/.github/workflows/macOS.yml
@@ -27,7 +27,7 @@ jobs:
       run: git submodule update --init --recursive
     # install dependencies
     - name: Install dependencies
-      run: brew install cmake doxygen capnp tbb bison flex boost libyaml-cpp-dev
+      run: brew install cmake doxygen capnp tbb bison flex boost libyaml-cpp-dev libspdlog-dev
     - name: set env variable
       run: |
         echo "/usr/local/opt/flex/bin" >> $GITHUB_PATH; echo "/usr/local/opt/bison/bin" >> $GITHUB_PATH;
diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index 1dd1800e..02bc784d 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -30,7 +30,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -yq libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp-dev
+      run: sudo apt-get update && sudo apt-get install -yq libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp-dev libspdlog-dev
       
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20

From 12c5291ccefae4ec357f51e0f18d974f2f83693c Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sat, 29 Nov 2025 21:27:24 +0100
Subject: [PATCH 06/43] fix

---
 .github/workflows/regress.yml | 2 +-
 CMakeLists.txt                | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index 02bc784d..fb148e3f 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -30,7 +30,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -yq libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp-dev libspdlog-dev
+      run: sudo apt-get update && sudo apt-get install -yq libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp-dev libspdlog-dev 
       
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 61d4a51b..40779bc3 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -21,15 +21,15 @@ set(ARGPARSE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/naja/thirdparty/argparse
 
 set(CMAKE_CXX_STANDARD 20 CACHE STRING "C++ standard" FORCE)
 
+find_package(TBB REQUIRED)
+find_package(yaml-cpp REQUIRED)
+find_package(spdlog REQUIRED)
+
 add_subdirectory(src)
 add_subdirectory(thirdparty)
 include(CTest)
 add_subdirectory(test)
 
-find_package(TBB REQUIRED)
-find_package(yaml-cpp REQUIRED)
-find_package(spdlog REQUIRED)
-
 # if you’re using find_package(TBB), ensure it picked up Homebrew’s install
 
 target_include_directories(formal_structures

From 7b09ff17ed22730d48fa4781a7d7b37caeca7512 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sat, 29 Nov 2025 22:11:49 +0100
Subject: [PATCH 07/43] fix

---
 .github/workflows/macOS.yml | 2 +-
 CMakeLists.txt              | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/macOS.yml b/.github/workflows/macOS.yml
index 82113e35..f79d4d34 100644
--- a/.github/workflows/macOS.yml
+++ b/.github/workflows/macOS.yml
@@ -27,7 +27,7 @@ jobs:
       run: git submodule update --init --recursive
     # install dependencies
     - name: Install dependencies
-      run: brew install cmake doxygen capnp tbb bison flex boost libyaml-cpp-dev libspdlog-dev
+      run: brew install cmake doxygen capnp tbb bison flex boost yaml-cpp spdlog
     - name: set env variable
       run: |
         echo "/usr/local/opt/flex/bin" >> $GITHUB_PATH; echo "/usr/local/opt/bison/bin" >> $GITHUB_PATH;
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 40779bc3..ac694e05 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -37,6 +37,7 @@ target_include_directories(formal_structures
     ${TBB_INCLUDE_DIRS}          # if defined by find_package
     /opt/homebrew/include        # fallback for tbb headers
 )
+
 target_link_libraries(formal_structures
   PRIVATE TBB::tbb
   yaml-cpp::yaml-cpp

From cf00ac0886e0698a7c054ccf2c592c8d35ac4cde Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sat, 29 Nov 2025 22:21:00 +0100
Subject: [PATCH 08/43] fix

---
 .github/workflows/c-cpp.yml   | 2 +-
 .github/workflows/regress.yml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml
index e37195a4..76dac385 100644
--- a/.github/workflows/c-cpp.yml
+++ b/.github/workflows/c-cpp.yml
@@ -29,7 +29,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -yq libspdlog-dev libyaml-cpp-dev libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
+      run: sudo apt-get update && sudo apt-get install -yq pkg-config libspdlog-dev libyaml-cpp-dev libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
       
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index fb148e3f..15a7bf99 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -30,7 +30,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -yq libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp-dev libspdlog-dev 
+      run: sudo apt-get update && sudo apt-get install -yq pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp-dev libspdlog-dev 
       
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20

From 94c2e7f62b837cc2b14476176a458e6410332cf6 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sat, 29 Nov 2025 22:33:50 +0100
Subject: [PATCH 09/43] fix

---
 CMakeLists.txt | 109 ++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 94 insertions(+), 15 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index ac694e05..6bff3340 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -17,29 +17,108 @@ project(kepler-formal
   HOMEPAGE_URL https://github.com/keplertech/kepler-formal
 )
 
+# Option to enable/disable the Python interface. CI disables it by default.
+option(PYTHON_INTERFACE "Enable Python interface" OFF)
+
+# If the python interface is disabled, provide a no-op INTERFACE target so
+# other targets that unconditionally link PYTHON_INTERFACE still configure.
+# This must be created before add_subdirectory(...) so subprojects can link to it.
+if(NOT PYTHON_INTERFACE AND NOT TARGET PYTHON_INTERFACE)
+  add_library(PYTHON_INTERFACE INTERFACE)
+endif()
+
 set(ARGPARSE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/naja/thirdparty/argparse-3.1/include)
 
 set(CMAKE_CXX_STANDARD 20 CACHE STRING "C++ standard" FORCE)
 
-find_package(TBB REQUIRED)
-find_package(yaml-cpp REQUIRED)
-find_package(spdlog REQUIRED)
+# Find packages early so we can create compatibility imported targets if needed.
+find_package(TBB QUIET)
+find_package(yaml-cpp QUIET)
+find_package(spdlog QUIET)
+
+# If find_package didn't create modern imported targets but did set legacy variables,
+# create lightweight imported targets for consistent usage below.
+# yaml-cpp compatibility
+if(NOT TARGET yaml-cpp::yaml-cpp)
+  if(yaml-cpp_FOUND)
+    # If module-mode provided YAML_CPP_LIBRARIES / INCLUDE dirs, create an imported target
+    add_library(yaml-cpp::yaml-cpp UNKNOWN IMPORTED)
+    if(DEFINED YAML_CPP_LIBRARIES)
+      set_target_properties(yaml-cpp::yaml-cpp PROPERTIES
+        IMPORTED_LOCATION "${YAML_CPP_LIBRARIES}")
+    elseif(DEFINED yaml-cpp_LIBRARIES)
+      set_target_properties(yaml-cpp::yaml-cpp PROPERTIES
+        IMPORTED_LOCATION "${yaml-cpp_LIBRARIES}")
+    endif()
+    if(DEFINED YAML_CPP_INCLUDE_DIR)
+      set_property(TARGET yaml-cpp::yaml-cpp PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${YAML_CPP_INCLUDE_DIR}")
+    elseif(DEFINED yaml-cpp_INCLUDE_DIRS)
+      set_property(TARGET yaml-cpp::yaml-cpp PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${yaml-cpp_INCLUDE_DIRS}")
+    endif()
+  else()
+    message(STATUS "yaml-cpp not found via quiet search; will fallback to REQUIRED search momentarily")
+  endif()
+endif()
+
+# spdlog compatibility
+if(NOT TARGET spdlog::spdlog)
+  if(spdlog_FOUND)
+    add_library(spdlog::spdlog UNKNOWN IMPORTED)
+    if(DEFINED spdlog_LIBRARIES)
+      set_target_properties(spdlog::spdlog PROPERTIES IMPORTED_LOCATION "${spdlog_LIBRARIES}")
+    endif()
+    if(DEFINED spdlog_INCLUDE_DIRS)
+      set_property(TARGET spdlog::spdlog PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${spdlog_INCLUDE_DIRS}")
+    endif()
+  endif()
+endif()
+
+# TBB compatibility (libtbb usually provides target TBB::tbb; provide fallback)
+if(NOT TARGET TBB::tbb)
+  if(TBB_FOUND AND DEFINED TBB_LIBRARY)
+    add_library(TBB::tbb UNKNOWN IMPORTED)
+    set_target_properties(TBB::tbb PROPERTIES IMPORTED_LOCATION "${TBB_LIBRARY}")
+    if(DEFINED TBB_INCLUDE_DIRS)
+      set_property(TARGET TBB::tbb PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${TBB_INCLUDE_DIRS}")
+    endif()
+  endif()
+endif()
 
+# If any package is required by your project policy, explicitly require them now.
+# Using REQUIRED to cause clear configure failure if not present.
+if(NOT TARGET yaml-cpp::yaml-cpp)
+  find_package(yaml-cpp REQUIRED)  # will error if missing
+endif()
+if(NOT TARGET spdlog::spdlog)
+  find_package(spdlog REQUIRED)
+endif()
+if(NOT TARGET TBB::tbb)
+  find_package(TBB REQUIRED)
+endif()
+
+# Add project subdirectories (these define formal_structures and others).
 add_subdirectory(src)
 add_subdirectory(thirdparty)
 include(CTest)
 add_subdirectory(test)
 
-# if you’re using find_package(TBB), ensure it picked up Homebrew’s install
-
-target_include_directories(formal_structures
-  PRIVATE
-    ${TBB_INCLUDE_DIRS}          # if defined by find_package
-    /opt/homebrew/include        # fallback for tbb headers
-)
+# Now, only set include_directories / link libraries if the formal_structures
+# target exists. This avoids ordering issues.
+if(TARGET formal_structures)
+  # Include TBB headers (TBB::tbb provides interface dirs; keep fallback path for macOS Homebrew)
+  target_include_directories(formal_structures
+    PRIVATE
+      $<$<TARGET_EXISTS:TBB::tbb>:$<TARGET_PROPERTY:TBB::tbb,INTERFACE_INCLUDE_DIRECTORIES>>
+      /opt/homebrew/include
+  )
 
-target_link_libraries(formal_structures
-  PRIVATE TBB::tbb
-  yaml-cpp::yaml-cpp
-  spdlog::spdlog
-)
+  # Link to available targets in a guarded way.
+  target_link_libraries(formal_structures
+    PRIVATE
+      $<$<TARGET_EXISTS:TBB::tbb>:TBB::tbb>
+      $<$<TARGET_EXISTS:yaml-cpp::yaml-cpp>:yaml-cpp::yaml-cpp>
+      $<$<TARGET_EXISTS:spdlog::spdlog>:spdlog::spdlog>
+  )
+else()
+  message(WARNING "formal_structures target was not defined by subdirectories; skipping top-level link/include setup.")
+endif()
\ No newline at end of file

From daf836605e4b6357e10cf8a8086c638e4b22984b Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sat, 29 Nov 2025 22:39:24 +0100
Subject: [PATCH 10/43] fix

---
 src/bin/CMakeLists.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/bin/CMakeLists.txt b/src/bin/CMakeLists.txt
index 8f666b78..92c91783 100644
--- a/src/bin/CMakeLists.txt
+++ b/src/bin/CMakeLists.txt
@@ -6,5 +6,5 @@ target_include_directories(kepler_formal SYSTEM BEFORE PUBLIC ${Boost_INCLUDE_DI
 target_include_directories(kepler_formal PUBLIC ${ARGPARSE_DIR})
 target_link_libraries(kepler_formal
     naja_snl_pyloader
-    naja_dnl naja_opt formal_strategies)
+    naja_dnl naja_opt formal_strategies yaml-cpp::yaml-cpp spdlog::spdlog)
 install(TARGETS kepler_formal DESTINATION ${CMAKE_INSTALL_BINDIR})

From 611bca80a44814f397241b6fc6e22430c45eb83d Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sat, 29 Nov 2025 23:01:49 +0100
Subject: [PATCH 11/43] fix

---
 src/bin/CMakeLists.txt | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/bin/CMakeLists.txt b/src/bin/CMakeLists.txt
index 92c91783..15516e3a 100644
--- a/src/bin/CMakeLists.txt
+++ b/src/bin/CMakeLists.txt
@@ -6,5 +6,6 @@ target_include_directories(kepler_formal SYSTEM BEFORE PUBLIC ${Boost_INCLUDE_DI
 target_include_directories(kepler_formal PUBLIC ${ARGPARSE_DIR})
 target_link_libraries(kepler_formal
     naja_snl_pyloader
-    naja_dnl naja_opt formal_strategies yaml-cpp::yaml-cpp spdlog::spdlog)
+    naja_dnl naja_opt formal_strategies $<$<TARGET_EXISTS:yaml-cpp::yaml-cpp>:yaml-cpp::yaml-cpp>
+    $<$<TARGET_EXISTS:spdlog::spdlog>:spdlog::spdlog> )
 install(TARGETS kepler_formal DESTINATION ${CMAKE_INSTALL_BINDIR})

From 28f4f774fad01f4c2bc9d8aa163f45bf864679ef Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sat, 29 Nov 2025 23:05:08 +0100
Subject: [PATCH 12/43] fix

---
 .github/workflows/c-cpp.yml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml
index 76dac385..91d985ff 100644
--- a/.github/workflows/c-cpp.yml
+++ b/.github/workflows/c-cpp.yml
@@ -30,7 +30,8 @@ jobs:
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
       run: sudo apt-get update && sudo apt-get install -yq pkg-config libspdlog-dev libyaml-cpp-dev libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
-      
+    - name: Install dependencies with vcpkg
+      run: vcpkg install yaml-cpp
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
     - name: Build

From eeee7d2e2a75d50ac023e53a2c13463f4071a520 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 00:05:12 +0100
Subject: [PATCH 13/43] fix

---
 .github/workflows/c-cpp.yml   | 2 +-
 .github/workflows/regress.yml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml
index 91d985ff..88a9f8b8 100644
--- a/.github/workflows/c-cpp.yml
+++ b/.github/workflows/c-cpp.yml
@@ -29,7 +29,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -yq pkg-config libspdlog-dev libyaml-cpp-dev libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
+      run: sudo apt-get update && sudo apt-get install -yq pkg-config libspdlog-dev libyaml-cpp libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
     - name: Install dependencies with vcpkg
       run: vcpkg install yaml-cpp
     - name: Configure CMake
diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index 15a7bf99..6b2b91fe 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -30,7 +30,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -yq pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp-dev libspdlog-dev 
+      run: sudo apt-get update && sudo apt-get install -yq pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp libspdlog-dev 
       
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20

From f590a8abea9edd78e0ebb8a14835b9bab29456dc Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 00:08:18 +0100
Subject: [PATCH 14/43] fix

---
 .github/workflows/c-cpp.yml   | 2 +-
 .github/workflows/regress.yml | 2 +-
 src/bin/CMakeLists.txt        | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml
index 88a9f8b8..91d985ff 100644
--- a/.github/workflows/c-cpp.yml
+++ b/.github/workflows/c-cpp.yml
@@ -29,7 +29,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -yq pkg-config libspdlog-dev libyaml-cpp libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
+      run: sudo apt-get update && sudo apt-get install -yq pkg-config libspdlog-dev libyaml-cpp-dev libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
     - name: Install dependencies with vcpkg
       run: vcpkg install yaml-cpp
     - name: Configure CMake
diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index 6b2b91fe..15a7bf99 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -30,7 +30,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -yq pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp libspdlog-dev 
+      run: sudo apt-get update && sudo apt-get install -yq pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp-dev libspdlog-dev 
       
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
diff --git a/src/bin/CMakeLists.txt b/src/bin/CMakeLists.txt
index 15516e3a..05697f01 100644
--- a/src/bin/CMakeLists.txt
+++ b/src/bin/CMakeLists.txt
@@ -3,7 +3,7 @@
 
 add_executable(kepler_formal KeplerFormal.cpp)
 target_include_directories(kepler_formal SYSTEM BEFORE PUBLIC ${Boost_INCLUDE_DIR})
-target_include_directories(kepler_formal PUBLIC ${ARGPARSE_DIR})
+target_include_directories(kepler_formal PUBLIC ${ARGPARSE_DIR} ${YAML_CPP_INCLUDE_DIR})
 target_link_libraries(kepler_formal
     naja_snl_pyloader
     naja_dnl naja_opt formal_strategies $<$<TARGET_EXISTS:yaml-cpp::yaml-cpp>:yaml-cpp::yaml-cpp>

From a6efcab331c83f8a793171e1d268aa55422a6b20 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 00:35:53 +0100
Subject: [PATCH 15/43] fix

---
 CMakeLists.txt         | 44 +++++++++++++++++++++++-------------------
 src/bin/CMakeLists.txt |  4 ++--
 2 files changed, 26 insertions(+), 22 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 6bff3340..7e35e2ad 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -60,28 +60,32 @@ if(NOT TARGET yaml-cpp::yaml-cpp)
   endif()
 endif()
 
-# spdlog compatibility
-if(NOT TARGET spdlog::spdlog)
-  if(spdlog_FOUND)
-    add_library(spdlog::spdlog UNKNOWN IMPORTED)
-    if(DEFINED spdlog_LIBRARIES)
-      set_target_properties(spdlog::spdlog PROPERTIES IMPORTED_LOCATION "${spdlog_LIBRARIES}")
-    endif()
-    if(DEFINED spdlog_INCLUDE_DIRS)
-      set_property(TARGET spdlog::spdlog PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${spdlog_INCLUDE_DIRS}")
-    endif()
-  endif()
+# --- after your find_package(...) and compatibility imported-target creation ---
+
+# Canonical target variables (prefer modern names, fall back to vendored unnamespaced targets)
+if (TARGET yaml-cpp::yaml-cpp)
+  set(YAML_CPP_TARGET yaml-cpp::yaml-cpp)
+elseif (TARGET yaml-cpp)
+  set(YAML_CPP_TARGET yaml-cpp)
+else()
+  # yaml-cpp should already be REQUIRED above; this is defensive
+  message(FATAL_ERROR "yaml-cpp target not available")
 endif()
 
-# TBB compatibility (libtbb usually provides target TBB::tbb; provide fallback)
-if(NOT TARGET TBB::tbb)
-  if(TBB_FOUND AND DEFINED TBB_LIBRARY)
-    add_library(TBB::tbb UNKNOWN IMPORTED)
-    set_target_properties(TBB::tbb PROPERTIES IMPORTED_LOCATION "${TBB_LIBRARY}")
-    if(DEFINED TBB_INCLUDE_DIRS)
-      set_property(TARGET TBB::tbb PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${TBB_INCLUDE_DIRS}")
-    endif()
-  endif()
+if (TARGET spdlog::spdlog)
+  set(SPDLOG_TARGET spdlog::spdlog)
+elseif (TARGET spdlog)
+  set(SPDLOG_TARGET spdlog)
+else()
+  message(FATAL_ERROR "spdlog target not available")
+endif()
+
+if (TARGET TBB::tbb)
+  set(TBB_TARGET TBB::tbb)
+elseif (TARGET TBB)
+  set(TBB_TARGET TBB)
+else()
+  message(FATAL_ERROR "TBB target not available")
 endif()
 
 # If any package is required by your project policy, explicitly require them now.
diff --git a/src/bin/CMakeLists.txt b/src/bin/CMakeLists.txt
index 05697f01..cd5da51e 100644
--- a/src/bin/CMakeLists.txt
+++ b/src/bin/CMakeLists.txt
@@ -6,6 +6,6 @@ target_include_directories(kepler_formal SYSTEM BEFORE PUBLIC ${Boost_INCLUDE_DI
 target_include_directories(kepler_formal PUBLIC ${ARGPARSE_DIR} ${YAML_CPP_INCLUDE_DIR})
 target_link_libraries(kepler_formal
     naja_snl_pyloader
-    naja_dnl naja_opt formal_strategies $<$<TARGET_EXISTS:yaml-cpp::yaml-cpp>:yaml-cpp::yaml-cpp>
-    $<$<TARGET_EXISTS:spdlog::spdlog>:spdlog::spdlog> )
+    naja_dnl naja_opt formal_strategies ${YAML_CPP_TARGET}
+    ${SPDLOG_TARGET})
 install(TARGETS kepler_formal DESTINATION ${CMAKE_INSTALL_BINDIR})

From 0374345674334abfe381902c14250f98c6d5b14d Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 00:40:04 +0100
Subject: [PATCH 16/43] fix

---
 CMakeLists.txt         | 34 ++++++++++++++++++++++++++++------
 src/bin/CMakeLists.txt | 14 +++++++++++---
 2 files changed, 39 insertions(+), 9 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 7e35e2ad..67187021 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -60,16 +60,37 @@ if(NOT TARGET yaml-cpp::yaml-cpp)
   endif()
 endif()
 
-# --- after your find_package(...) and compatibility imported-target creation ---
+# spdlog compatibility
+if(NOT TARGET spdlog::spdlog)
+  if(spdlog_FOUND)
+    add_library(spdlog::spdlog UNKNOWN IMPORTED)
+    if(DEFINED spdlog_LIBRARIES)
+      set_target_properties(spdlog::spdlog PROPERTIES IMPORTED_LOCATION "${spdlog_LIBRARIES}")
+    endif()
+    if(DEFINED spdlog_INCLUDE_DIRS)
+      set_property(TARGET spdlog::spdlog PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${spdlog_INCLUDE_DIRS}")
+    endif()
+  endif()
+endif()
 
-# Canonical target variables (prefer modern names, fall back to vendored unnamespaced targets)
+# TBB compatibility (libtbb usually provides target TBB::tbb; provide fallback)
+if(NOT TARGET TBB::tbb)
+  if(TBB_FOUND AND DEFINED TBB_LIBRARY)
+    add_library(TBB::tbb UNKNOWN IMPORTED)
+    set_target_properties(TBB::tbb PROPERTIES IMPORTED_LOCATION "${TBB_LIBRARY}")
+    if(DEFINED TBB_INCLUDE_DIRS)
+      set_property(TARGET TBB::tbb PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${TBB_INCLUDE_DIRS}")
+    endif()
+  endif()
+endif()
+
+# Canonical target names (prefer namespaced targets, fall back to vendored names)
 if (TARGET yaml-cpp::yaml-cpp)
   set(YAML_CPP_TARGET yaml-cpp::yaml-cpp)
 elseif (TARGET yaml-cpp)
   set(YAML_CPP_TARGET yaml-cpp)
 else()
-  # yaml-cpp should already be REQUIRED above; this is defensive
-  message(FATAL_ERROR "yaml-cpp target not available")
+  message(FATAL_ERROR "yaml-cpp target not available; ensure find_package(yaml-cpp) succeeded or vendored yaml-cpp added")
 endif()
 
 if (TARGET spdlog::spdlog)
@@ -77,7 +98,7 @@ if (TARGET spdlog::spdlog)
 elseif (TARGET spdlog)
   set(SPDLOG_TARGET spdlog)
 else()
-  message(FATAL_ERROR "spdlog target not available")
+  message(FATAL_ERROR "spdlog target not available; ensure find_package(spdlog) succeeded or vendored spdlog added")
 endif()
 
 if (TARGET TBB::tbb)
@@ -85,9 +106,10 @@ if (TARGET TBB::tbb)
 elseif (TARGET TBB)
   set(TBB_TARGET TBB)
 else()
-  message(FATAL_ERROR "TBB target not available")
+  message(FATAL_ERROR "TBB target not available; ensure find_package(TBB) succeeded")
 endif()
 
+
 # If any package is required by your project policy, explicitly require them now.
 # Using REQUIRED to cause clear configure failure if not present.
 if(NOT TARGET yaml-cpp::yaml-cpp)
diff --git a/src/bin/CMakeLists.txt b/src/bin/CMakeLists.txt
index cd5da51e..7c62ee30 100644
--- a/src/bin/CMakeLists.txt
+++ b/src/bin/CMakeLists.txt
@@ -3,9 +3,17 @@
 
 add_executable(kepler_formal KeplerFormal.cpp)
 target_include_directories(kepler_formal SYSTEM BEFORE PUBLIC ${Boost_INCLUDE_DIR})
-target_include_directories(kepler_formal PUBLIC ${ARGPARSE_DIR} ${YAML_CPP_INCLUDE_DIR})
+target_include_directories(kepler_formal PUBLIC ${ARGPARSE_DIR})
+
 target_link_libraries(kepler_formal
+  PRIVATE
     naja_snl_pyloader
-    naja_dnl naja_opt formal_strategies ${YAML_CPP_TARGET}
-    ${SPDLOG_TARGET})
+    naja_dnl
+    naja_opt
+    formal_strategies
+    ${YAML_CPP_TARGET}
+    ${SPDLOG_TARGET}
+)
+
 install(TARGETS kepler_formal DESTINATION ${CMAKE_INSTALL_BINDIR})
+

From ec8a27d00fa616ad5ed6bd2df8a626993f263a1b Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 00:50:09 +0100
Subject: [PATCH 17/43] fix

---
 .github/workflows/c-cpp.yml   |   2 +-
 .github/workflows/regress.yml |   2 +-
 CMakeLists.txt                | 139 +++++++++++++++++++---------------
 3 files changed, 80 insertions(+), 63 deletions(-)

diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml
index 91d985ff..0315897d 100644
--- a/.github/workflows/c-cpp.yml
+++ b/.github/workflows/c-cpp.yml
@@ -29,7 +29,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -yq pkg-config libspdlog-dev libyaml-cpp-dev libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
+      run: sudo apt-get update && sudo apt-get install -y pkg-config libspdlog-dev libyaml-cpp-dev libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
     - name: Install dependencies with vcpkg
       run: vcpkg install yaml-cpp
     - name: Configure CMake
diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index 15a7bf99..5b97d83a 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -30,7 +30,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -yq pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp-dev libspdlog-dev 
+      run: sudo apt-get update && sudo apt-get install -y pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp-dev libspdlog-dev 
       
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 67187021..f6709a6e 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -31,66 +31,89 @@ set(ARGPARSE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/naja/thirdparty/argparse
 
 set(CMAKE_CXX_STANDARD 20 CACHE STRING "C++ standard" FORCE)
 
-# Find packages early so we can create compatibility imported targets if needed.
+# ---------------------------------------------------------------------------
+# Find dependencies (prefer system packages; fall back to vendored copies)
+# ---------------------------------------------------------------------------
+
+# Try system packages quietly first
 find_package(TBB QUIET)
 find_package(yaml-cpp QUIET)
 find_package(spdlog QUIET)
 
-# If find_package didn't create modern imported targets but did set legacy variables,
-# create lightweight imported targets for consistent usage below.
-# yaml-cpp compatibility
-if(NOT TARGET yaml-cpp::yaml-cpp)
-  if(yaml-cpp_FOUND)
-    # If module-mode provided YAML_CPP_LIBRARIES / INCLUDE dirs, create an imported target
-    add_library(yaml-cpp::yaml-cpp UNKNOWN IMPORTED)
-    if(DEFINED YAML_CPP_LIBRARIES)
-      set_target_properties(yaml-cpp::yaml-cpp PROPERTIES
-        IMPORTED_LOCATION "${YAML_CPP_LIBRARIES}")
-    elseif(DEFINED yaml-cpp_LIBRARIES)
-      set_target_properties(yaml-cpp::yaml-cpp PROPERTIES
-        IMPORTED_LOCATION "${yaml-cpp_LIBRARIES}")
-    endif()
-    if(DEFINED YAML_CPP_INCLUDE_DIR)
-      set_property(TARGET yaml-cpp::yaml-cpp PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${YAML_CPP_INCLUDE_DIR}")
-    elseif(DEFINED yaml-cpp_INCLUDE_DIRS)
-      set_property(TARGET yaml-cpp::yaml-cpp PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${yaml-cpp_INCLUDE_DIRS}")
-    endif()
-  else()
-    message(STATUS "yaml-cpp not found via quiet search; will fallback to REQUIRED search momentarily")
+# If system packages didn't provide modern imported targets, try to create
+# lightweight imported targets from legacy variables (keeps compatibility).
+# yaml-cpp compatibility (legacy variable names vary by distro/CMake mode)
+if(NOT TARGET yaml-cpp::yaml-cpp AND yaml-cpp_FOUND)
+  add_library(yaml-cpp::yaml-cpp UNKNOWN IMPORTED)
+  if(DEFINED YAML_CPP_LIBRARIES)
+    set_target_properties(yaml-cpp::yaml-cpp PROPERTIES IMPORTED_LOCATION "${YAML_CPP_LIBRARIES}")
+  elseif(DEFINED yaml-cpp_LIBRARIES)
+    set_target_properties(yaml-cpp::yaml-cpp PROPERTIES IMPORTED_LOCATION "${yaml-cpp_LIBRARIES}")
+  endif()
+  if(DEFINED YAML_CPP_INCLUDE_DIR)
+    set_property(TARGET yaml-cpp::yaml-cpp PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${YAML_CPP_INCLUDE_DIR}")
+  elseif(DEFINED yaml-cpp_INCLUDE_DIRS)
+    set_property(TARGET yaml-cpp::yaml-cpp PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${yaml-cpp_INCLUDE_DIRS}")
   endif()
 endif()
 
 # spdlog compatibility
+if(NOT TARGET spdlog::spdlog AND spdlog_FOUND)
+  add_library(spdlog::spdlog UNKNOWN IMPORTED)
+  if(DEFINED spdlog_LIBRARIES)
+    set_target_properties(spdlog::spdlog PROPERTIES IMPORTED_LOCATION "${spdlog_LIBRARIES}")
+  endif()
+  if(DEFINED spdlog_INCLUDE_DIRS)
+    set_property(TARGET spdlog::spdlog PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${spdlog_INCLUDE_DIRS}")
+  endif()
+endif()
+
+# TBB compatibility
+if(NOT TARGET TBB::tbb AND TBB_FOUND AND DEFINED TBB_LIBRARY)
+  add_library(TBB::tbb UNKNOWN IMPORTED)
+  set_target_properties(TBB::tbb PROPERTIES IMPORTED_LOCATION "${TBB_LIBRARY}")
+  if(DEFINED TBB_INCLUDE_DIRS)
+    set_property(TARGET TBB::tbb PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${TBB_INCLUDE_DIRS}")
+  endif()
+endif()
+
+# ---------------------------------------------------------------------------
+# Fallback: if system packages not found, try vendored thirdparty directories
+# (these add_subdirectory calls must happen before any subdir that links them)
+# ---------------------------------------------------------------------------
+
+# yaml-cpp: prefer system, else vendored
+if(NOT TARGET yaml-cpp::yaml-cpp)
+  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/yaml-cpp/CMakeLists.txt")
+    message(STATUS "Using vendored yaml-cpp from thirdparty/yaml-cpp")
+    add_subdirectory(thirdparty/yaml-cpp EXCLUDE_FROM_ALL)
+  endif()
+endif()
+
+# spdlog: prefer system, else vendored
 if(NOT TARGET spdlog::spdlog)
-  if(spdlog_FOUND)
-    add_library(spdlog::spdlog UNKNOWN IMPORTED)
-    if(DEFINED spdlog_LIBRARIES)
-      set_target_properties(spdlog::spdlog PROPERTIES IMPORTED_LOCATION "${spdlog_LIBRARIES}")
-    endif()
-    if(DEFINED spdlog_INCLUDE_DIRS)
-      set_property(TARGET spdlog::spdlog PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${spdlog_INCLUDE_DIRS}")
-    endif()
+  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/spdlog/CMakeLists.txt")
+    message(STATUS "Using vendored spdlog from thirdparty/spdlog")
+    add_subdirectory(thirdparty/spdlog EXCLUDE_FROM_ALL)
   endif()
 endif()
 
-# TBB compatibility (libtbb usually provides target TBB::tbb; provide fallback)
+# TBB: prefer system; vendored TBB is uncommon, so require system if not present
 if(NOT TARGET TBB::tbb)
-  if(TBB_FOUND AND DEFINED TBB_LIBRARY)
-    add_library(TBB::tbb UNKNOWN IMPORTED)
-    set_target_properties(TBB::tbb PROPERTIES IMPORTED_LOCATION "${TBB_LIBRARY}")
-    if(DEFINED TBB_INCLUDE_DIRS)
-      set_property(TARGET TBB::tbb PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${TBB_INCLUDE_DIRS}")
-    endif()
+  if (NOT TBB_FOUND)
+    message(FATAL_ERROR "TBB not found. Install system TBB or vendor it under thirdparty/")
   endif()
 endif()
 
-# Canonical target names (prefer namespaced targets, fall back to vendored names)
+# ---------------------------------------------------------------------------
+# Canonical target variables (subprojects should use these names)
+# ---------------------------------------------------------------------------
 if (TARGET yaml-cpp::yaml-cpp)
   set(YAML_CPP_TARGET yaml-cpp::yaml-cpp)
 elseif (TARGET yaml-cpp)
   set(YAML_CPP_TARGET yaml-cpp)
 else()
-  message(FATAL_ERROR "yaml-cpp target not available; ensure find_package(yaml-cpp) succeeded or vendored yaml-cpp added")
+  message(FATAL_ERROR "yaml-cpp target not available; ensure system package installed or vendored copy present")
 endif()
 
 if (TARGET spdlog::spdlog)
@@ -98,7 +121,7 @@ if (TARGET spdlog::spdlog)
 elseif (TARGET spdlog)
   set(SPDLOG_TARGET spdlog)
 else()
-  message(FATAL_ERROR "spdlog target not available; ensure find_package(spdlog) succeeded or vendored spdlog added")
+  message(FATAL_ERROR "spdlog target not available; ensure system package installed or vendored copy present")
 endif()
 
 if (TARGET TBB::tbb)
@@ -106,45 +129,39 @@ if (TARGET TBB::tbb)
 elseif (TARGET TBB)
   set(TBB_TARGET TBB)
 else()
-  message(FATAL_ERROR "TBB target not available; ensure find_package(TBB) succeeded")
+  message(FATAL_ERROR "TBB target not available; ensure system package installed")
 endif()
 
+message(STATUS "Using YAML_CPP_TARGET = ${YAML_CPP_TARGET}")
+message(STATUS "Using SPDLOG_TARGET  = ${SPDLOG_TARGET}")
+message(STATUS "Using TBB_TARGET     = ${TBB_TARGET}")
 
-# If any package is required by your project policy, explicitly require them now.
-# Using REQUIRED to cause clear configure failure if not present.
-if(NOT TARGET yaml-cpp::yaml-cpp)
-  find_package(yaml-cpp REQUIRED)  # will error if missing
-endif()
-if(NOT TARGET spdlog::spdlog)
-  find_package(spdlog REQUIRED)
-endif()
-if(NOT TARGET TBB::tbb)
-  find_package(TBB REQUIRED)
-endif()
-
+# ---------------------------------------------------------------------------
 # Add project subdirectories (these define formal_structures and others).
+# ---------------------------------------------------------------------------
 add_subdirectory(src)
 add_subdirectory(thirdparty)
 include(CTest)
 add_subdirectory(test)
 
-# Now, only set include_directories / link libraries if the formal_structures
-# target exists. This avoids ordering issues.
+# ---------------------------------------------------------------------------
+# Top-level link/include setup for formal_structures (guarded)
+# ---------------------------------------------------------------------------
 if(TARGET formal_structures)
   # Include TBB headers (TBB::tbb provides interface dirs; keep fallback path for macOS Homebrew)
   target_include_directories(formal_structures
     PRIVATE
-      $<$<TARGET_EXISTS:TBB::tbb>:$<TARGET_PROPERTY:TBB::tbb,INTERFACE_INCLUDE_DIRECTORIES>>
+      $<$<TARGET_EXISTS:${TBB_TARGET}>:$<TARGET_PROPERTY:${TBB_TARGET},INTERFACE_INCLUDE_DIRECTORIES>>
       /opt/homebrew/include
   )
 
-  # Link to available targets in a guarded way.
+  # Link to available targets using canonical variables
   target_link_libraries(formal_structures
     PRIVATE
-      $<$<TARGET_EXISTS:TBB::tbb>:TBB::tbb>
-      $<$<TARGET_EXISTS:yaml-cpp::yaml-cpp>:yaml-cpp::yaml-cpp>
-      $<$<TARGET_EXISTS:spdlog::spdlog>:spdlog::spdlog>
+      $<$<BOOL:${TBB_TARGET}>:${TBB_TARGET}>
+      $<$<BOOL:${YAML_CPP_TARGET}>:${YAML_CPP_TARGET}>
+      $<$<BOOL:${SPDLOG_TARGET}>:${SPDLOG_TARGET}>
   )
 else()
   message(WARNING "formal_structures target was not defined by subdirectories; skipping top-level link/include setup.")
-endif()
\ No newline at end of file
+endif()

From 9eb58095363256d1f8692957714f2ca9da25500d Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 00:53:44 +0100
Subject: [PATCH 18/43] fix

---
 src/bin/CMakeLists.txt | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

diff --git a/src/bin/CMakeLists.txt b/src/bin/CMakeLists.txt
index 7c62ee30..0e992590 100644
--- a/src/bin/CMakeLists.txt
+++ b/src/bin/CMakeLists.txt
@@ -3,17 +3,9 @@
 
 add_executable(kepler_formal KeplerFormal.cpp)
 target_include_directories(kepler_formal SYSTEM BEFORE PUBLIC ${Boost_INCLUDE_DIR})
-target_include_directories(kepler_formal PUBLIC ${ARGPARSE_DIR})
-
+target_include_directories(kepler_formal PUBLIC ${ARGPARSE_DIR} ${YAML_CPP_INCLUDE_DIR})
 target_link_libraries(kepler_formal
-  PRIVATE
     naja_snl_pyloader
-    naja_dnl
-    naja_opt
-    formal_strategies
-    ${YAML_CPP_TARGET}
-    ${SPDLOG_TARGET}
-)
+    naja_dnl naja_opt formal_strategies yaml-cpp::yaml-cpp spdlog::spdlog)
 
-install(TARGETS kepler_formal DESTINATION ${CMAKE_INSTALL_BINDIR})
 

From 29f304d34af0c0b9c6759fbf53c400b47ed3d326 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 00:59:41 +0100
Subject: [PATCH 19/43] fix

---
 CMakeLists.txt         | 42 ++++++++++++++----------------------------
 src/bin/CMakeLists.txt | 11 +++++++++--
 2 files changed, 23 insertions(+), 30 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index f6709a6e..ee4eb2ac 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -2,8 +2,6 @@
 # SPDX-License-Identifier: GPL-3.0-only
 
 cmake_minimum_required(VERSION 3.21)
-# tell CMake to pretend any cmake_minimum_required(VERSION X) with X<3.5
-# is OK.  Mirrors the -DCMAKE_POLICY_VERSION_MINIMUM=3.5 hack.
 set(CMAKE_POLICY_VERSION_MINIMUM 3.5 CACHE INTERNAL
     "Allow parsing of subprojects that require CMake < 3.5")
 
@@ -17,12 +15,8 @@ project(kepler-formal
   HOMEPAGE_URL https://github.com/keplertech/kepler-formal
 )
 
-# Option to enable/disable the Python interface. CI disables it by default.
 option(PYTHON_INTERFACE "Enable Python interface" OFF)
 
-# If the python interface is disabled, provide a no-op INTERFACE target so
-# other targets that unconditionally link PYTHON_INTERFACE still configure.
-# This must be created before add_subdirectory(...) so subprojects can link to it.
 if(NOT PYTHON_INTERFACE AND NOT TARGET PYTHON_INTERFACE)
   add_library(PYTHON_INTERFACE INTERFACE)
 endif()
@@ -32,17 +26,16 @@ set(ARGPARSE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/naja/thirdparty/argparse
 set(CMAKE_CXX_STANDARD 20 CACHE STRING "C++ standard" FORCE)
 
 # ---------------------------------------------------------------------------
-# Find dependencies (prefer system packages; fall back to vendored copies)
+# Try system packages first (quiet). We'll fall back to vendored copies below.
 # ---------------------------------------------------------------------------
-
-# Try system packages quietly first
 find_package(TBB QUIET)
 find_package(yaml-cpp QUIET)
 find_package(spdlog QUIET)
 
-# If system packages didn't provide modern imported targets, try to create
-# lightweight imported targets from legacy variables (keeps compatibility).
-# yaml-cpp compatibility (legacy variable names vary by distro/CMake mode)
+# ---------------------------------------------------------------------------
+# If system packages provided legacy variables but no imported targets, create
+# lightweight imported targets so subprojects can link consistently.
+# ---------------------------------------------------------------------------
 if(NOT TARGET yaml-cpp::yaml-cpp AND yaml-cpp_FOUND)
   add_library(yaml-cpp::yaml-cpp UNKNOWN IMPORTED)
   if(DEFINED YAML_CPP_LIBRARIES)
@@ -57,7 +50,6 @@ if(NOT TARGET yaml-cpp::yaml-cpp AND yaml-cpp_FOUND)
   endif()
 endif()
 
-# spdlog compatibility
 if(NOT TARGET spdlog::spdlog AND spdlog_FOUND)
   add_library(spdlog::spdlog UNKNOWN IMPORTED)
   if(DEFINED spdlog_LIBRARIES)
@@ -68,7 +60,6 @@ if(NOT TARGET spdlog::spdlog AND spdlog_FOUND)
   endif()
 endif()
 
-# TBB compatibility
 if(NOT TARGET TBB::tbb AND TBB_FOUND AND DEFINED TBB_LIBRARY)
   add_library(TBB::tbb UNKNOWN IMPORTED)
   set_target_properties(TBB::tbb PROPERTIES IMPORTED_LOCATION "${TBB_LIBRARY}")
@@ -78,29 +69,26 @@ if(NOT TARGET TBB::tbb AND TBB_FOUND AND DEFINED TBB_LIBRARY)
 endif()
 
 # ---------------------------------------------------------------------------
-# Fallback: if system packages not found, try vendored thirdparty directories
-# (these add_subdirectory calls must happen before any subdir that links them)
+# Vendored fallback: add_subdirectory for thirdparty copies if system not found.
+# These must be added before subdirs that link to them.
 # ---------------------------------------------------------------------------
-
-# yaml-cpp: prefer system, else vendored
 if(NOT TARGET yaml-cpp::yaml-cpp)
-  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/yaml-cpp/CMakeLists.txt")
+  if(EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/yaml-cpp/CMakeLists.txt")
     message(STATUS "Using vendored yaml-cpp from thirdparty/yaml-cpp")
     add_subdirectory(thirdparty/yaml-cpp EXCLUDE_FROM_ALL)
   endif()
 endif()
 
-# spdlog: prefer system, else vendored
 if(NOT TARGET spdlog::spdlog)
-  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/spdlog/CMakeLists.txt")
+  if(EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/spdlog/CMakeLists.txt")
     message(STATUS "Using vendored spdlog from thirdparty/spdlog")
     add_subdirectory(thirdparty/spdlog EXCLUDE_FROM_ALL)
   endif()
 endif()
 
-# TBB: prefer system; vendored TBB is uncommon, so require system if not present
+# Require TBB from system (common on CI). If you vendor TBB, add similar fallback.
 if(NOT TARGET TBB::tbb)
-  if (NOT TBB_FOUND)
+  if(NOT TBB_FOUND)
     message(FATAL_ERROR "TBB not found. Install system TBB or vendor it under thirdparty/")
   endif()
 endif()
@@ -113,7 +101,7 @@ if (TARGET yaml-cpp::yaml-cpp)
 elseif (TARGET yaml-cpp)
   set(YAML_CPP_TARGET yaml-cpp)
 else()
-  message(FATAL_ERROR "yaml-cpp target not available; ensure system package installed or vendored copy present")
+  message(FATAL_ERROR "yaml-cpp target not available; install libyaml-cpp-dev or add thirdparty/yaml-cpp")
 endif()
 
 if (TARGET spdlog::spdlog)
@@ -121,7 +109,7 @@ if (TARGET spdlog::spdlog)
 elseif (TARGET spdlog)
   set(SPDLOG_TARGET spdlog)
 else()
-  message(FATAL_ERROR "spdlog target not available; ensure system package installed or vendored copy present")
+  message(FATAL_ERROR "spdlog target not available; install libspdlog-dev or add thirdparty/spdlog")
 endif()
 
 if (TARGET TBB::tbb)
@@ -129,7 +117,7 @@ if (TARGET TBB::tbb)
 elseif (TARGET TBB)
   set(TBB_TARGET TBB)
 else()
-  message(FATAL_ERROR "TBB target not available; ensure system package installed")
+  message(FATAL_ERROR "TBB target not available; ensure system TBB is installed")
 endif()
 
 message(STATUS "Using YAML_CPP_TARGET = ${YAML_CPP_TARGET}")
@@ -148,14 +136,12 @@ add_subdirectory(test)
 # Top-level link/include setup for formal_structures (guarded)
 # ---------------------------------------------------------------------------
 if(TARGET formal_structures)
-  # Include TBB headers (TBB::tbb provides interface dirs; keep fallback path for macOS Homebrew)
   target_include_directories(formal_structures
     PRIVATE
       $<$<TARGET_EXISTS:${TBB_TARGET}>:$<TARGET_PROPERTY:${TBB_TARGET},INTERFACE_INCLUDE_DIRECTORIES>>
       /opt/homebrew/include
   )
 
-  # Link to available targets using canonical variables
   target_link_libraries(formal_structures
     PRIVATE
       $<$<BOOL:${TBB_TARGET}>:${TBB_TARGET}>
diff --git a/src/bin/CMakeLists.txt b/src/bin/CMakeLists.txt
index 0e992590..2d6d5630 100644
--- a/src/bin/CMakeLists.txt
+++ b/src/bin/CMakeLists.txt
@@ -3,9 +3,16 @@
 
 add_executable(kepler_formal KeplerFormal.cpp)
 target_include_directories(kepler_formal SYSTEM BEFORE PUBLIC ${Boost_INCLUDE_DIR})
-target_include_directories(kepler_formal PUBLIC ${ARGPARSE_DIR} ${YAML_CPP_INCLUDE_DIR})
+target_include_directories(kepler_formal PUBLIC ${ARGPARSE_DIR})
+
 target_link_libraries(kepler_formal
+  PRIVATE
     naja_snl_pyloader
-    naja_dnl naja_opt formal_strategies yaml-cpp::yaml-cpp spdlog::spdlog)
+    naja_dnl
+    naja_opt
+    formal_strategies
+    ${YAML_CPP_TARGET}
+    ${SPDLOG_TARGET}
+)
 
 

From 670f3ea3a56c481fd0d9f508c39ebab3e6defc18 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 01:04:17 +0100
Subject: [PATCH 20/43] fix

---
 .github/workflows/c-cpp.yml | 42 ++++++++++++++++++-------------------
 1 file changed, 21 insertions(+), 21 deletions(-)

diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml
index 0315897d..8160d548 100644
--- a/.github/workflows/c-cpp.yml
+++ b/.github/workflows/c-cpp.yml
@@ -8,40 +8,40 @@ on:
   workflow_dispatch:
 
 env:
-  # Customize the CMake build type here (Release, Debug, RelWithDebInfo, etc.)
   BUILD_TYPE: Debug
 
 jobs:
   build:
-    # The CMake configure and build commands are platform agnostic and should work equally
-    # well on Windows or Mac.  You can convert this to a matrix build if you need
-    # cross-platform coverage.
-    # See: https://docs.github.com/en/free-pro-team@latest/actions/learn-github-actions/managing-complex-workflows#using-a-build-matrix
     runs-on: ubuntu-22.04
 
     steps:
     - uses: actions/checkout@v4
       with:
         submodules: true
-    # install dependencies
-    - name: Install GoogleTest
-      run: sudo apt-get update && sudo apt-get install -y libgtest-dev cmake
-    - name: Checkout submodules
-      run: git submodule update --init --recursive
-    - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -y pkg-config libspdlog-dev libyaml-cpp-dev libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev
-    - name: Install dependencies with vcpkg
-      run: vcpkg install yaml-cpp
+
+    - name: Install system dependencies
+      run: |
+        sudo apt-get update
+        sudo apt-get install -yq \
+          build-essential cmake ninja-build clang pkg-config \
+          libboost-dev libfl-dev libtbb-dev capnproto libcapnp-dev \
+          libgtest-dev libspdlog-dev libyaml-cpp-dev
+
     - name: Configure CMake
-      run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
+      run: |
+        rm -rf build
+        cmake -B build -GNinja \
+          -DCMAKE_BUILD_TYPE=${{ env.BUILD_TYPE }} \
+          -DCMAKE_C_COMPILER=clang \
+          -DENABLE_SANITIZERS=ON \
+          -DPYTHON_INTERFACE=OFF \
+          -DCMAKE_CXX_STANDARD=20
+
     - name: Build
-      # Build your program with the given configuration
-      run: cmake --build ${{github.workspace}}/build --config ${{env.BUILD_TYPE}}
+      run: cmake --build build --config ${{ env.BUILD_TYPE }} -- -j
 
     - name: Test
-      working-directory: ${{github.workspace}}/build
+      working-directory: build
       env:
         PYTHONMALLOC: malloc
-      # Execute tests defined by the CMake configuration.  
-      # See https://cmake.org/cmake/help/latest/manual/ctest.1.html for more detail
-      run: ctest -VV -E ".*[p|P]ython.*" -C ${{env.BUILD_TYPE}}
+      run: ctest -VV -E ".*[p|P]ython.*" -C ${{ env.BUILD_TYPE }}

From c707644379457ececbeaf4202a934403e4be5330 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 01:06:53 +0100
Subject: [PATCH 21/43] fix

---
 .github/workflows/c-cpp.yml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml
index 8160d548..e08f3c68 100644
--- a/.github/workflows/c-cpp.yml
+++ b/.github/workflows/c-cpp.yml
@@ -18,7 +18,12 @@ jobs:
     - uses: actions/checkout@v4
       with:
         submodules: true
-
+     # install dependencies
+    - name: Install GoogleTest
+      run: sudo apt-get update && sudo apt-get install -y libgtest-dev cmake
+    - name: Checkout submodules
+      run: git submodule update --init --recursive
+ 
     - name: Install system dependencies
       run: |
         sudo apt-get update

From 717078fa441d9e03e8ac9d6c5d672068cf7890f8 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 01:11:35 +0100
Subject: [PATCH 22/43] fix

---
 .github/workflows/c-cpp.yml | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml
index e08f3c68..64836ff7 100644
--- a/.github/workflows/c-cpp.yml
+++ b/.github/workflows/c-cpp.yml
@@ -35,18 +35,15 @@ jobs:
     - name: Configure CMake
       run: |
         rm -rf build
-        cmake -B build -GNinja \
-          -DCMAKE_BUILD_TYPE=${{ env.BUILD_TYPE }} \
-          -DCMAKE_C_COMPILER=clang \
-          -DENABLE_SANITIZERS=ON \
-          -DPYTHON_INTERFACE=OFF \
-          -DCMAKE_CXX_STANDARD=20
+        run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
+  
 
     - name: Build
-      run: cmake --build build --config ${{ env.BUILD_TYPE }} -- -j
+      run: cmake --build ${{github.workspace}}/build --config ${{env.BUILD_TYPE}}
 
     - name: Test
-      working-directory: build
+      working-directory: ${{github.workspace}}/build
       env:
         PYTHONMALLOC: malloc
       run: ctest -VV -E ".*[p|P]ython.*" -C ${{ env.BUILD_TYPE }}
+

From 48a927e166de77eb883d7f33e3e00e089f48e8b6 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 01:15:00 +0100
Subject: [PATCH 23/43] fix

---
 .github/workflows/c-cpp.yml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml
index 64836ff7..256d0c71 100644
--- a/.github/workflows/c-cpp.yml
+++ b/.github/workflows/c-cpp.yml
@@ -33,9 +33,10 @@ jobs:
           libgtest-dev libspdlog-dev libyaml-cpp-dev
 
     - name: Configure CMake
+      working-directory: ${{github.workspace}}/
       run: |
         rm -rf build
-        run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
+        cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
   
 
     - name: Build

From ceaa20eb5668969234ba15989e56abf53a54d94c Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 01:21:22 +0100
Subject: [PATCH 24/43] fix

---
 src/bin/CMakeLists.txt | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/bin/CMakeLists.txt b/src/bin/CMakeLists.txt
index 2d6d5630..7c62ee30 100644
--- a/src/bin/CMakeLists.txt
+++ b/src/bin/CMakeLists.txt
@@ -15,4 +15,5 @@ target_link_libraries(kepler_formal
     ${SPDLOG_TARGET}
 )
 
+install(TARGETS kepler_formal DESTINATION ${CMAKE_INSTALL_BINDIR})
 

From 4c125b1d570ce5113f4414343ad93242c61606fe Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 01:34:29 +0100
Subject: [PATCH 25/43] fix

---
 .gitmodules               |  3 +++
 CMakeLists.txt            | 27 ---------------------------
 src/bin/CMakeLists.txt    |  2 +-
 thirdparty/CMakeLists.txt |  1 +
 thirdparty/yaml-cpp       |  1 +
 5 files changed, 6 insertions(+), 28 deletions(-)
 create mode 160000 thirdparty/yaml-cpp

diff --git a/.gitmodules b/.gitmodules
index 023d22f1..03af70c6 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -4,3 +4,6 @@
 [submodule "thirdparty/naja"]
 	path = thirdparty/naja
 	url = https://github.com/nanocoh/naja.git
+[submodule "thirdparty/yaml-cpp"]
+	path = thirdparty/yaml-cpp
+	url = https://github.com/jbeder/yaml-cpp.git
diff --git a/CMakeLists.txt b/CMakeLists.txt
index ee4eb2ac..ca9b362e 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -29,26 +29,12 @@ set(CMAKE_CXX_STANDARD 20 CACHE STRING "C++ standard" FORCE)
 # Try system packages first (quiet). We'll fall back to vendored copies below.
 # ---------------------------------------------------------------------------
 find_package(TBB QUIET)
-find_package(yaml-cpp QUIET)
 find_package(spdlog QUIET)
 
 # ---------------------------------------------------------------------------
 # If system packages provided legacy variables but no imported targets, create
 # lightweight imported targets so subprojects can link consistently.
 # ---------------------------------------------------------------------------
-if(NOT TARGET yaml-cpp::yaml-cpp AND yaml-cpp_FOUND)
-  add_library(yaml-cpp::yaml-cpp UNKNOWN IMPORTED)
-  if(DEFINED YAML_CPP_LIBRARIES)
-    set_target_properties(yaml-cpp::yaml-cpp PROPERTIES IMPORTED_LOCATION "${YAML_CPP_LIBRARIES}")
-  elseif(DEFINED yaml-cpp_LIBRARIES)
-    set_target_properties(yaml-cpp::yaml-cpp PROPERTIES IMPORTED_LOCATION "${yaml-cpp_LIBRARIES}")
-  endif()
-  if(DEFINED YAML_CPP_INCLUDE_DIR)
-    set_property(TARGET yaml-cpp::yaml-cpp PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${YAML_CPP_INCLUDE_DIR}")
-  elseif(DEFINED yaml-cpp_INCLUDE_DIRS)
-    set_property(TARGET yaml-cpp::yaml-cpp PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${yaml-cpp_INCLUDE_DIRS}")
-  endif()
-endif()
 
 if(NOT TARGET spdlog::spdlog AND spdlog_FOUND)
   add_library(spdlog::spdlog UNKNOWN IMPORTED)
@@ -72,12 +58,6 @@ endif()
 # Vendored fallback: add_subdirectory for thirdparty copies if system not found.
 # These must be added before subdirs that link to them.
 # ---------------------------------------------------------------------------
-if(NOT TARGET yaml-cpp::yaml-cpp)
-  if(EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/yaml-cpp/CMakeLists.txt")
-    message(STATUS "Using vendored yaml-cpp from thirdparty/yaml-cpp")
-    add_subdirectory(thirdparty/yaml-cpp EXCLUDE_FROM_ALL)
-  endif()
-endif()
 
 if(NOT TARGET spdlog::spdlog)
   if(EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/spdlog/CMakeLists.txt")
@@ -96,13 +76,6 @@ endif()
 # ---------------------------------------------------------------------------
 # Canonical target variables (subprojects should use these names)
 # ---------------------------------------------------------------------------
-if (TARGET yaml-cpp::yaml-cpp)
-  set(YAML_CPP_TARGET yaml-cpp::yaml-cpp)
-elseif (TARGET yaml-cpp)
-  set(YAML_CPP_TARGET yaml-cpp)
-else()
-  message(FATAL_ERROR "yaml-cpp target not available; install libyaml-cpp-dev or add thirdparty/yaml-cpp")
-endif()
 
 if (TARGET spdlog::spdlog)
   set(SPDLOG_TARGET spdlog::spdlog)
diff --git a/src/bin/CMakeLists.txt b/src/bin/CMakeLists.txt
index 7c62ee30..bf576969 100644
--- a/src/bin/CMakeLists.txt
+++ b/src/bin/CMakeLists.txt
@@ -11,7 +11,7 @@ target_link_libraries(kepler_formal
     naja_dnl
     naja_opt
     formal_strategies
-    ${YAML_CPP_TARGET}
+    yaml-cpp
     ${SPDLOG_TARGET}
 )
 
diff --git a/thirdparty/CMakeLists.txt b/thirdparty/CMakeLists.txt
index 192f1947..f09374cb 100644
--- a/thirdparty/CMakeLists.txt
+++ b/thirdparty/CMakeLists.txt
@@ -3,4 +3,5 @@
 
 add_subdirectory(naja)
 add_subdirectory(glucose)
+add_subdirectory(yaml-cpp)
 #add_subdirectory(cpptrace EXCLUDE_FROM_ALL)
diff --git a/thirdparty/yaml-cpp b/thirdparty/yaml-cpp
new file mode 160000
index 00000000..a83cd315
--- /dev/null
+++ b/thirdparty/yaml-cpp
@@ -0,0 +1 @@
+Subproject commit a83cd31548b19d50f3f983b069dceb4f4d50756d

From b1f97ce34621c12af40dce72cacbb2da449afef8 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 01:43:21 +0100
Subject: [PATCH 26/43] fix

---
 .github/workflows/c-cpp.yml |   2 +-
 CMakeLists.txt              | 112 +++++-------------------------------
 2 files changed, 14 insertions(+), 100 deletions(-)

diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml
index 256d0c71..f9d60434 100644
--- a/.github/workflows/c-cpp.yml
+++ b/.github/workflows/c-cpp.yml
@@ -30,7 +30,7 @@ jobs:
         sudo apt-get install -yq \
           build-essential cmake ninja-build clang pkg-config \
           libboost-dev libfl-dev libtbb-dev capnproto libcapnp-dev \
-          libgtest-dev libspdlog-dev libyaml-cpp-dev
+          libgtest-dev libspdlog-dev libfmt-dev
 
     - name: Configure CMake
       working-directory: ${{github.workspace}}/
diff --git a/CMakeLists.txt b/CMakeLists.txt
index ca9b362e..68dbc8f2 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -2,6 +2,8 @@
 # SPDX-License-Identifier: GPL-3.0-only
 
 cmake_minimum_required(VERSION 3.21)
+# tell CMake to pretend any cmake_minimum_required(VERSION X) with X<3.5
+# is OK.  Mirrors the -DCMAKE_POLICY_VERSION_MINIMUM=3.5 hack.
 set(CMAKE_POLICY_VERSION_MINIMUM 3.5 CACHE INTERNAL
     "Allow parsing of subprojects that require CMake < 3.5")
 
@@ -15,112 +17,24 @@ project(kepler-formal
   HOMEPAGE_URL https://github.com/keplertech/kepler-formal
 )
 
-option(PYTHON_INTERFACE "Enable Python interface" OFF)
-
-if(NOT PYTHON_INTERFACE AND NOT TARGET PYTHON_INTERFACE)
-  add_library(PYTHON_INTERFACE INTERFACE)
-endif()
-
 set(ARGPARSE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/naja/thirdparty/argparse-3.1/include)
 
 set(CMAKE_CXX_STANDARD 20 CACHE STRING "C++ standard" FORCE)
 
-# ---------------------------------------------------------------------------
-# Try system packages first (quiet). We'll fall back to vendored copies below.
-# ---------------------------------------------------------------------------
-find_package(TBB QUIET)
-find_package(spdlog QUIET)
-
-# ---------------------------------------------------------------------------
-# If system packages provided legacy variables but no imported targets, create
-# lightweight imported targets so subprojects can link consistently.
-# ---------------------------------------------------------------------------
-
-if(NOT TARGET spdlog::spdlog AND spdlog_FOUND)
-  add_library(spdlog::spdlog UNKNOWN IMPORTED)
-  if(DEFINED spdlog_LIBRARIES)
-    set_target_properties(spdlog::spdlog PROPERTIES IMPORTED_LOCATION "${spdlog_LIBRARIES}")
-  endif()
-  if(DEFINED spdlog_INCLUDE_DIRS)
-    set_property(TARGET spdlog::spdlog PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${spdlog_INCLUDE_DIRS}")
-  endif()
-endif()
-
-if(NOT TARGET TBB::tbb AND TBB_FOUND AND DEFINED TBB_LIBRARY)
-  add_library(TBB::tbb UNKNOWN IMPORTED)
-  set_target_properties(TBB::tbb PROPERTIES IMPORTED_LOCATION "${TBB_LIBRARY}")
-  if(DEFINED TBB_INCLUDE_DIRS)
-    set_property(TARGET TBB::tbb PROPERTY INTERFACE_INCLUDE_DIRECTORIES "${TBB_INCLUDE_DIRS}")
-  endif()
-endif()
-
-# ---------------------------------------------------------------------------
-# Vendored fallback: add_subdirectory for thirdparty copies if system not found.
-# These must be added before subdirs that link to them.
-# ---------------------------------------------------------------------------
-
-if(NOT TARGET spdlog::spdlog)
-  if(EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/thirdparty/spdlog/CMakeLists.txt")
-    message(STATUS "Using vendored spdlog from thirdparty/spdlog")
-    add_subdirectory(thirdparty/spdlog EXCLUDE_FROM_ALL)
-  endif()
-endif()
-
-# Require TBB from system (common on CI). If you vendor TBB, add similar fallback.
-if(NOT TARGET TBB::tbb)
-  if(NOT TBB_FOUND)
-    message(FATAL_ERROR "TBB not found. Install system TBB or vendor it under thirdparty/")
-  endif()
-endif()
-
-# ---------------------------------------------------------------------------
-# Canonical target variables (subprojects should use these names)
-# ---------------------------------------------------------------------------
-
-if (TARGET spdlog::spdlog)
-  set(SPDLOG_TARGET spdlog::spdlog)
-elseif (TARGET spdlog)
-  set(SPDLOG_TARGET spdlog)
-else()
-  message(FATAL_ERROR "spdlog target not available; install libspdlog-dev or add thirdparty/spdlog")
-endif()
-
-if (TARGET TBB::tbb)
-  set(TBB_TARGET TBB::tbb)
-elseif (TARGET TBB)
-  set(TBB_TARGET TBB)
-else()
-  message(FATAL_ERROR "TBB target not available; ensure system TBB is installed")
-endif()
-
-message(STATUS "Using YAML_CPP_TARGET = ${YAML_CPP_TARGET}")
-message(STATUS "Using SPDLOG_TARGET  = ${SPDLOG_TARGET}")
-message(STATUS "Using TBB_TARGET     = ${TBB_TARGET}")
-
-# ---------------------------------------------------------------------------
-# Add project subdirectories (these define formal_structures and others).
-# ---------------------------------------------------------------------------
 add_subdirectory(src)
 add_subdirectory(thirdparty)
 include(CTest)
 add_subdirectory(test)
 
-# ---------------------------------------------------------------------------
-# Top-level link/include setup for formal_structures (guarded)
-# ---------------------------------------------------------------------------
-if(TARGET formal_structures)
-  target_include_directories(formal_structures
-    PRIVATE
-      $<$<TARGET_EXISTS:${TBB_TARGET}>:$<TARGET_PROPERTY:${TBB_TARGET},INTERFACE_INCLUDE_DIRECTORIES>>
-      /opt/homebrew/include
-  )
+find_package(TBB REQUIRED)
+
+# if you’re using find_package(TBB), ensure it picked up Homebrew’s install
 
-  target_link_libraries(formal_structures
-    PRIVATE
-      $<$<BOOL:${TBB_TARGET}>:${TBB_TARGET}>
-      $<$<BOOL:${YAML_CPP_TARGET}>:${YAML_CPP_TARGET}>
-      $<$<BOOL:${SPDLOG_TARGET}>:${SPDLOG_TARGET}>
-  )
-else()
-  message(WARNING "formal_structures target was not defined by subdirectories; skipping top-level link/include setup.")
-endif()
+target_include_directories(formal_structures
+  PRIVATE
+    ${TBB_INCLUDE_DIRS}          # if defined by find_package
+    /opt/homebrew/include        # fallback for tbb headers
+)
+target_link_libraries(formal_structures
+  PRIVATE TBB::tbb
+)

From 80286376e7dcf5cc4e4a509d17115d64aaa2f2a3 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 01:52:47 +0100
Subject: [PATCH 27/43] test update

---
 .github/workflows/regress.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index 5b97d83a..5f55a863 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -30,7 +30,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -y pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libyaml-cpp-dev libspdlog-dev 
+      run: sudo apt-get update && sudo apt-get install -y pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libspdlog-dev 
       
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
@@ -82,7 +82,7 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal ./test_config.yaml
+        ./build/src/bin/kepler_formal --config ./test_config.yaml
     
     - name: Run on verilog edited
       working-directory: ${{github.workspace}}

From 301ddf6a52cec517abde0931ffa86a13e3f70f4b Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 01:59:09 +0100
Subject: [PATCH 28/43] update logs

---
 src/bin/KeplerFormal.cpp               | 4 ++--
 src/strategies/miter/MiterStrategy.cpp | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/bin/KeplerFormal.cpp b/src/bin/KeplerFormal.cpp
index 42e03dcd..ee94c780 100644
--- a/src/bin/KeplerFormal.cpp
+++ b/src/bin/KeplerFormal.cpp
@@ -255,9 +255,9 @@ int main(int argc, char** argv) {
   try {
     KEPLER_FORMAL::MiterStrategy MiterS(top0, top1);
     if (MiterS.run()) {
-      SPDLOG_INFO("Miter strategy succeeded: outputs are identical.");
+      SPDLOG_INFO("No difference was found.");
     } else {
-      SPDLOG_INFO("Miter strategy failed: outputs differ.");
+      SPDLOG_INFO("Difference was found. Please refer to the log(miter_log_x.txt) for details.");
     }
   } catch (const std::exception& e) {
     SPDLOG_ERROR("Workflow failed: {}", e.what());
diff --git a/src/strategies/miter/MiterStrategy.cpp b/src/strategies/miter/MiterStrategy.cpp
index cf65a83c..c04dfff0 100644
--- a/src/strategies/miter/MiterStrategy.cpp
+++ b/src/strategies/miter/MiterStrategy.cpp
@@ -480,7 +480,7 @@ bool MiterStrategy::run() {
   logger->info("Finished Glucose solving: {}", sat ? "SAT" : "UNSAT");
 
   if (sat) {
-    logger->warn("Miter failed: analyzing individual POs");
+    logger->warn("Miter found a difference -> moving to analyze individual POs");
     for (size_t i = 0; i < POs0.size(); ++i) {
       if (builder0.getOutputs2OutputsIDs().at(builder0.getDNLIDforOutput(i)) !=
           builder1.getOutputs2OutputsIDs().at(builder1.getDNLIDforOutput(i))) {
@@ -503,7 +503,7 @@ bool MiterStrategy::run() {
       singleSolver.addClause(singleRootLit);
       if (singleSolver.solve()) {
         failedPOs_.push_back(i);
-        logger->info("Check failed for PO: {}", i);
+        logger->info("Found difference for PO: {}", i);
         // logger->info("Clause 0 {}", POs0[i]->toString());
         // logger->info("Clause 1 {}", POs1[i]->toString());
         std::vector<naja::NL::SNLDesign*> topModels;

From fe0dd45e006986bd21f6fcd0520bc00915f385f3 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 02:06:36 +0100
Subject: [PATCH 29/43] Update README.md

---
 README.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/README.md b/README.md
index 0fa4406d..bb351c79 100644
--- a/README.md
+++ b/README.md
@@ -56,7 +56,10 @@ make
 ## Usage
 
 ```bash
+# Classic 
 "build/src/bin/kepler_formal <-verilog/-naja_if> <netlist1> <netlist2> [<liberty-file>...]"
+# Through yaml config file
+build/src/bin/kepler_formal --config <yaml file>
 ```
 
 ## Example 

From 075dd2c50a0c523d321015e85fbfc9b1c713bf90 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 02:13:07 +0100
Subject: [PATCH 30/43] Update README with config file usage for kepler_formal

Added command to run kepler_formal with a config file.
---
 example/README.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/example/README.md b/example/README.md
index 38171804..5a4ce868 100644
--- a/example/README.md
+++ b/example/README.md
@@ -9,5 +9,7 @@ python edit.py
 # For naja_if
 ../build/src/bin/kepler_formal -naja_if tinyrocket_naja.if tinyrocket_naja_edited.if NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib fakeram45_64x32.lib
 # For verilog
-../build/src/bin/kepler_formal -verilog tinyrocket_pre_edited.v tinyrocket_edited.v NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib /example/fakeram45_64x32.lib 
+../build/src/bin/kepler_formal -verilog tinyrocket_pre_edited.v tinyrocket_edited.v NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib /example/fakeram45_64x32.lib
+# Through config file
+../build/src/bin/kepler_formal --config test_config.yaml 
 ```

From b04716a476b089911769005a9cca9ba4c776795f Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 02:26:08 +0100
Subject: [PATCH 31/43] Update README.md

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index bb351c79..f33469ea 100644
--- a/README.md
+++ b/README.md
@@ -59,7 +59,7 @@ make
 # Classic 
 "build/src/bin/kepler_formal <-verilog/-naja_if> <netlist1> <netlist2> [<liberty-file>...]"
 # Through yaml config file
-build/src/bin/kepler_formal --config <yaml file>
+"build/src/bin/kepler_formal --config <yaml file>"
 ```
 
 ## Example 

From 46a3b1c7f89a8121c69e9bc2e1d49fe8d11bf870 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 10:37:11 +0100
Subject: [PATCH 32/43] Update regress.yml

---
 .github/workflows/regress.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index 5f55a863..e6dbeb00 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -82,7 +82,7 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal --config ./test_config.yaml
+        ./build/src/bin/kepler_formal --config ./example/test_config.yaml
     
     - name: Run on verilog edited
       working-directory: ${{github.workspace}}

From fe4a98e61c4cf4b1918969cc689710138b755cf4 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 10:42:05 +0100
Subject: [PATCH 33/43] regress update

---
 .github/workflows/regress.yml                         |  9 ++-------
 .../{test_config.yaml => test_config_naja_if.yaml}    |  0
 example/test_config_verilog.yaml                      | 11 +++++++++++
 3 files changed, 13 insertions(+), 7 deletions(-)
 rename example/{test_config.yaml => test_config_naja_if.yaml} (100%)
 create mode 100644 example/test_config_verilog.yaml

diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index 5f55a863..10a8f5a7 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -82,19 +82,14 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal --config ./test_config.yaml
+        ./build/src/bin/kepler_formal --config ./test_config_naja_if.yaml
     
     - name: Run on verilog edited
       working-directory: ${{github.workspace}}
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal -verilog \
-          ./example/tinyrocket.v \
-          ./example/tinyrocket_edited.v \
-          ./example/NangateOpenCellLibrary_typical.lib \
-          ./example/fakeram45_1024x32.lib \
-          ./example/fakeram45_64x32.lib 
+        ./build/src/bin/kepler_formal --config ./test_config_verilog.yaml
 
 
 
diff --git a/example/test_config.yaml b/example/test_config_naja_if.yaml
similarity index 100%
rename from example/test_config.yaml
rename to example/test_config_naja_if.yaml
diff --git a/example/test_config_verilog.yaml b/example/test_config_verilog.yaml
new file mode 100644
index 00000000..44877c1d
--- /dev/null
+++ b/example/test_config_verilog.yaml
@@ -0,0 +1,11 @@
+# tinyrocket_config.yaml
+format: verilog
+input_paths:
+  - tinyrocket.v
+  - tinyrocket_edited.v
+liberty_files:
+  - NangateOpenCellLibrary_typical.lib
+  - fakeram45_1024x32.lib
+  - fakeram45_64x32.lib
+log_level: info
+

From 6b16bf12bc2729402ca9f0a41525c8fcd46bd447 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 10:47:29 +0100
Subject: [PATCH 34/43] wf update

---
 .github/workflows/macOS.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/macOS.yml b/.github/workflows/macOS.yml
index f79d4d34..0b72912f 100644
--- a/.github/workflows/macOS.yml
+++ b/.github/workflows/macOS.yml
@@ -27,7 +27,7 @@ jobs:
       run: git submodule update --init --recursive
     # install dependencies
     - name: Install dependencies
-      run: brew install cmake doxygen capnp tbb bison flex boost yaml-cpp spdlog
+      run: brew install cmake doxygen capnp tbb bison flex boost spdlog
     - name: set env variable
       run: |
         echo "/usr/local/opt/flex/bin" >> $GITHUB_PATH; echo "/usr/local/opt/bison/bin" >> $GITHUB_PATH;

From e5c79708c7b93da78b77c69db7419a4c4e72101b Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 11:00:58 +0100
Subject: [PATCH 35/43] wf update

---
 .github/workflows/regress.yml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index d30cea18..7502236e 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -78,18 +78,18 @@ jobs:
       run: python edit.py
 
     - name: Run on naja if edited
-      working-directory: ${{github.workspace}}
+      working-directory: ${{github.workspace}}/example
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal --config ./example/test_config_naja_if.yaml
+        ./build/src/bin/kepler_formal --config test_config_naja_if.yaml
     
     - name: Run on verilog edited
-      working-directory: ${{github.workspace}}
+      working-directory: ${{github.workspace}}/example
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal --config ./example/test_config_verilog.yaml
+        ./build/src/bin/kepler_formal --config test_config_verilog.yaml
 
 
 

From bd787598f2be4d849113f7d70d80a457eea4c739 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 11:21:16 +0100
Subject: [PATCH 36/43] fix wf + const ref

---
 .github/workflows/regress.yml |  4 ++--
 src/formal/BoolExpr.cpp       | 41 +++++++++++++++++++----------------
 src/formal/BoolExpr.h         | 20 ++++++++---------
 src/formal/BoolExprCache.cpp  |  4 ++--
 src/formal/BoolExprCache.h    |  4 ++--
 5 files changed, 38 insertions(+), 35 deletions(-)

diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index 7502236e..249d7ece 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -82,14 +82,14 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal --config test_config_naja_if.yaml
+        ../build/src/bin/kepler_formal --config test_config_naja_if.yaml
     
     - name: Run on verilog edited
       working-directory: ${{github.workspace}}/example
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal --config test_config_verilog.yaml
+        ../build/src/bin/kepler_formal --config test_config_verilog.yaml
 
 
 
diff --git a/src/formal/BoolExpr.cpp b/src/formal/BoolExpr.cpp
index 31c0adde..b484422d 100644
--- a/src/formal/BoolExpr.cpp
+++ b/src/formal/BoolExpr.cpp
@@ -16,8 +16,8 @@ tbb::concurrent_unordered_map<BoolExprCache::Key,
 
 /// Private ctor
 BoolExpr::BoolExpr(Op op, size_t id,
-                   std::shared_ptr<BoolExpr> a,
-                   std::shared_ptr<BoolExpr> b)
+                   const std::shared_ptr<BoolExpr>& a,
+                   const std::shared_ptr<BoolExpr>& b)
   : op_(op), varID_(id)/*, left_(l) , right_(r)*/ {
     if (b == nullptr) {
         if (a == nullptr && op != Op::VAR) {
@@ -66,7 +66,7 @@ std::shared_ptr<BoolExpr> BoolExpr::Var(size_t id) {
     return createNode(k);
 }
 
-std::shared_ptr<BoolExpr> BoolExpr::Not(std::shared_ptr<BoolExpr> a) {
+std::shared_ptr<BoolExpr> BoolExpr::Not(const std::shared_ptr<BoolExpr>& a) {
     // constant-fold
     if (a->op_ == Op::VAR && a->varID_ < 2)
         return Var(1 - a->varID_);
@@ -78,8 +78,8 @@ std::shared_ptr<BoolExpr> BoolExpr::Not(std::shared_ptr<BoolExpr> a) {
 }
 
 std::shared_ptr<BoolExpr> BoolExpr::And(
-    std::shared_ptr<BoolExpr> a,
-    std::shared_ptr<BoolExpr> b)
+    const std::shared_ptr<BoolExpr>& a,
+    const std::shared_ptr<BoolExpr>& b)
 {
     // constant-fold
     if ((a->op_ == Op::VAR && a->varID_ == 0) ||
@@ -92,14 +92,15 @@ std::shared_ptr<BoolExpr> BoolExpr::And(
     if (b->op_==Op::NOT && b->left_==a) return Var(0);
 
     // canonical order
-    if (b < a) std::swap(a, b);
-    BoolExprCache::Key k{Op::AND, 0, a, b};
+    // if (b < a) std::swap(a, b);
+    // BoolExprCache::Key k{Op::AND, 0, a, b};
+    BoolExprCache::Key k{Op::AND, 0, (b < a) ? a : b, (b < a) ? b : a};
     return createNode(k);
 }
 
 std::shared_ptr<BoolExpr> BoolExpr::Or(
-    std::shared_ptr<BoolExpr> a,
-    std::shared_ptr<BoolExpr> b)
+    const std::shared_ptr<BoolExpr>& a,
+    const std::shared_ptr<BoolExpr>& b)
 {
     if ((a->op_ == Op::VAR && a->varID_ == 1) ||
         (b->op_ == Op::VAR && b->varID_ == 1))
@@ -110,14 +111,15 @@ std::shared_ptr<BoolExpr> BoolExpr::Or(
     if (a->op_==Op::NOT && a->left_==b) return Var(1);
     if (b->op_==Op::NOT && b->left_==a) return Var(1);
 
-    if (b < a) std::swap(a, b);
-    BoolExprCache::Key k{Op::OR, 0, a, b};
+    // if (b < a) std::swap(a, b);
+    // BoolExprCache::Key k{Op::OR, 0, a, b};
+    BoolExprCache::Key k{Op::OR, 0, (b < a) ? a : b, (b < a) ? b : a};
     return createNode(k);
 }
 
 std::shared_ptr<BoolExpr> BoolExpr::Xor(
-    std::shared_ptr<BoolExpr> a,
-    std::shared_ptr<BoolExpr> b)
+    const std::shared_ptr<BoolExpr>& a,
+    const std::shared_ptr<BoolExpr>& b)
 {
     if (a->op_ == Op::VAR && a->varID_ == 0)     return b;
     if (b->op_ == Op::VAR && b->varID_ == 0)     return a;
@@ -125,8 +127,9 @@ std::shared_ptr<BoolExpr> BoolExpr::Xor(
     if (b->op_ == Op::VAR && b->varID_ == 1)     return Not(a);
     if (a == b)                  return Var(0);
 
-    if (b < a) std::swap(a, b);
-    BoolExprCache::Key k{Op::XOR, 0, a, b};
+    // if (b < a) std::swap(a, b);
+    // BoolExprCache::Key k{Op::XOR, 0, a, b};
+    BoolExprCache::Key k{Op::XOR, 0, (b < a) ? a : b, (b < a) ? b : a};
     return createNode(k);
 }
 
@@ -184,14 +187,14 @@ std::string BoolExpr::OpToString(Op op) {
 
 // replace previous isConstFalse/isConstTrue and Simplify implementation with this:
 
-static inline bool isConstFalse(std::shared_ptr<BoolExpr> e) {
+static inline bool isConstFalse(const std::shared_ptr<BoolExpr>& e) {
     return e->getOp() == Op::VAR && e->getId() == 0;
 }
-static inline bool isConstTrue(std::shared_ptr<BoolExpr> e) {
+static inline bool isConstTrue(const std::shared_ptr<BoolExpr>& e) {
     return e->getOp() == Op::VAR && e->getId() == 1;
 }
 
-std::shared_ptr<BoolExpr> BoolExpr::simplify(std::shared_ptr<BoolExpr> e) {
+std::shared_ptr<BoolExpr> BoolExpr::simplify(const std::shared_ptr<BoolExpr>& e) {
     if (!e) return nullptr;
     if (e->getOp() == Op::VAR) return e;
 
@@ -215,7 +218,7 @@ std::shared_ptr<BoolExpr> BoolExpr::simplify(std::shared_ptr<BoolExpr> e) {
         }
     }
 
-    for (std::shared_ptr<BoolExpr> node : order) {
+    for (const std::shared_ptr<BoolExpr>& node : order) {
         switch (node->getOp()) {
         case Op::NOT: {
             std::shared_ptr<BoolExpr> a = memo.count(node->getLeft()) ? memo[node->getLeft()] : node->getLeft();
diff --git a/src/formal/BoolExpr.h b/src/formal/BoolExpr.h
index e01ddd0e..67dfd86a 100644
--- a/src/formal/BoolExpr.h
+++ b/src/formal/BoolExpr.h
@@ -28,13 +28,13 @@ class BoolExpr : public std::enable_shared_from_this<BoolExpr> {
 
   // Factory methods (canonical, fold constants, share structure)
   static std::shared_ptr<BoolExpr> Var(size_t id);
-  static std::shared_ptr<BoolExpr> Not(std::shared_ptr<BoolExpr> a);
-  static std::shared_ptr<BoolExpr> And(std::shared_ptr<BoolExpr> a,
-                                       std::shared_ptr<BoolExpr> b);
-  static std::shared_ptr<BoolExpr> Or(std::shared_ptr<BoolExpr> a,
-                                      std::shared_ptr<BoolExpr> b);
-  static std::shared_ptr<BoolExpr> Xor(std::shared_ptr<BoolExpr> a,
-                                       std::shared_ptr<BoolExpr> b);
+  static std::shared_ptr<BoolExpr> Not(const std::shared_ptr<BoolExpr>& a);
+  static std::shared_ptr<BoolExpr> And(const std::shared_ptr<BoolExpr>& a,
+                                       const std::shared_ptr<BoolExpr>& b);
+  static std::shared_ptr<BoolExpr> Or(const std::shared_ptr<BoolExpr>& a,
+                                      const std::shared_ptr<BoolExpr>& b);
+  static std::shared_ptr<BoolExpr> Xor(const std::shared_ptr<BoolExpr>& a,
+                                       const std::shared_ptr<BoolExpr>& b);
 
   // Print and stringify
   void Print(std::ostream& out) const;
@@ -83,14 +83,14 @@ class BoolExpr : public std::enable_shared_from_this<BoolExpr> {
   }
   // Simplify/optimize an expression DAG (returns interned canonical node)
   // Memoized, safe on DAGs.
-  static std::shared_ptr<BoolExpr> simplify(std::shared_ptr<BoolExpr> e);
+  static std::shared_ptr<BoolExpr> simplify(const std::shared_ptr<BoolExpr>& e);
 
  private:
   // Private ctor: use factory methods
   BoolExpr(Op op,
            size_t id,
-           std::shared_ptr<BoolExpr> a,
-           std::shared_ptr<BoolExpr> b);
+           const std::shared_ptr<BoolExpr>& a,
+           const std::shared_ptr<BoolExpr>& b);
 
   Op op_ = Op::NONE;
   size_t varID_ = (size_t)-1;  // only for VAR
diff --git a/src/formal/BoolExprCache.cpp b/src/formal/BoolExprCache.cpp
index e22abe26..c4407e48 100644
--- a/src/formal/BoolExprCache.cpp
+++ b/src/formal/BoolExprCache.cpp
@@ -66,8 +66,8 @@ BoolExprCache::Impl& BoolExprCache::impl() {
 
 static inline TupleKey make_tuple_key(Op op,
                                       size_t varId,
-                                      std::shared_ptr<BoolExpr> lptr,
-                                      std::shared_ptr<BoolExpr> rptr) noexcept {
+                                      const std::shared_ptr<BoolExpr>& lptr,
+                                      const std::shared_ptr<BoolExpr>& rptr) noexcept {
   // use pointer identity as integer; nullptr -> 0
   auto lid = reinterpret_cast<uint64_t>(lptr.get());
   auto rid = reinterpret_cast<uint64_t>(rptr.get());
diff --git a/src/formal/BoolExprCache.h b/src/formal/BoolExprCache.h
index 4cbf6d5d..f44408c5 100644
--- a/src/formal/BoolExprCache.h
+++ b/src/formal/BoolExprCache.h
@@ -18,9 +18,9 @@ enum class Op { VAR, AND, OR, NOT, XOR, NONE };
 struct BoolExprCacheKey {
   Op op;
   size_t varId;
-  std::shared_ptr<BoolExpr>
+  const std::shared_ptr<BoolExpr>&
       l;  // raw pointer — not owning; use index/ptr identity for the key
-  std::shared_ptr<BoolExpr> r;  // raw pointer
+  const std::shared_ptr<BoolExpr>& r;  // raw pointer
 };
 
 class BoolExprCache {

From 399526d81fa378c8dcba7da6e10c915917b3ecc0 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 11:43:35 +0100
Subject: [PATCH 37/43] sync (#27)

* yaml support (#25)

* yaml support

* update testing

* update testing

* yaml dep

* spdlog dep

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* test update

* update logs

* Update README.md

* Update README with config file usage for kepler_formal

Added command to run kepler_formal with a config file.

* Update README.md

* Update regress.yml

* regress update

* wf update

* wf update

* fix wf + const ref

* Update README.md
---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index f33469ea..2529825a 100644
--- a/README.md
+++ b/README.md
@@ -28,13 +28,13 @@ The property of stable indices is employed to localize the scopes affected by ed
 On Ubuntu:
 
 ```bash
-sudo apt-get install g++ libboost-dev python3.9-dev capnproto libcapnp-dev libtbb-dev pkg-config bison flex doxygen
+sudo apt-get install g++ libboost-dev python3.9-dev capnproto libcapnp-dev libtbb-dev pkg-config bison flex doxygen libspdlog-dev 
 ```
 
 On macOS, using [Homebrew](https://brew.sh/):
 
 ```bash
-brew install cmake doxygen capnp tbb bison flex boost
+brew install cmake doxygen capnp tbb bison flex boost spdlog
 ```
 
 Ensure the versions of `bison` and `flex` installed via Homebrew take precedence over the macOS defaults by modifying your $PATH environment variable as follows:

From 5c06eb796c6581078e6b110f4739d851c3d9a87d Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 30 Nov 2025 11:43:52 +0100
Subject: [PATCH 38/43] ct

---
 src/clauses/Tree2BoolExpr.cpp | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/clauses/Tree2BoolExpr.cpp b/src/clauses/Tree2BoolExpr.cpp
index 881c0265..0cf8f187 100644
--- a/src/clauses/Tree2BoolExpr.cpp
+++ b/src/clauses/Tree2BoolExpr.cpp
@@ -58,7 +58,7 @@ void clearTermsETS() {
   termsLocal.second = 0;
 }
 
-void pushBackTermsETS(std::shared_ptr<BoolExpr> term) {
+void pushBackTermsETS(const std::shared_ptr<BoolExpr>& term) {
   auto& termsLocal = getTErmsETS();
   auto& vec = termsLocal.first;
   auto& sz = termsLocal.second;
@@ -205,7 +205,7 @@ void clearMemoETS() {
   memoLocal.second = 0;
 }
 
-void pushBackMemoETS(std::shared_ptr<BoolExpr> expr) {
+void pushBackMemoETS(const std::shared_ptr<BoolExpr>& expr) {
   auto& memoLocal = getMemoETS();
   auto& vec = memoLocal.first;
   auto& sz = memoLocal.second;
@@ -232,7 +232,7 @@ void reserveMemoETS(size_t n) {
   vec.assign(n, nullptr);
 }
 
-void setMemoETS(size_t i, std::shared_ptr<BoolExpr> expr) {
+void setMemoETS(size_t i, const std::shared_ptr<BoolExpr>& expr) {
   auto& memoLocal = getMemoETS();
   if (i >= memoLocal.second) {
     assert(false && "setMemoETS: index out of range");
@@ -240,7 +240,7 @@ void setMemoETS(size_t i, std::shared_ptr<BoolExpr> expr) {
   memoLocal.first[i] = expr;
 }
 
-std::shared_ptr<BoolExpr> getMemoETS(size_t i) {
+const std::shared_ptr<BoolExpr>& getMemoETS(size_t i) {
   auto& memoLocal = getMemoETS();
   if (i >= memoLocal.second) {
     assert(false && "getMemoETS: index out of range");
@@ -288,7 +288,7 @@ void clearChildFETS() {
   childLocal.second = 0;
 }
 
-void pushBackChildFETS(std::shared_ptr<BoolExpr> expr) {
+void pushBackChildFETS(const std::shared_ptr<BoolExpr>& expr) {
   auto& childLocal = getChildFETS();
   auto& vec = childLocal.first;
   auto& sz = childLocal.second;
@@ -315,7 +315,7 @@ void reserveChildFETS(size_t n) {
   vec.assign(n, nullptr);
 }
 
-std::shared_ptr<BoolExpr> getChildFETS(size_t i) {
+const std::shared_ptr<BoolExpr>& getChildFETS(size_t i) {
   auto& childLocal = getChildFETS();
   if (i >= childLocal.second) {
     assert(false && "getChildFETS: index out of range");
@@ -323,7 +323,7 @@ std::shared_ptr<BoolExpr> getChildFETS(size_t i) {
   return childLocal.first[i];
 }
 
-void setChildFETS(size_t i, std::shared_ptr<BoolExpr> expr) {
+void setChildFETS(size_t i, const std::shared_ptr<BoolExpr>& expr) {
   auto& childLocal = getChildFETS();
   if (i >= childLocal.second) {
     assert(false && "setChildFETS: index out of range");

From d5108aefc03bfb7df4afd3dc3cbd16494c75ebe3 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Fri, 5 Dec 2025 18:10:02 +0100
Subject: [PATCH 39/43] sync (#29)

* ct (#28)

* yaml support

* update testing

* update testing

* yaml dep

* spdlog dep

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* test update

* update logs

* Update README.md

* Update README with config file usage for kepler_formal

Added command to run kepler_formal with a config file.

* Update README.md

* Update regress.yml

* regress update

* wf update

* wf update

* fix wf + const ref

* sync (#27)

* yaml support (#25)

* yaml support

* update testing

* update testing

* yaml dep

* spdlog dep

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* test update

* update logs

* Update README.md

* Update README with config file usage for kepler_formal

Added command to run kepler_formal with a config file.

* Update README.md

* Update regress.yml

* regress update

* wf update

* wf update

* fix wf + const ref

* Update README.md

* ct

* Update README.md

* tests under option

---------

Co-authored-by: xtof <christophe.alexandre@keplertech.io>
---
 CMakeLists.txt | 8 ++++++--
 README.md      | 9 ++++++++-
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 68dbc8f2..61654d1e 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -23,8 +23,12 @@ set(CMAKE_CXX_STANDARD 20 CACHE STRING "C++ standard" FORCE)
 
 add_subdirectory(src)
 add_subdirectory(thirdparty)
-include(CTest)
-add_subdirectory(test)
+
+option(ENABLE_UNIT_TESTS ON)
+if(ENABLE_UNIT_TESTS)
+  include(CTest)
+  add_subdirectory(test)
+endif()
 
 find_package(TBB REQUIRED)
 
diff --git a/README.md b/README.md
index 2529825a..375394f0 100644
--- a/README.md
+++ b/README.md
@@ -49,10 +49,17 @@ git clone --recurse-submodules https://github.com/keplertech/kepler-formal.git
 cd kepler-formal
 mkdir build
 cd build
-cmake ..
+cmake .. 
 make
 ```
 
+```bash
+# For optimized performance use: 
+cmake .. -DCMAKE_BUILD_TYPE=Release \
+  -DCMAKE_CXX_FLAGS_RELEASE="-Ofast -march=native \
+  -ffast-math -flto" -DCMAKE_EXE_LINKER_FLAGS="-flto"
+```
+
 ## Usage
 
 ```bash

From b96bfcd43ec6ee35a303b3c0b2b64df3c6c85fb6 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Fri, 5 Dec 2025 18:11:27 +0100
Subject: [PATCH 40/43] prints

---
 src/strategies/miter/BuildPrimaryOutputClauses.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/strategies/miter/BuildPrimaryOutputClauses.cpp b/src/strategies/miter/BuildPrimaryOutputClauses.cpp
index 4ac3fff4..2cfa0b4b 100644
--- a/src/strategies/miter/BuildPrimaryOutputClauses.cpp
+++ b/src/strategies/miter/BuildPrimaryOutputClauses.cpp
@@ -395,7 +395,7 @@ void BuildPrimaryOutputClauses::build() {
   tbb::task_arena arena(40);
   auto processOutput = [&](size_t i) {
     DNLID out = outputs_[i];
-    printf("Procssing output %zu/%zu: %s\n", ++processedOutputs,
+    DEBUG_LOG("Procssing output %zu/%zu: %s\n", ++processedOutputs,
            outputs_.size(),
            get()
                ->getDNLTerminalFromID(out)

From 7899ca6bb0db4f81852193a05933de5e66d89b04 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Fri, 5 Dec 2025 18:15:13 +0100
Subject: [PATCH 41/43] remove prints

---
 src/strategies/miter/BuildPrimaryOutputClauses.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/strategies/miter/BuildPrimaryOutputClauses.cpp b/src/strategies/miter/BuildPrimaryOutputClauses.cpp
index 2cfa0b4b..661a9e1c 100644
--- a/src/strategies/miter/BuildPrimaryOutputClauses.cpp
+++ b/src/strategies/miter/BuildPrimaryOutputClauses.cpp
@@ -360,7 +360,7 @@ void BuildPrimaryOutputClauses::collect() {
     KeyT key{ path, std::move(ids) };
     outputsMap_[std::move(key)]  =
             output;
-    printf("Output collected: %s\n", naja::DNL::get()
+    DEBUG_LOG("Output collected: %s\n", naja::DNL::get()
                                          ->getDNLTerminalFromID(output)
                                          .getSnlBitTerm()
                                          ->getName()

From 43ed29b5fe2734a0f23fde729b0850bab099a711 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Fri, 5 Dec 2025 18:15:59 +0100
Subject: [PATCH 42/43] sync (#30)

* ct (#28)

* yaml support

* update testing

* update testing

* yaml dep

* spdlog dep

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* test update

* update logs

* Update README.md

* Update README with config file usage for kepler_formal

Added command to run kepler_formal with a config file.

* Update README.md

* Update regress.yml

* regress update

* wf update

* wf update

* fix wf + const ref

* sync (#27)

* yaml support (#25)

* yaml support

* update testing

* update testing

* yaml dep

* spdlog dep

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* test update

* update logs

* Update README.md

* Update README with config file usage for kepler_formal

Added command to run kepler_formal with a config file.

* Update README.md

* Update regress.yml

* regress update

* wf update

* wf update

* fix wf + const ref

* Update README.md

* ct

* Update README.md

* tests under option

---------

Co-authored-by: xtof <christophe.alexandre@keplertech.io>

From 9153707101164c8e260559219269597062267e88 Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Sun, 21 Dec 2025 14:21:56 +0100
Subject: [PATCH 43/43] sync (#33)

* clean debug prints (#32)

* yaml support

* update testing

* update testing

* yaml dep

* spdlog dep

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* test update

* update logs

* Update README.md

* Update README with config file usage for kepler_formal

Added command to run kepler_formal with a config file.

* Update README.md

* Update regress.yml

* regress update

* wf update

* wf update

* fix wf + const ref

* sync (#27)

* yaml support (#25)

* yaml support

* update testing

* update testing

* yaml dep

* spdlog dep

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* test update

* update logs

* Update README.md

* Update README with config file usage for kepler_formal

Added command to run kepler_formal with a config file.

* Update README.md

* Update regress.yml

* regress update

* wf update

* wf update

* fix wf + const ref

* Update README.md

* ct

* sync (#29)

* ct (#28)

* yaml support

* update testing

* update testing

* yaml dep

* spdlog dep

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* test update

* update logs

* Update README.md

* Update README with config file usage for kepler_formal

Added command to run kepler_formal with a config file.

* Update README.md

* Update regress.yml

* regress update

* wf update

* wf update

* fix wf + const ref

* sync (#27)

* yaml support (#25)

* yaml support

* update testing

* update testing

* yaml dep

* spdlog dep

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* test update

* update logs

* Update README.md

* Update README with config file usage for kepler_formal

Added command to run kepler_formal with a config file.

* Update README.md

* Update regress.yml

* regress update

* wf update

* wf update

* fix wf + const ref

* Update README.md

* ct

* Update README.md

* tests under option

---------

Co-authored-by: xtof <christophe.alexandre@keplertech.io>

* prints

* remove prints

* sync (#30)

* ct (#28)

* yaml support

* update testing

* update testing

* yaml dep

* spdlog dep

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* test update

* update logs

* Update README.md

* Update README with config file usage for kepler_formal

Added command to run kepler_formal with a config file.

* Update README.md

* Update regress.yml

* regress update

* wf update

* wf update

* fix wf + const ref

* sync (#27)

* yaml support (#25)

* yaml support

* update testing

* update testing

* yaml dep

* spdlog dep

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* test update

* update logs

* Update README.md

* Update README with config file usage for kepler_formal

Added command to run kepler_formal with a config file.

* Update README.md

* Update regress.yml

* regress update

* wf update

* wf update

* fix wf + const ref

* Update README.md

* ct

* Update README.md

* tests under option

---------

Co-authored-by: xtof <christophe.alexandre@keplertech.io>

---------

Co-authored-by: xtof <christophe.alexandre@keplertech.io>

* ignore with warning unparallel observation points

* Update regress.yml

* Update README.md

* Fix typos in README for kepler-formal commands

* logfile command

* update naja for gz liberty parser

---------

Co-authored-by: xtof <christophe.alexandre@keplertech.io>
---
 .github/workflows/c-cpp.yml            |  2 +-
 .github/workflows/macOS.yml            |  2 +-
 .github/workflows/regress.yml          | 10 ++--
 README.md                              |  4 +-
 example/README.md                      |  8 +--
 src/bin/CMakeLists.txt                 | 10 ++--
 src/bin/KeplerFormal.cpp               | 10 +++-
 src/strategies/miter/MiterStrategy.cpp | 74 +++++++++++++++++++++++++-
 src/strategies/miter/MiterStrategy.h   | 10 ++--
 thirdparty/naja                        |  2 +-
 10 files changed, 103 insertions(+), 29 deletions(-)

diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml
index f9d60434..710738d9 100644
--- a/.github/workflows/c-cpp.yml
+++ b/.github/workflows/c-cpp.yml
@@ -30,7 +30,7 @@ jobs:
         sudo apt-get install -yq \
           build-essential cmake ninja-build clang pkg-config \
           libboost-dev libfl-dev libtbb-dev capnproto libcapnp-dev \
-          libgtest-dev libspdlog-dev libfmt-dev
+          libgtest-dev libspdlog-dev libfmt-dev libboost-iostreams-dev zlib1g-dev
 
     - name: Configure CMake
       working-directory: ${{github.workspace}}/
diff --git a/.github/workflows/macOS.yml b/.github/workflows/macOS.yml
index 0b72912f..2fdc1c70 100644
--- a/.github/workflows/macOS.yml
+++ b/.github/workflows/macOS.yml
@@ -27,7 +27,7 @@ jobs:
       run: git submodule update --init --recursive
     # install dependencies
     - name: Install dependencies
-      run: brew install cmake doxygen capnp tbb bison flex boost spdlog
+      run: brew install cmake doxygen capnp tbb bison flex boost spdlog zlib
     - name: set env variable
       run: |
         echo "/usr/local/opt/flex/bin" >> $GITHUB_PATH; echo "/usr/local/opt/bison/bin" >> $GITHUB_PATH;
diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml
index 249d7ece..5ac73660 100644
--- a/.github/workflows/regress.yml
+++ b/.github/workflows/regress.yml
@@ -30,7 +30,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -y pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libspdlog-dev 
+      run: sudo apt-get update && sudo apt-get install -y pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libspdlog-dev libboost-iostreams-dev zlib1g-dev
       
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
@@ -51,7 +51,7 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal -naja_if \
+        ./build/src/bin/kepler-formal -naja_if \
           ./example/tinyrocket_naja.if \
           ./example/tinyrocket_naja.if \
           ./example/NangateOpenCellLibrary_typical.lib \
@@ -63,7 +63,7 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal -verilog \
+        ./build/src/bin/kepler-formal -verilog \
           ./example/tinyrocket.v \
           ./example/tinyrocket.v \
           ./example/NangateOpenCellLibrary_typical.lib \
@@ -82,14 +82,14 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ../build/src/bin/kepler_formal --config test_config_naja_if.yaml
+        ../build/src/bin/kepler-formal --config test_config_naja_if.yaml
     
     - name: Run on verilog edited
       working-directory: ${{github.workspace}}/example
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ../build/src/bin/kepler_formal --config test_config_verilog.yaml
+        ../build/src/bin/kepler-formal --config test_config_verilog.yaml
 
 
 
diff --git a/README.md b/README.md
index 375394f0..b1c0ea75 100644
--- a/README.md
+++ b/README.md
@@ -64,9 +64,9 @@ cmake .. -DCMAKE_BUILD_TYPE=Release \
 
 ```bash
 # Classic 
-"build/src/bin/kepler_formal <-verilog/-naja_if> <netlist1> <netlist2> [<liberty-file>...]"
+"build/src/bin/kepler-formal <-verilog/-naja_if> <netlist1> <netlist2> [<liberty-file>...]"
 # Through yaml config file
-"build/src/bin/kepler_formal --config <yaml file>"
+"build/src/bin/kepler-formal --config <yaml file>"
 ```
 
 ## Example 
diff --git a/example/README.md b/example/README.md
index da3868c5..a743b650 100644
--- a/example/README.md
+++ b/example/README.md
@@ -7,10 +7,10 @@ cd example
 pip install najaeda
 python edit.py
 # For naja_if
-../build/src/bin/kepler_formal -naja_if tinyrocket_naja.if tinyrocket_naja_edited.if NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib fakeram45_64x32.lib
+../build/src/bin/kepler-formal -naja_if tinyrocket_naja.if tinyrocket_naja_edited.if NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib fakeram45_64x32.lib
 # For verilog
-../build/src/bin/kepler_formal -verilog tinyrocket_pre_edited.v tinyrocket_edited.v NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib /example/fakeram45_64x32.lib
+../build/src/bin/kepler-formal -verilog tinyrocket_pre_edited.v tinyrocket_edited.v NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib /example/fakeram45_64x32.lib
 # Through config file
-../build/src/bin/kepler_formal --config test_config_naja_if.yaml
-../build/src/bin/kepler_formal --config test_config_verilog.yaml 
+../build/src/bin/kepler-formal --config test_config_naja_if.yaml
+../build/src/bin/kepler-formal --config test_config_verilog.yaml 
 ```
diff --git a/src/bin/CMakeLists.txt b/src/bin/CMakeLists.txt
index bf576969..df030f2b 100644
--- a/src/bin/CMakeLists.txt
+++ b/src/bin/CMakeLists.txt
@@ -1,11 +1,11 @@
 # Copyright 2024-2025 keplertech.io
 # SPDX-License-Identifier: GPL-3.0-only
 
-add_executable(kepler_formal KeplerFormal.cpp)
-target_include_directories(kepler_formal SYSTEM BEFORE PUBLIC ${Boost_INCLUDE_DIR})
-target_include_directories(kepler_formal PUBLIC ${ARGPARSE_DIR})
+add_executable(kepler-formal KeplerFormal.cpp)
+target_include_directories(kepler-formal SYSTEM BEFORE PUBLIC ${Boost_INCLUDE_DIR})
+target_include_directories(kepler-formal PUBLIC ${ARGPARSE_DIR})
 
-target_link_libraries(kepler_formal
+target_link_libraries(kepler-formal
   PRIVATE
     naja_snl_pyloader
     naja_dnl
@@ -15,5 +15,5 @@ target_link_libraries(kepler_formal
     ${SPDLOG_TARGET}
 )
 
-install(TARGETS kepler_formal DESTINATION ${CMAKE_INSTALL_BINDIR})
+install(TARGETS kepler-formal DESTINATION ${CMAKE_INSTALL_BINDIR})
 
diff --git a/src/bin/KeplerFormal.cpp b/src/bin/KeplerFormal.cpp
index ee94c780..f4e828cf 100644
--- a/src/bin/KeplerFormal.cpp
+++ b/src/bin/KeplerFormal.cpp
@@ -59,6 +59,9 @@ int main(int argc, char** argv) {
 
   // Check for config mode (--config or -c). If present, YAML takes precedence.
   bool usedConfig = false;
+
+  std::string logFileName;
+
   for (int i = 1; i < argc; ++i) {
     std::string a = argv[i];
     if (a == "--config" || a == "-c") {
@@ -94,6 +97,11 @@ int main(int argc, char** argv) {
           logLevel = cfg["log_level"].as<std::string>();
         }
 
+        // Add log file name
+        if (cfg["log_file"] && cfg["log_file"].IsScalar()) {
+          logFileName = cfg["log_file"].as<std::string>();
+        }
+
         usedConfig = true;
       } catch (const std::exception& e) {
         SPDLOG_CRITICAL("Failed to parse config {}: {}", cfgPath, e.what());
@@ -253,7 +261,7 @@ int main(int argc, char** argv) {
   // 4. Hand off to the rest of the editing/analysis workflow
   // --------------------------------------------------------------------------
   try {
-    KEPLER_FORMAL::MiterStrategy MiterS(top0, top1);
+    KEPLER_FORMAL::MiterStrategy MiterS(top0, top1, logFileName);
     if (MiterS.run()) {
       SPDLOG_INFO("No difference was found.");
     } else {
diff --git a/src/strategies/miter/MiterStrategy.cpp b/src/strategies/miter/MiterStrategy.cpp
index c04dfff0..7e0c3d44 100644
--- a/src/strategies/miter/MiterStrategy.cpp
+++ b/src/strategies/miter/MiterStrategy.cpp
@@ -34,6 +34,7 @@ using namespace KEPLER_FORMAL;
 
 SNLDesign* MiterStrategy::top0_ = nullptr;
 SNLDesign* MiterStrategy::top1_ = nullptr;
+std::string MiterStrategy::logFileName_ = "";
 namespace {
 
 static std::shared_ptr<spdlog::logger> logger;
@@ -45,6 +46,10 @@ void ensureLoggerInitialized() {
       // already exist and then crete mitter_log_(x+1).txt
       int logIndex = 0;
       while (true) {
+        if (MiterStrategy::logFileName_ != "") {
+          logIndex = -1;
+          break;
+        }
         std::string logFileName =
             "miter_log_" + std::to_string(logIndex) + ".txt";
         std::ifstream infile(logFileName);
@@ -56,6 +61,13 @@ void ensureLoggerInitialized() {
       }
       std::string logFileName =
           "miter_log_" + std::to_string(logIndex) + ".txt";
+      if (MiterStrategy::logFileName_ != "") {
+        if (!MiterStrategy::logFileName_.empty()) {
+            std::filesystem::path p(MiterStrategy::logFileName_);
+            std::filesystem::create_directories(p.parent_path());
+            logFileName = p.string();
+        }
+      }
       auto file_sink = std::make_shared<spdlog::sinks::basic_file_sink_mt>(
           logFileName, true);
       logger = std::make_shared<spdlog::logger>("miter_logger", file_sink);
@@ -225,6 +237,13 @@ Glucose::Lit tseitinEncode(
 
 }  // namespace
 
+ MiterStrategy::MiterStrategy(naja::NL::SNLDesign* top0, naja::NL::SNLDesign* top1, const std::string& logFileName, const std::string& prefix)
+      : prefix_(prefix) {
+    top0_ = top0;
+    top1_ = top1;
+    logFileName_ = logFileName;
+  }
+
 void MiterStrategy::normalizeInputs(
     std::vector<naja::DNL::DNLID>& inputs0,
     std::vector<naja::DNL::DNLID>& inputs1,
@@ -328,11 +347,25 @@ void MiterStrategy::normalizeOutputs(
   for (const auto& [path0, output0] : outputs0Map) {
     if (pathsCommon.find(path0) == pathsCommon.end()) {
       diff0.push_back(output0);
+      std::string fullName;
+      for (const auto& name : path0.first) {
+        fullName += name.getString() + ".";
+      }
+      fullName += std::to_string(path0.second[0]) + ".";
+      fullName += std::to_string(path0.second[1]);
+      logger->info("Will ignore the analysis for: {} from netlist 0 as it does not exist in netlist 1", fullName);
     }
   }
   std::vector<naja::DNL::DNLID> diff1;
   for (const auto& [path1, output1] : outputs1Map) {
     if (pathsCommon.find(path1) == pathsCommon.end()) {
+      std::string fullName;
+      for (const auto& name : path1.first) {
+        fullName += name.getString() + ".";
+      }
+      fullName += std::to_string(path1.second[0]) + ".";
+      fullName += std::to_string(path1.second[1]);
+      logger->info("Will ignore the analysis for: {} from netlist 1 as it does not exist in netlist 0", fullName);
       diff1.push_back(output1);
     }
   }
@@ -340,12 +373,12 @@ void MiterStrategy::normalizeOutputs(
   for (const auto& path : pathsCommon) {
     outputs0.push_back(outputs0Map.at(path));
   }
-  outputs0.insert(outputs0.end(), diff0.begin(), diff0.end());
+  //outputs0.insert(outputs0.end(), diff0.begin(), diff0.end());
   outputs1.clear();
   for (const auto& path : pathsCommon) {
     outputs1.push_back(outputs1Map.at(path));
   }
-  outputs1.insert(outputs1.end(), diff1.begin(), diff1.end());
+  //outputs1.insert(outputs1.end(), diff1.begin(), diff1.end());
   logger->debug("size of common outputs: {}", pathsCommon.size());
   logger->debug("size of diff0 outputs: {}", diff0.size());
   logger->debug("size of diff1 outputs: {}", diff1.size());
@@ -484,6 +517,24 @@ bool MiterStrategy::run() {
     for (size_t i = 0; i < POs0.size(); ++i) {
       if (builder0.getOutputs2OutputsIDs().at(builder0.getDNLIDforOutput(i)) !=
           builder1.getOutputs2OutputsIDs().at(builder1.getDNLIDforOutput(i))) {
+        auto path0 = builder0.getOutputs2OutputsIDs().at(builder0.getDNLIDforOutput(i));
+        auto path1 = builder1.getOutputs2OutputsIDs().at(builder1.getDNLIDforOutput(i));
+        // print path0
+        for (const auto& name : path0.first) {
+          logger->info("%s.", name.getString().c_str());
+        }
+        for (const auto& id : path0.second) {
+          logger->info("%lu.", id);
+        }
+        logger->info("\n");
+        // print path1
+        for (const auto& name : path1.first) {
+          logger->info("%s.", name.getString().c_str());
+        }
+        for (const auto& id : path1.second) {
+          logger->info("%lu.", id);
+        }
+        logger->info("\n");
         throw std::runtime_error("Miter PO index " + std::to_string(i) +
                                  " DNLIDs do not match");
       }
@@ -506,6 +557,25 @@ bool MiterStrategy::run() {
         logger->info("Found difference for PO: {}", i);
         // logger->info("Clause 0 {}", POs0[i]->toString());
         // logger->info("Clause 1 {}", POs1[i]->toString());
+        // print path of index i
+        auto path0 = builder0.getOutputs2OutputsIDs().at(builder0.getDNLIDforOutput(i));
+        std::string pathString = "";
+        for (const auto& name : path0.first) {
+          pathString += name.getString() + ".";
+        }
+        for (const auto& id : path0.second) {
+          pathString += std::to_string(id) + ".";
+        }
+        logger->info("Path of differing PO {}: {}", i, pathString);
+        auto path1 = builder1.getOutputs2OutputsIDs().at(builder1.getDNLIDforOutput(i));
+        std::string pathString1 = "";
+        for (const auto& name : path1.first) {
+          pathString1 += name.getString() + ".";
+        }
+        for (const auto& id : path1.second) {
+          pathString1 += std::to_string(id) + ".";
+        }
+        logger->info("Path of differing PO {}: {}", i, pathString1);
         std::vector<naja::NL::SNLDesign*> topModels;
         topModels.push_back(top0_);
         topModels.push_back(top1_);
diff --git a/src/strategies/miter/MiterStrategy.h b/src/strategies/miter/MiterStrategy.h
index 339044c2..4581858e 100644
--- a/src/strategies/miter/MiterStrategy.h
+++ b/src/strategies/miter/MiterStrategy.h
@@ -18,11 +18,7 @@ namespace KEPLER_FORMAL {
 
 class MiterStrategy {
  public:
-  MiterStrategy(naja::NL::SNLDesign* top0, naja::NL::SNLDesign* top1, const std::string& prefix = "")
-      : prefix_(prefix) {
-    top0_ = top0;
-    top1_ = top1;
-  }
+  MiterStrategy(naja::NL::SNLDesign* top0, naja::NL::SNLDesign* top1, const std::string& logFileName = "", const std::string& prefix = "");
 
   bool run();
 
@@ -36,12 +32,12 @@ class MiterStrategy {
                         const std::map<std::pair<std::vector<NLName>, std::vector<NLID::DesignObjectID>>, naja::DNL::DNLID>& outputs0Map,
                         const std::map<std::pair<std::vector<NLName>, std::vector<NLID::DesignObjectID>>, naja::DNL::DNLID>& outputs1Map);
   
-
+  static std::string logFileName_;
  private:
   std::shared_ptr<BoolExpr> buildMiter(
       const tbb::concurrent_vector<std::shared_ptr<BoolExpr>>& A,
       const tbb::concurrent_vector<std::shared_ptr<BoolExpr>>& B) const;
-
+  
   static naja::NL::SNLDesign* top0_;
   static naja::NL::SNLDesign* top1_;
   tbb::concurrent_vector<BoolExpr> POs0_;
diff --git a/thirdparty/naja b/thirdparty/naja
index 7093e127..ee3d489e 160000
--- a/thirdparty/naja
+++ b/thirdparty/naja
@@ -1 +1 @@
-Subproject commit 7093e127c5ead385cd0044f105c72b25eac3eca5
+Subproject commit ee3d489e8f5d9b0d3d026b73eef6c965b83bbe3a