diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index 1a65bcb1c..3b63bbdcf 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -293,29 +293,6 @@ namespace polysat {
         return c.display(out);
     }
 
-    struct fi_record {
-        eval_interval               interval;
-        vector<signed_constraint>   side_cond;
-        signed_constraint           src;
-        rational                    coeff;
-
-        /** Create invalid fi_record */
-        fi_record(): interval(eval_interval::full()) {}
-
-        fi_record(eval_interval interval, vector<signed_constraint> side_cond, signed_constraint src, rational coeff):
-            interval(interval),
-            side_cond(side_cond),
-            src(src),
-            coeff(coeff)
-        {}
-
-        struct less {
-            bool operator()(fi_record const& a, fi_record const& b) const {
-                return a.interval.lo_val() < b.interval.lo_val();
-            }
-        };
-    };
-
     class constraint_pp {
         constraint const* c;
         lbool status;
diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h
index a61fe1c26..96093ed79 100644
--- a/src/math/polysat/forbidden_intervals.h
+++ b/src/math/polysat/forbidden_intervals.h
@@ -20,6 +20,29 @@ namespace polysat {
 
     class solver;
 
+    struct fi_record {
+        eval_interval               interval;
+        vector<signed_constraint>   side_cond;
+        signed_constraint           src;
+        rational                    coeff;
+
+        /** Create invalid fi_record */
+        fi_record(): interval(eval_interval::full()) {}
+
+        fi_record(eval_interval interval, vector<signed_constraint> side_cond, signed_constraint src, rational coeff):
+            interval(interval),
+            side_cond(side_cond),
+            src(src),
+            coeff(coeff)
+        {}
+
+        struct less {
+            bool operator()(fi_record const& a, fi_record const& b) const {
+                return a.interval.lo_val() < b.interval.lo_val();
+            }
+        };
+    };
+
     class forbidden_intervals {
         solver& s;