diff --git a/src/math/bigfix/kremlib/LowStar_Endianness.h b/src/math/bigfix/kremlib/LowStar_Endianness.h
index d6f6f7857..84d2afb5e 100644
--- a/src/math/bigfix/kremlib/LowStar_Endianness.h
+++ b/src/math/bigfix/kremlib/LowStar_Endianness.h
@@ -11,7 +11,7 @@
 #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"
+#include "math/bigfix/kremlib/FStar_UInt128.h"
 
 static inline void store128_le(uint8_t *x0, FStar_UInt128_uint128 x1);
 
diff --git a/src/math/interval/mod_interval.h b/src/math/interval/mod_interval.h
index aa790b8b1..56929acc4 100644
--- a/src/math/interval/mod_interval.h
+++ b/src/math/interval/mod_interval.h
@@ -42,11 +42,11 @@ template<typename Numeral>
 class mod_interval {
     bool emp { false };
 public:
-    virtual ~mod_interval() {}
     Numeral lo { 0 };
     Numeral hi { 0 };
     mod_interval() {}
     mod_interval(Numeral const& l, Numeral const& h): lo(l), hi(h) {}
+    virtual ~mod_interval() {}
     static mod_interval free() { return mod_interval(0, 0); }
     static mod_interval empty() { mod_interval i(0, 0); i.emp = true; return i; }
 
@@ -60,12 +60,12 @@ public:
     void set_bounds(Numeral const& l, Numeral const& h) { lo = l; hi = h; }
     void set_empty() { emp = true; }
 
-    void intersect_ule(Numeral const& h);
-    void intersect_uge(Numeral const& l);
-    void intersect_ult(Numeral const& h);
-    void intersect_ugt(Numeral const& l);
-    void intersect_fixed(Numeral const& n);
-    void intersect_diff(Numeral const& n);
+    mod_interval& intersect_ule(Numeral const& h);
+    mod_interval& intersect_uge(Numeral const& l);
+    mod_interval& intersect_ult(Numeral const& h);
+    mod_interval& intersect_ugt(Numeral const& l);
+    mod_interval& intersect_fixed(Numeral const& n);
+    mod_interval& intersect_diff(Numeral const& n);
 
     mod_interval operator&(mod_interval const& other) const;
     mod_interval operator+(mod_interval const& other) const;
diff --git a/src/math/interval/mod_interval_def.h b/src/math/interval/mod_interval_def.h
index c41054ba3..0e1b07d95 100644
--- a/src/math/interval/mod_interval_def.h
+++ b/src/math/interval/mod_interval_def.h
@@ -124,35 +124,37 @@ Numeral mod_interval<Numeral>::closest_value(Numeral const& n) const {
 // TBD: correctness and completeness for wrap-around semantics needs to be checked/fixed
 
 template<typename Numeral>
-void mod_interval<Numeral>::intersect_ule(Numeral const& h) {
+mod_interval<Numeral>& mod_interval<Numeral>::intersect_ule(Numeral const& h) {
     if (is_empty())
-        return;
+        return *this;
     if (is_max(h))
-        return;
+        return *this;
     else if (is_free())
         lo = 0, hi = h + 1;
     else if (hi > lo && lo > h)
         set_empty();
     else if (hi != 0 || h + 1 < hi)
-        hi = h + 1;  
+        hi = h + 1; 
+    return *this;
 }
 
 template<typename Numeral>
-void mod_interval<Numeral>::intersect_uge(Numeral const& l) {
+mod_interval<Numeral>& mod_interval<Numeral>::intersect_uge(Numeral const& l) {
     if (is_empty())
-        return;
+        return *this;
     if (lo < hi && hi <= l)
         set_empty();
     else if (is_free())
         lo = l, hi = 0;
     else if (lo < hi && lo < l)
-        lo = l;                    
+        lo = l;     
+    return *this;
 }
 
 template<typename Numeral>
-void mod_interval<Numeral>::intersect_ult(Numeral const& h) {
+mod_interval<Numeral>& mod_interval<Numeral>::intersect_ult(Numeral const& h) {
     if (is_empty())
-        return;
+        return *this;
     if (h == 0)
         set_empty();
     else if (is_free())
@@ -161,12 +163,13 @@ void mod_interval<Numeral>::intersect_ult(Numeral const& h) {
         set_empty();
     else if (hi > lo && h < hi)
         hi = h;
+    return *this;
 }
 
 template<typename Numeral>
-void mod_interval<Numeral>::intersect_ugt(Numeral const& l) {
+mod_interval<Numeral>& mod_interval<Numeral>::intersect_ugt(Numeral const& l) {
     if (is_empty())
-        return;
+        return *this;
     if (is_max(l))
         set_empty();
     else if (is_free())
@@ -177,24 +180,26 @@ void mod_interval<Numeral>::intersect_ugt(Numeral const& l) {
         set_empty();
     else if (lo < hi) 
         lo = l + 1;
+    return *this;
 }
 
 template<typename Numeral>
-void mod_interval<Numeral>::intersect_fixed(Numeral const& a) {
+mod_interval<Numeral>& mod_interval<Numeral>::intersect_fixed(Numeral const& a) {
     if (is_empty())
-        return;
+        return *this;
     if (!contains(a))
         set_empty();
     else if (is_max(a))
         lo = a, hi = 0;
     else
         lo = a, hi = a + 1;
+    return *this;
 }
 
 template<typename Numeral>
-void mod_interval<Numeral>::intersect_diff(Numeral const& a) {
+mod_interval<Numeral>& mod_interval<Numeral>::intersect_diff(Numeral const& a) {
     if (!contains(a) || is_empty())
-        return;
+        return *this;
     if (a == lo && a + 1 == hi)
         set_empty();
     else if (a == lo && hi == 0 && is_max(a))
@@ -205,4 +210,5 @@ void mod_interval<Numeral>::intersect_diff(Numeral const& a) {
         hi = a;
     else if (hi == 0 && is_max(a))
         hi = a;
+    return *this;
 }
diff --git a/src/test/mod_interval.cpp b/src/test/mod_interval.cpp
index f9990fea8..70e3a6eea 100644
--- a/src/test/mod_interval.cpp
+++ b/src/test/mod_interval.cpp
@@ -11,6 +11,14 @@ static void test_interval1() {
     std::cout << "-" << i2 << " := " << (-i2) << "\n";
 }
 
+static void test_interval2() {
+    mod_interval<uint32_t> i;
+    std::cout << " >= 0: " << i.intersect_uge(0) << "\n";
+    std::cout << " >= 1: " << i.intersect_uge(1) << "\n";
+
+}
+
 void tst_mod_interval() {
     test_interval1();
+    test_interval2();
 }