diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index dc60ef58a..97cc45f95 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -80,7 +80,7 @@ def init_project_def():
     add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
     add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp',  'fd_solver', 'qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
     add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt')
-    add_lib('polysat', ['util','dd','simplex'],'math/polysat')
+    add_lib('polysat', ['util','dd','simplex','interval'],'math/polysat')
     API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_fpa.h', 'z3_spacer.h']
     add_lib('api', ['portfolio',  'realclosure', 'opt'],
             includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index ec100d569..166f960e0 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -39,9 +39,9 @@ add_subdirectory(math/polynomial)
 add_subdirectory(math/dd)
 add_subdirectory(math/hilbert)
 add_subdirectory(math/simplex)
+add_subdirectory(math/interval)
 add_subdirectory(math/polysat)
 add_subdirectory(math/automata)
-add_subdirectory(math/interval)
 add_subdirectory(math/realclosure)
 add_subdirectory(math/subpaving)
 add_subdirectory(ast)
diff --git a/src/math/interval/mod_interval.h b/src/math/interval/mod_interval.h
new file mode 100644
index 000000000..901528f55
--- /dev/null
+++ b/src/math/interval/mod_interval.h
@@ -0,0 +1,67 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    mod_interval.h
+
+Abstract:
+
+    Intervals over fixed precision modular arithmetic
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+
+#pragma once
+
+
+template<typename Numeral>
+struct pp {
+    Numeral n;
+    pp(Numeral const& n):n(n) {}
+};
+
+template<typename Numeral>
+inline std::ostream& operator<<(std::ostream& out, pp<Numeral> const& p) {
+    if ((0 - p.n) < p.n)
+        return out << "-" << (0 - p.n);
+    return out << p.n;
+}
+
+template<typename Numeral>
+struct mod_interval {
+    bool emp { false };
+    Numeral lo { 0 };
+    Numeral hi { 0 };
+    mod_interval() {}
+    mod_interval(Numeral const& l, Numeral const& h): lo(l), hi(h) {}
+    static mod_interval free() { return mod_interval(0, 0); }
+    static mod_interval empty() { mod_interval i(0, 0); i.emp = true; return i; }
+    bool is_free() const { return !emp && lo == hi; }
+    bool is_empty() const { return emp; }
+    bool contains(Numeral const& n) const;
+    mod_interval operator&(mod_interval const& other) const;
+    mod_interval operator+(mod_interval const& other) const;
+    mod_interval operator-(mod_interval const& other) const;
+    mod_interval operator*(mod_interval const& other) const;
+    mod_interval operator-() const;
+    mod_interval operator*(Numeral const& n) const;
+    mod_interval operator+(Numeral const& n) const { return mod_interval(lo + n, hi + n); }
+    mod_interval operator-(Numeral const& n) const { return mod_interval(lo - n, hi - n); }
+    mod_interval& operator+=(mod_interval const& other) { *this = *this + other; return *this; }
+    std::ostream& display(std::ostream& out) const { 
+        if (is_empty()) return out << "empty"; 
+        if (is_free()) return out << "free";
+        return out << "[" << pp(lo) << ", " << pp(hi) << "["; 
+    }
+};
+
+template<typename Numeral>
+inline std::ostream& operator<<(std::ostream& out, mod_interval<Numeral> const& i) {
+    return i.display(out);
+}
+
diff --git a/src/math/interval/mod_interval_def.h b/src/math/interval/mod_interval_def.h
new file mode 100644
index 000000000..8062015f2
--- /dev/null
+++ b/src/math/interval/mod_interval_def.h
@@ -0,0 +1,111 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    mod_interval_def.h
+
+Abstract:
+
+    Intervals over fixed precision modular arithmetic
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+
+#pragma once
+
+#include "math/interval/mod_interval.h"
+
+template<typename Numeral>
+bool mod_interval<Numeral>::contains(Numeral const& n) const {
+    if (is_empty())
+        return false;
+    if (is_free())
+        return true;
+    if (lo < hi)
+        return lo <= n && n < hi;
+    else
+        return lo <= n || n < hi;
+}
+
+template<typename Numeral>
+mod_interval<Numeral> mod_interval<Numeral>::operator+(mod_interval<Numeral> const& other) const {
+    if (is_empty())
+        return *this;
+    if (other.is_empty())
+        return other;
+    if (is_free())
+        return *this;
+    if (other.is_free())
+        return other;
+    Numeral sz = (hi - lo) + (other.hi - other.lo);
+    if (sz < (hi - lo))
+        return mod_interval::free();
+    return mod_interval(lo + other.lo, hi + other.hi);
+}
+
+template<typename Numeral>
+mod_interval<Numeral> mod_interval<Numeral>::operator-(mod_interval<Numeral> const& other) const {
+    return *this + (-other);
+}
+
+template<typename Numeral>
+mod_interval<Numeral> mod_interval<Numeral>::operator-() const {
+    if (is_empty())
+        return *this;
+    if (is_free())
+        return *this;
+    return mod_interval(1 - hi, 1 - lo);
+}
+
+template<typename Numeral>
+mod_interval<Numeral> mod_interval<Numeral>::operator*(Numeral const& n) const {
+    if (is_empty())
+        return *this;
+    if (n == 0)
+        return mod_interval(0, 1);
+    if (n == 1)
+        return *this;
+    if (is_free())
+        return *this;
+    Numeral sz = hi - lo;
+    if (0 - n < n) {
+        Numeral mn = 0 - n;
+        Numeral mz = mn * sz;            
+        if (mz / mn != sz)
+            return mod_interval::free();
+        return mod_interval((hi - 1) * n, n * lo + 1);
+    }
+    else {
+        Numeral mz = n * sz;
+        if (mz / n != sz)
+            return mod_interval::free();
+        return mod_interval(n * lo, n * (hi - 1) + 1);
+    }
+}
+
+template<typename Numeral>
+mod_interval<Numeral> mod_interval<Numeral>::operator&(mod_interval const& other) const {
+    Numeral l, h;
+    if (is_free() || other.is_empty())
+        return other;
+    if (other.is_free() || is_empty())
+        return *this;
+    if (contains(other.lo))
+        l = other.lo;
+    else if (other.contains(lo))
+        l = lo;
+    else 
+        return mod_interval::empty();
+    if (contains(other.hi - 1))
+        h = other.hi;
+    else if (other.contains(hi - 1))
+        h = hi;
+    else
+        return mod_interval::empty();
+    return mod_interval(l, h);
+}
diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt
index 9e3a45798..657104167 100644
--- a/src/math/polysat/CMakeLists.txt
+++ b/src/math/polysat/CMakeLists.txt
@@ -12,4 +12,5 @@ z3_add_component(polysat
     util
     dd
     simplex
+    interval
 )
diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h
index 5c7fdcf97..c570ebbf3 100644
--- a/src/math/polysat/fixplex.h
+++ b/src/math/polysat/fixplex.h
@@ -20,6 +20,7 @@ Author:
 
 #include <limits>
 #include "math/simplex/sparse_matrix.h"
+#include "math/interval/mod_interval.h"
 #include "util/heap.h"
 #include "util/map.h"
 #include "util/lbool.h"
@@ -29,54 +30,6 @@ namespace polysat {
 
     typedef unsigned var_t;
 
-    template<typename Numeral>
-    struct pp {
-        Numeral n;
-        pp(Numeral const& n):n(n) {}
-    };
-
-    template<typename Numeral>
-    inline std::ostream& operator<<(std::ostream& out, pp<Numeral> const& p) {
-        if ((0 - p.n) < p.n)
-            return out << "-" << (0 - p.n);
-        return out << p.n;
-    }
-
-    /**
-     * Modular interval arithmetic
-     */
-    template<typename Numeral>
-    struct interval {
-        bool emp { false };
-        Numeral lo { 0 };
-        Numeral hi { 0 };
-        interval() {}
-        interval(Numeral const& l, Numeral const& h): lo(l), hi(h) {}
-        static interval free() { return interval(0, 0); }
-        static interval empty() { interval i(0, 0); i.emp = true; return i; }
-        bool is_free() const { return !emp && lo == hi; }
-        bool is_empty() const { return emp; }
-        bool contains(Numeral const& n) const;
-        interval operator&(interval const& other) const;
-        interval operator+(interval const& other) const;
-        interval operator-(interval const& other) const;
-        interval operator*(interval const& other) const;
-        interval operator-() const;
-        interval operator*(Numeral const& n) const;
-        interval operator+(Numeral const& n) const { return interval(lo + n, hi + n); }
-        interval operator-(Numeral const& n) const { return interval(lo - n, hi - n); }
-        interval& operator+=(interval const& other) { *this = *this + other; return *this; }
-        std::ostream& display(std::ostream& out) const { 
-            if (is_empty()) return out << "empty"; 
-            if (is_free()) return out << "free";
-            return out << "[" << pp(lo) << ", " << pp(hi) << "["; 
-        }
-    };
-
-    template<typename Numeral>
-    inline std::ostream& operator<<(std::ostream& out, interval<Numeral> const& i) {
-        return i.display(out);
-    }
 
     template<typename Ext>
     class fixplex {
@@ -111,7 +64,7 @@ namespace polysat {
             S_DEFAULT
         };
 
-        struct var_info : public interval<numeral> {
+        struct var_info : public mod_interval<numeral> {
             unsigned    m_base2row:29;
             unsigned    m_is_base:1;
             numeral     m_value { 0 };
@@ -119,8 +72,8 @@ namespace polysat {
                 m_base2row(0),
                 m_is_base(false)
             {}
-            var_info& operator&=(interval<numeral> const& range) {
-                interval<numeral>::operator=(range);
+            var_info& operator&=(mod_interval<numeral> const& range) {
+                mod_interval<numeral>::operator=(range);
                 return *this;
             }
         };
@@ -215,7 +168,7 @@ namespace polysat {
         void fixed_var_eh(row const& r, var_t x);
         void eq_eh(var_t x, var_t y, row const& r1, row const& r2);
         void propagate_bounds(row const& r);
-        void new_bound(row const& r, var_t x, interval<numeral> const& range);
+        void new_bound(row const& r, var_t x, mod_interval<numeral> const& range);
         void pivot(var_t x_i, var_t x_j, numeral const& b, numeral const& value);
         numeral value2delta(var_t v, numeral const& new_value) const;
         void update_value(var_t v, numeral const& delta);
@@ -224,7 +177,7 @@ namespace polysat {
         var_t select_pivot_core(var_t x, numeral const& new_value, numeral& out_b);
         bool in_bounds(var_t v) const { return in_bounds(v, value(v)); }
         bool in_bounds(var_t v, numeral const& b) const { return in_bounds(b, m_vars[v]); }
-        bool in_bounds(numeral const& val, interval<numeral> const& range) const { return range.contains(val); }
+        bool in_bounds(numeral const& val, mod_interval<numeral> const& range) const { return range.contains(val); }
         bool is_free(var_t v) const { return lo(v) == hi(v); }
         bool is_non_free(var_t v) const { return !is_free(v); }
         bool is_fixed(var_t v) const { return lo(v) + 1 == hi(v); }
diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h
index 354bab72c..00a520b3d 100644
--- a/src/math/polysat/fixplex_def.h
+++ b/src/math/polysat/fixplex_def.h
@@ -20,99 +20,10 @@ Author:
 
 #include "math/polysat/fixplex.h"
 #include "math/simplex/sparse_matrix_def.h"
+#include "math/interval/mod_interval_def.h"
 
 namespace polysat {
 
-    template<typename Numeral>
-    bool interval<Numeral>::contains(Numeral const& n) const {
-        if (is_empty())
-            return false;
-        if (is_free())
-            return true;
-        if (lo < hi)
-            return lo <= n && n < hi;
-        else
-            return lo <= n || n < hi;
-    }
-
-    template<typename Numeral>
-    interval<Numeral> interval<Numeral>::operator+(interval<Numeral> const& other) const {
-        if (is_empty())
-            return *this;
-        if (other.is_empty())
-            return other;
-        if (is_free())
-            return *this;
-        if (other.is_free())
-            return other;
-        Numeral sz = (hi - lo) + (other.hi - other.lo);
-        if (sz < (hi - lo))
-            return interval::free();
-        return interval(lo + other.lo, hi + other.hi);
-    }
-
-    template<typename Numeral>
-    interval<Numeral> interval<Numeral>::operator-(interval<Numeral> const& other) const {
-        return *this + (-other);
-    }
-
-    template<typename Numeral>
-    interval<Numeral> interval<Numeral>::operator-() const {
-        if (is_empty())
-            return *this;
-        if (is_free())
-            return *this;
-        return interval(1 - hi, 1 - lo);
-    }
-
-    template<typename Numeral>
-    interval<Numeral> interval<Numeral>::operator*(Numeral const& n) const {
-        if (is_empty())
-            return *this;
-        if (n == 0)
-            return interval(0, 1);
-        if (n == 1)
-            return *this;
-        if (is_free())
-            return *this;
-        Numeral sz = hi - lo;
-        if (0 - n < n) {
-            Numeral mn = 0 - n;
-            Numeral mz = mn * sz;            
-            if (mz / mn != sz)
-                return interval::free();
-            return interval((hi - 1) * n, n * lo + 1);
-        }
-        else {
-            Numeral mz = n * sz;
-            if (mz / n != sz)
-                return interval::free();
-            return interval(n * lo, n * (hi - 1) + 1);
-        }
-    }
-
-    template<typename Numeral>
-    interval<Numeral> interval<Numeral>::operator&(interval const& other) const {
-        Numeral l, h;
-        if (is_free() || other.is_empty())
-            return other;
-        if (other.is_free() || is_empty())
-            return *this;
-        if (contains(other.lo))
-            l = other.lo;
-        else if (other.contains(lo))
-            l = lo;
-        else 
-            return interval::empty();
-        if (contains(other.hi - 1))
-            h = other.hi;
-        else if (other.contains(hi - 1))
-            h = hi;
-        else
-            return interval::empty();
-        return interval(l, h);
-    }
-
     template<typename Ext>
     fixplex<Ext>::~fixplex() {
         reset();
@@ -513,7 +424,7 @@ namespace polysat {
     bool fixplex<Ext>::is_infeasible_row(var_t x) {
         SASSERT(is_base(x));
         auto r = base2row(x);
-        interval<numeral> range(0, 1);
+        mod_interval<numeral> range(0, 1);
         for (auto const& e : M.row_entries(row(r))) {
             var_t v = e.var();
             numeral const& c = e.coeff();
@@ -915,7 +826,7 @@ namespace polysat {
 
     template<typename Ext>
     void fixplex<Ext>::propagate_bounds(row const& r) {
-        interval<numeral> range(0, 1);
+        mod_interval<numeral> range(0, 1);
         numeral free_c = 0;
         var_t free_v = null_var;
         for (auto const& e : M.row_entries(r)) {
@@ -949,7 +860,7 @@ namespace polysat {
     }
 
     template<typename Ext>
-    void fixplex<Ext>::new_bound(row const& r, var_t x, interval<numeral> const& range) {
+    void fixplex<Ext>::new_bound(row const& r, var_t x, mod_interval<numeral> const& range) {
         if (range.is_free())
             return;
         m_vars[x] &= range;
diff --git a/src/test/fixplex.cpp b/src/test/fixplex.cpp
index d5da95071..0ca951c9d 100644
--- a/src/test/fixplex.cpp
+++ b/src/test/fixplex.cpp
@@ -115,8 +115,8 @@ namespace polysat {
 
 
     static void test_interval() {
-        interval<uint64_t> i1(1, 2);
-        interval<uint64_t> i2(3, 6);
+        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";