diff --git a/src/math/bigfix/types.h b/src/math/bigfix/types.h
index c1bd7a56e..2eb51b39e 100644
--- a/src/math/bigfix/types.h
+++ b/src/math/bigfix/types.h
@@ -50,7 +50,7 @@ typedef struct FStar_UInt128_uint128_s {
  * latter is for internal use. */
 typedef FStar_UInt128_uint128 FStar_UInt128_t, uint128_t;
 
-#include "math/bigfix/lowstar_endianness.h"
+#include "math/bigfix/LowStar_Endianness.h"
 
 #endif
 
diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h
index 805583bdf..18cb7b121 100644
--- a/src/math/polysat/fixplex_def.h
+++ b/src/math/polysat/fixplex_def.h
@@ -97,7 +97,6 @@ namespace polysat {
     lbool fixplex<Ext>::make_feasible() {
         ++m_stats.m_num_checks;
         m_left_basis.reset();
-        m_unsat_core.reset();
         unsigned num_iterations = 0;
         unsigned num_repeated = 0;
         var_t v = null_var;
@@ -1220,6 +1219,8 @@ namespace polysat {
         }
         for (unsigned i = 0; i < m_vars.size(); ++i) {
             SASSERT(is_base(i) || in_bounds(i));
+            if (!is_base(i) && !in_bounds(i))
+                return false;
         }
         return true;
     }