From 2da3593f50ede049e9e819b944ae1822a39f0f7e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Aug 2021 17:36:42 -0700 Subject: [PATCH] lower/upper case Signed-off-by: Nikolaj Bjorner --- src/math/bigfix/types.h | 2 +- src/math/polysat/fixplex_def.h | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) 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::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; }