diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index eb0e94173..5e55adbd5 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -89,6 +89,7 @@ add_executable(test-z3
   permutation.cpp
   polynomial.cpp
   polynorm.cpp
+  polysat.cpp
   prime_generator.cpp
   proof_checker.cpp
   qe_arith.cpp
diff --git a/src/test/main.cpp b/src/test/main.cpp
index 3e3f1d575..7bea9d746 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -262,4 +262,5 @@ int main(int argc, char ** argv) {
     TST(solver_pool);
     //TST_ARGV(hs);
     TST(finder);
+    TST(polysat);
 }
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
new file mode 100644
index 000000000..823563cc6
--- /dev/null
+++ b/src/test/polysat.cpp
@@ -0,0 +1,15 @@
+#include "math/polysat/polysat.h"
+
+namespace polysat {
+    // test resolve, factoring routines
+    // auxiliary 
+    static void test1() {
+
+    }
+}
+
+// also add test that loads from a file and runs the polysat engine.
+
+void tst_polysat() {
+    polysat::test1();
+}