diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt
index 6f04bb7c6..a3f46e54c 100644
--- a/src/sat/CMakeLists.txt
+++ b/src/sat/CMakeLists.txt
@@ -26,6 +26,7 @@ z3_add_component(sat
     sat_lut_finder.cpp
     sat_model_converter.cpp
     sat_mus.cpp
+    sat_npn3_finder.cpp
     sat_parallel.cpp
     sat_prob.cpp
     sat_probing.cpp
diff --git a/src/sat/sat_npn3_finder.cpp b/src/sat/sat_npn3_finder.cpp
new file mode 100644
index 000000000..dece7eeb3
Binary files /dev/null and b/src/sat/sat_npn3_finder.cpp differ
diff --git a/src/sat/sat_npn3_finder.h b/src/sat/sat_npn3_finder.h
new file mode 100644
index 000000000..7ff3070a7
Binary files /dev/null and b/src/sat/sat_npn3_finder.h differ
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 3c76e858f..bb0b1cde3 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -220,6 +220,7 @@ namespace sat {
         friend class xor_finder;
         friend class aig_finder;
         friend class lut_finder;
+        friend class npn3_finder;
     public:
         solver(params_ref const & p, reslimit& l);
         ~solver() override;