diff --git a/src/math/bigfix/kremlib/FStar_UInt128.h b/src/math/bigfix/kremlib/FStar_UInt128.h
index 9b5ece517..570832839 100644
--- a/src/math/bigfix/kremlib/FStar_UInt128.h
+++ b/src/math/bigfix/kremlib/FStar_UInt128.h
@@ -8,9 +8,9 @@
 #define __FStar_UInt128_H
 #include <inttypes.h>
 #include <stdbool.h>
-#include "kremlin/lowstar_endianness.h"
-#include "kremlin/internal/types.h"
-#include "kremlin/internal/target.h"
+#include "math/bigfix/kremlin/lowstar_endianness.h"
+#include "math/bigfix/kremlin/internal/types.h"
+#include "math/bigfix/kremlin/internal/target.h"
 
 
 
diff --git a/src/math/bigfix/kremlib/FStar_UInt_8_16_32_64.h b/src/math/bigfix/kremlib/FStar_UInt_8_16_32_64.h
index a7d3cbae7..12626858e 100644
--- a/src/math/bigfix/kremlib/FStar_UInt_8_16_32_64.h
+++ b/src/math/bigfix/kremlib/FStar_UInt_8_16_32_64.h
@@ -8,9 +8,9 @@
 #define __FStar_UInt_8_16_32_64_H
 #include <inttypes.h>
 #include <stdbool.h>
-#include "kremlin/lowstar_endianness.h"
-#include "kremlin/internal/types.h"
-#include "kremlin/internal/target.h"
+#include "math/bigfix/kremlin/lowstar_endianness.h"
+#include "math/bigfix/kremlin/internal/types.h"
+#include "math/bigfix/kremlin/internal/target.h"
 
 static inline uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b)
 {
diff --git a/src/math/bigfix/kremlib/LowStar_Endianness.h b/src/math/bigfix/kremlib/LowStar_Endianness.h
index 5cd3be350..d6f6f7857 100644
--- a/src/math/bigfix/kremlib/LowStar_Endianness.h
+++ b/src/math/bigfix/kremlib/LowStar_Endianness.h
@@ -8,12 +8,10 @@
 #define __LowStar_Endianness_H
 #include <inttypes.h>
 #include <stdbool.h>
-#include "kremlin/lowstar_endianness.h"
-#include "kremlin/internal/types.h"
-#include "kremlin/internal/target.h"
-
-
-#include "FStar_UInt128.h"
+#include "math/bigfix/kremlin/lowstar_endianness.h"
+#include "math/bigfix/kremlin/internal/types.h"
+#include "math/bigfix/kremlin/internal/target.h"
+#include "math/bigfix/FStar_UInt128.h"
 
 static inline void store128_le(uint8_t *x0, FStar_UInt128_uint128 x1);
 
diff --git a/src/math/bigfix/kremlib/fstar_uint128_gcc64.h b/src/math/bigfix/kremlib/fstar_uint128_gcc64.h
index aae6a7dc9..e0b8926f1 100644
--- a/src/math/bigfix/kremlib/fstar_uint128_gcc64.h
+++ b/src/math/bigfix/kremlib/fstar_uint128_gcc64.h
@@ -23,9 +23,9 @@
 #ifndef FSTAR_UINT128_GCC64
 #define FSTAR_UINT128_GCC64
 
-#include "FStar_UInt128.h"
-#include "FStar_UInt_8_16_32_64.h"
-#include "LowStar_Endianness.h"
+#include "math/bigfix/kremlib/FStar_UInt128.h"
+#include "math/bigfix/kremlib/FStar_UInt_8_16_32_64.h"
+#include "math/bigfix/kremlib/LowStar_Endianness.h"
 
 /* GCC + using native unsigned __int128 support */
 
diff --git a/src/math/bigfix/kremlib/fstar_uint128_msvc.h b/src/math/bigfix/kremlib/fstar_uint128_msvc.h
index c2a28abc6..aa4f4c262 100644
--- a/src/math/bigfix/kremlib/fstar_uint128_msvc.h
+++ b/src/math/bigfix/kremlib/fstar_uint128_msvc.h
@@ -11,9 +11,9 @@
 #ifndef FSTAR_UINT128_MSVC
 #define FSTAR_UINT128_MSVC
 
-#include "kremlin/internal/types.h"
-#include "FStar_UInt128.h"
-#include "FStar_UInt_8_16_32_64.h"
+#include "math/bigfix/kremlin/internal/types.h"
+#include "math/bigfix/kremlib/FStar_UInt128.h"
+#include "math/bigfix/kremlib/FStar_UInt_8_16_32_64.h"
 
 #ifndef _MSC_VER
 #  error This file only works with the MSVC compiler
diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index 366ee69ef..64d658f6d 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -67,6 +67,7 @@ add_executable(test-z3
   matcher.cpp
   "${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
   memory.cpp
+  mod_interval.cpp
   model2expr.cpp
   model_based_opt.cpp
   model_evaluator.cpp
diff --git a/src/test/fixplex.cpp b/src/test/fixplex.cpp
index 8481dca79..4fefbfcbd 100644
--- a/src/test/fixplex.cpp
+++ b/src/test/fixplex.cpp
@@ -115,18 +115,6 @@ namespace polysat {
         
     }
 
-
-    static void test_interval() {
-        mod_interval<uint64_t> i1(1, 2);
-        mod_interval<uint64_t> i2(3, 6);
-        std::cout << i1 << " " << i2 << "\n";
-        std::cout << i1 << " * 4 := " << (i1 * 4) << "\n";
-        std::cout << i2 << " * 3 := " << (i2 * 3) << "\n";
-        std::cout << i1 << " * -4 := " << (i1 * (0 - 4)) << "\n";
-        std::cout << i2 << " * -3 := " << (i2 * (0 - 3)) << "\n";
-        std::cout << "-" << i2 << " := " << (-i2) << "\n";
-    }
-
     static void test_gcd() {
         std::cout << "gcd\n";
         uint64_ext::manager e;
@@ -147,7 +135,6 @@ void tst_fixplex() {
     polysat::test4();
     polysat::test5();
 
-    polysat::test_interval();
     polysat::test_gcd();
     polysat::test_eq();
 }
diff --git a/src/test/main.cpp b/src/test/main.cpp
index e8d073f3d..3cb287f63 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -265,4 +265,5 @@ int main(int argc, char ** argv) {
     TST(polysat);
     TST_ARGV(polysat_argv);
     TST(fixplex);
+    TST(mod_interval);
 }
diff --git a/src/test/mod_interval.cpp b/src/test/mod_interval.cpp
new file mode 100644
index 000000000..f9990fea8
--- /dev/null
+++ b/src/test/mod_interval.cpp
@@ -0,0 +1,16 @@
+#include "math/interval/mod_interval_def.h"
+
+static void test_interval1() {
+    mod_interval<uint64_t> i1(1, 2);
+    mod_interval<uint64_t> i2(3, 6);
+    std::cout << i1 << " " << i2 << "\n";
+    std::cout << i1 << " * 4 := " << (i1 * 4) << "\n";
+    std::cout << i2 << " * 3 := " << (i2 * 3) << "\n";
+    std::cout << i1 << " * -4 := " << (i1 * (0 - 4)) << "\n";
+    std::cout << i2 << " * -3 := " << (i2 * (0 - 3)) << "\n";
+    std::cout << "-" << i2 << " := " << (-i2) << "\n";
+}
+
+void tst_mod_interval() {
+    test_interval1();
+}