diff --git a/src/math/polysat/interval.h b/src/math/polysat/interval.h
index 7e0b31bd0..7300b04b5 100644
--- a/src/math/polysat/interval.h
+++ b/src/math/polysat/interval.h
@@ -67,7 +67,7 @@ namespace polysat {
 
     // distance from a to b, wrapping around at mod_value.
     // basically mod(b - a, mod_value), but distance(0, mod_value, mod_value) = mod_value.
-    rational distance(rational const& a, rational const& b, rational const& mod_value) {
+    inline rational distance(rational const& a, rational const& b, rational const& mod_value) {
         SASSERT(mod_value.is_power_of_two());
         SASSERT(0 <= a && a < mod_value);
         SASSERT(0 <= b && b <= mod_value);
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 93b2bf169..4c14c2dc4 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -1435,6 +1435,7 @@ namespace polysat {
             e = n;
         } while (e != first);
         UNREACHABLE();
+        return {nullptr, false};
     }
 
     // find viable values in half-open interval [to_cover_lo;to_cover_hi[ w.r.t. unit intervals on the given layer
@@ -1564,6 +1565,9 @@ namespace polysat {
 
         // TODO: refinement and fallback solver -- can we refine without throwing out all the entry_cursors we have set up?
         //       we only have to chase intervals from the beginning if ec.cur has become inactive
+
+        NOT_IMPLEMENTED_YET();
+        return l_undef;
     }
 
     lbool viable::find_viable2(pvar v, rational& lo, rational& hi) {