diff --git a/src/api/yices_api.c b/src/api/yices_api.c
index faed13510..06b8b35f9 100644
--- a/src/api/yices_api.c
+++ b/src/api/yices_api.c
@@ -8510,7 +8510,7 @@ EXPORTED int32_t yices_push(context_t *ctx) {
     }
     assert(context_status(ctx) == STATUS_UNSAT);
     // fall through
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_SEARCHING:
     set_error_code(CTX_INVALID_OPERATION);
     return -1;
@@ -8555,7 +8555,7 @@ EXPORTED int32_t yices_pop(context_t *ctx) {
   switch (context_status(ctx)) {
   case STATUS_UNKNOWN:
   case STATUS_SAT:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     context_clear(ctx);
     break;
 
@@ -8699,7 +8699,7 @@ int32_t _o_yices_assert_formula(context_t *ctx, term_t t) {
     break;
 
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     set_error_code(CTX_INVALID_OPERATION);
     return -1;
 
@@ -8773,7 +8773,7 @@ EXPORTED int32_t yices_assert_formulas(context_t *ctx, uint32_t n, const term_t
     break;
 
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     set_error_code(CTX_INVALID_OPERATION);
     return -1;
 
@@ -8828,7 +8828,7 @@ EXPORTED int32_t yices_assert_blocking_clause(context_t *ctx) {
   case STATUS_UNSAT:
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     set_error_code(CTX_INVALID_OPERATION);
     return -1;
 
@@ -9029,13 +9029,13 @@ EXPORTED smt_status_t yices_check_context(context_t *ctx, const param_t *params)
       params = &default_params;
     }
     stat = check_context(ctx, params);
-    if (stat == STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
+    if (stat == YICES_STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
       context_cleanup(ctx);
     }
     break;
 
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     set_error_code(CTX_INVALID_OPERATION);
     stat = STATUS_ERROR;
     break;
@@ -9101,7 +9101,7 @@ smt_status_t _o_yices_check_context_with_assumptions(context_t *ctx, const param
     break;
 
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     set_error_code(CTX_INVALID_OPERATION);
     return STATUS_ERROR;
 
@@ -9136,7 +9136,7 @@ smt_status_t _o_yices_check_context_with_assumptions(context_t *ctx, const param
 
   // call check
   stat = check_context_with_assumptions(ctx, params, n, assumptions.data);
-  if (stat == STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
+  if (stat == YICES_STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
     context_cleanup(ctx);
   }
 
@@ -9212,7 +9212,7 @@ EXPORTED smt_status_t yices_check_context_with_model(context_t *ctx, const param
     break;
 
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     set_error_code(CTX_INVALID_OPERATION);
     return STATUS_ERROR;
 
@@ -9232,7 +9232,7 @@ EXPORTED smt_status_t yices_check_context_with_model(context_t *ctx, const param
 
   // call check
   stat = check_context_with_model(ctx, params, mdl, n, t);
-  if (stat == STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
+  if (stat == YICES_STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
     context_cleanup(ctx);
   }
 
@@ -10316,7 +10316,7 @@ static smt_status_t yices_ef_check_formulas(const term_t f[], uint32_t n, smt_lo
       break;
 
     case EF_STATUS_INTERRUPTED:
-      stat = STATUS_INTERRUPTED;
+      stat = YICES_STATUS_INTERRUPTED;
       break;
 
     case EF_STATUS_SUBST_ERROR:
diff --git a/src/context/context.h b/src/context/context.h
index de5d25396..d67f7a4d0 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -206,7 +206,7 @@ extern int32_t assert_blocking_clause(context_t *ctx);
  * - if parameters is NULL, the default values are used
  *
  * return status: either STATUS_UNSAT, STATUS_SAT, STATUS_UNKNOWN,
- * STATUS_INTERRUPTED (these codes are defined in smt_core.h)
+ * YICES_STATUS_INTERRUPTED (these codes are defined in smt_core.h)
  */
 extern smt_status_t check_context(context_t *ctx, const param_t *parameters);
 
@@ -219,7 +219,7 @@ extern smt_status_t check_context(context_t *ctx, const param_t *parameters);
  * - each a[i] must be defined in ctx->core
  *
  * return status: either STATUS_UNSAT, STATUS_SAT, STATUS_UNKNOWN,
- * STATUS_INTERRUPTED
+ * YICES_STATUS_INTERRUPTED
  *
  * If status is STATUS_UNSAT then the assumptions are inconsistent
  */
@@ -235,7 +235,7 @@ extern smt_status_t check_context_with_assumptions(context_t *ctx, const param_t
  * - t = variables to use from the model (size = n)
  *
  * return status: either STATUS_UNSAT, STATUS_SAT, STATUS_UNKNOWN,
- * STATUS_INTERRUPTED
+ * YICES_STATUS_INTERRUPTED
  *
  * If status is STATUS_UNSAT then the context and model are inconsistent
  */
@@ -434,7 +434,7 @@ extern int32_t context_process_formulas(context_t *ctx, uint32_t n, term_t *f);
  *  STATUS_UNKNOWN
  *  STATUS_SAT
  *  STATUS_UNSAT
- *  STATUS_INTERRUPTED
+ *  YICES_STATUS_INTERRUPTED
  */
 static inline smt_status_t context_status(context_t *ctx) {
   if (ctx->arch == CTX_ARCH_MCSAT) {
diff --git a/src/context/context_solver.c b/src/context/context_solver.c
index 32288b506..1eb3b9c27 100644
--- a/src/context/context_solver.c
+++ b/src/context/context_solver.c
@@ -149,7 +149,7 @@ static void search(smt_core_t *core, uint32_t conflict_bound, uint32_t *reduce_t
   uint32_t r_threshold;
   literal_t l;
 
-  assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == STATUS_INTERRUPTED);
+  assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);
 
   max_conflicts = num_conflicts(core) + conflict_bound;
   r_threshold = *reduce_threshold;
@@ -203,7 +203,7 @@ static void luby_search(smt_core_t *core, uint32_t conflict_bound, uint32_t *red
   uint32_t r_threshold;
   literal_t l;
 
-  assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == STATUS_INTERRUPTED);
+  assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);
 
   max_conflicts = num_conflicts(core) + conflict_bound;
   r_threshold = *reduce_threshold;
@@ -262,7 +262,7 @@ static void special_search(smt_core_t *core, uint32_t conflict_bound, uint32_t *
   uint32_t r_threshold;
   literal_t l;
 
-  assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == STATUS_INTERRUPTED);
+  assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);
 
   max_conflicts = num_conflicts(core) + conflict_bound;
   r_threshold = *reduce_threshold;
@@ -666,7 +666,7 @@ smt_status_t precheck_context(context_t *ctx) {
     stat = smt_status(core);
 
     assert(stat == STATUS_UNSAT || stat == STATUS_SEARCHING ||
-	   stat == STATUS_INTERRUPTED);
+	   stat == YICES_STATUS_INTERRUPTED);
 
     if (stat == STATUS_SEARCHING) {
       end_search_unknown(core);
@@ -703,7 +703,7 @@ smt_status_t check_with_delegate(context_t *ctx, const char *sat_solver, uint32_
     stat = smt_status(core);
 
     assert(stat == STATUS_UNSAT || stat == STATUS_SEARCHING ||
-	   stat == STATUS_INTERRUPTED);
+	   stat == YICES_STATUS_INTERRUPTED);
 
     if (stat == STATUS_SEARCHING) {
       if (smt_easy_sat(core)) {
@@ -763,7 +763,7 @@ int32_t bitblast_then_export_to_dimacs(context_t *ctx, const char *filename, smt
     stat = smt_status(core);
 
     assert(stat == STATUS_UNSAT || stat == STATUS_SEARCHING ||
-	   stat == STATUS_INTERRUPTED);
+	   stat == YICES_STATUS_INTERRUPTED);
 
     if (stat == STATUS_SEARCHING) {
       code = 1;
@@ -820,7 +820,7 @@ int32_t process_then_export_to_dimacs(context_t *ctx, const char *filename, smt_
     stat = smt_status(core);
 
     assert(stat == STATUS_UNSAT || stat == STATUS_SEARCHING ||
-	   stat == STATUS_INTERRUPTED);
+	   stat == YICES_STATUS_INTERRUPTED);
 
     if (stat == STATUS_SEARCHING) {
       if (smt_easy_sat(core)) {
diff --git a/src/exists_forall/efsolver.c b/src/exists_forall/efsolver.c
index 81faeea8c..0644dc307 100644
--- a/src/exists_forall/efsolver.c
+++ b/src/exists_forall/efsolver.c
@@ -508,7 +508,7 @@ static context_t *get_forall_context(ef_solver_t *solver) {
  *    - value[i] = a constant term mapped to evar[i] in the model
  * 2) code = STATUS_UNSAT: not satisfiable
  *
- * 3) other codes report an error of some kind or STATUS_INTERRUPTED
+ * 3) other codes report an error of some kind or YICES_STATUS_INTERRUPTED
  */
 static smt_status_t satisfy_context(ef_solver_t *solver, context_t *ctx, term_t *var, uint32_t n, term_t *value, model_t **model, bool is_exists) {
   smt_status_t stat;
@@ -829,7 +829,7 @@ static void ef_sample_constraint(ef_solver_t *solver, uint32_t i) {
       // no more samples for this constraints
       goto done;
 
-    case STATUS_INTERRUPTED:
+    case YICES_STATUS_INTERRUPTED:
       solver->status = EF_STATUS_INTERRUPTED;
       goto done;
 
@@ -1342,7 +1342,7 @@ static smt_status_t ef_solver_test_exists_model(ef_solver_t *solver, term_t doma
     case STATUS_UNSAT:
       break;
 
-    case STATUS_INTERRUPTED:
+    case YICES_STATUS_INTERRUPTED:
       solver->status = EF_STATUS_INTERRUPTED;
       break;
 
@@ -1389,7 +1389,7 @@ static void trace_candidate_check(ef_solver_t *solver, uint32_t i, smt_status_t
     trace_printf(solver->trace, 4, "(EF: candidate passed constraint %"PRIu32")\n", i);
     break;
 
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     trace_printf(solver->trace, 4, "(EF: candidate check was interrupted)\n");
     break;
 
@@ -1549,7 +1549,7 @@ static void ef_solver_search(ef_solver_t *solver) {
       solver->status = EF_STATUS_UNSAT;
       break;
 
-    case STATUS_INTERRUPTED:
+    case YICES_STATUS_INTERRUPTED:
       trace_puts(solver->trace, 4, "(EF: Interrupted)\n");
       solver->status = EF_STATUS_INTERRUPTED;
       break;
diff --git a/src/frontend/smt2/smt2_commands.c b/src/frontend/smt2/smt2_commands.c
index af6483f4f..82aa90286 100644
--- a/src/frontend/smt2/smt2_commands.c
+++ b/src/frontend/smt2/smt2_commands.c
@@ -277,7 +277,7 @@ static void bitblast_then_export(context_t *ctx, const char *s) {
   case STATUS_UNSAT:
     break;
 
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     fprintf(stderr, "Export to dimacs interrupted\n");
     break;
 
@@ -1551,7 +1551,7 @@ static void report_status(smt2_globals_t *g, smt_status_t status) {
   case STATUS_UNKNOWN:
   case STATUS_SAT:
   case STATUS_UNSAT:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     show_status(status);
     break;
 
@@ -2695,7 +2695,7 @@ static smt_status_t check_sat_with_timeout(smt2_globals_t *g, const param_t *par
   /*
    * Attempt to cleanly recover from interrupt
    */
-  if (stat == STATUS_INTERRUPTED) {
+  if (stat == YICES_STATUS_INTERRUPTED) {
     trace_printf(g->tracer, 2, "(check-sat: interrupted)\n");
     g->interrupted = true;
     if (context_get_mode(g->ctx) == CTX_MODE_INTERACTIVE) {
@@ -2741,7 +2741,7 @@ static smt_status_t check_sat_with_assumptions(smt2_globals_t *g, const param_t
   /*
    * Attempt to cleanly recover from interrupt
    */
-  if (stat == STATUS_INTERRUPTED) {
+  if (stat == YICES_STATUS_INTERRUPTED) {
     trace_printf(g->tracer, 2, "(check-sat-assuming: interrupted)\n");
     g->interrupted = true;
     if (context_get_mode(g->ctx) == CTX_MODE_INTERACTIVE) {
@@ -2787,7 +2787,7 @@ static smt_status_t check_sat_with_model(smt2_globals_t *g, const param_t *param
   /*
    * Attempt to cleanly recover from interrupt
    */
-  if (stat == STATUS_INTERRUPTED) {
+  if (stat == YICES_STATUS_INTERRUPTED) {
     trace_printf(g->tracer, 2, "(check-sat-assuming-model: interrupted)\n");
     g->interrupted = true;
     if (context_get_mode(g->ctx) == CTX_MODE_INTERACTIVE) {
@@ -3392,7 +3392,7 @@ static void cleanup_context(smt2_globals_t *g) {
     break;
 
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   default:
     bad_status_bug(g->err);
     break;
@@ -3448,7 +3448,7 @@ static void add_assertion(smt2_globals_t *g, term_t t) {
   case STATUS_UNKNOWN:
   case STATUS_SAT:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   default:
     bad_status_bug(g->err);
     break;
@@ -3492,7 +3492,7 @@ static void ctx_check_sat(smt2_globals_t *g) {
     break;
 
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   default:
     bad_status_bug(g->err);
     break;
@@ -3541,7 +3541,7 @@ static void ctx_unsat_core(smt2_globals_t *g) {
     case STATUS_UNKNOWN:
       // this should not happen.
     case STATUS_SEARCHING:
-    case STATUS_INTERRUPTED:
+    case YICES_STATUS_INTERRUPTED:
     default:
       bad_status_bug(g->err);
       break;
@@ -3588,7 +3588,7 @@ static void ctx_check_sat_assuming(smt2_globals_t *g, uint32_t n, signed_symbol_
     case STATUS_UNKNOWN:
     case STATUS_SAT:
     case STATUS_SEARCHING:
-    case STATUS_INTERRUPTED:
+    case YICES_STATUS_INTERRUPTED:
     default:
       bad_status_bug(g->err);
       break;
@@ -3620,7 +3620,7 @@ static void ctx_check_sat_assuming_model(smt2_globals_t *g, uint32_t n, const te
   case STATUS_UNKNOWN:
   case STATUS_SAT:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   default:
     bad_status_bug(g->err);
     break;
@@ -3648,7 +3648,7 @@ static void ctx_push(smt2_globals_t *g) {
   case STATUS_UNKNOWN:
   case STATUS_SAT:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   default:
     bad_status_bug(g->err);
     break;
@@ -3681,7 +3681,7 @@ static void ctx_pop(smt2_globals_t *g) {
   case STATUS_UNKNOWN:
   case STATUS_SAT:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   default:
     bad_status_bug(g->err);
     break;
@@ -3735,7 +3735,7 @@ static model_t *get_model(smt2_globals_t *g) {
         print_error("can't build a model. Call (check-sat) first");
         break;
 
-      case STATUS_INTERRUPTED:
+      case YICES_STATUS_INTERRUPTED:
 	print_error("the search was interrupted. No model is available");
 	break;
 
@@ -4142,7 +4142,7 @@ static void show_assignment(smt2_globals_t *g) {
       print_error("can't build the assignment. Call (check-sat) first");
       break;
 
-    case STATUS_INTERRUPTED:
+    case YICES_STATUS_INTERRUPTED:
       print_error("can't build the assignment. The search was interrupted");
       break;
 
@@ -4222,7 +4222,7 @@ static void show_unsat_core(smt2_globals_t *g) {
         delete_smt2_pp(&printer, true);
         break;
 
-      case STATUS_INTERRUPTED:
+      case YICES_STATUS_INTERRUPTED:
 	print_error("No unsat core. The search was interrupted");
 	break;
 
@@ -4264,7 +4264,7 @@ static void show_unsat_assumptions(smt2_globals_t *g) {
         delete_smt2_pp(&printer, true);
         break;
 
-      case STATUS_INTERRUPTED:
+      case YICES_STATUS_INTERRUPTED:
 	print_error("No unsat assumptions. The search was interrupted");
 	break;
 
@@ -4320,7 +4320,7 @@ static void show_unsat_model_interpolant(smt2_globals_t *g) {
       print_error("Call (check-sat-assuming-model) first");
       break;
 
-    case STATUS_INTERRUPTED:
+    case YICES_STATUS_INTERRUPTED:
       print_error("No model interpolant. Last call to check-sat timedout");
       break;
 
@@ -4524,7 +4524,7 @@ static void explain_unknown_status(smt2_globals_t *g) {
         break;
 
       case STATUS_SEARCHING:
-      case STATUS_INTERRUPTED:
+      case YICES_STATUS_INTERRUPTED:
       default:
         print_out("BUG: unexpected context status");
         freport_bug(__smt2_globals.err, "BUG: unexpected context status");
diff --git a/src/frontend/yices/yices_reval.c b/src/frontend/yices/yices_reval.c
index d1c8bd47a..6cb0b7071 100644
--- a/src/frontend/yices/yices_reval.c
+++ b/src/frontend/yices/yices_reval.c
@@ -1168,7 +1168,7 @@ static void cleanup_context(void) {
     break;
 
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   default:
     // should not happen
     freport_bug(stderr, "unexpected context status");
@@ -2735,7 +2735,7 @@ static void yices_check_cmd(void) {
       stat = do_check();
       print_status(stat);
       // force exit if the check was interrupted
-      done = (stat == STATUS_INTERRUPTED);
+      done = (stat == YICES_STATUS_INTERRUPTED);
 
     } else {
       if (code == TRIVIALLY_UNSAT) {
@@ -2777,7 +2777,7 @@ static void yices_check_cmd(void) {
 	// if the search was interrupted, cleanup
 	stat = do_check();
 	print_status(stat);
-	if (stat == STATUS_INTERRUPTED) {
+	if (stat == YICES_STATUS_INTERRUPTED) {
 	  if (mode == CTX_MODE_INTERACTIVE) {
 	    context_cleanup(context);
 	    assert(context_status(context) == STATUS_IDLE);
@@ -2795,7 +2795,7 @@ static void yices_check_cmd(void) {
 	if (stat != STATUS_ERROR) {
 	  print_status(stat);
 	}
-	if (stat == STATUS_INTERRUPTED) {
+	if (stat == YICES_STATUS_INTERRUPTED) {
 	  // try to cleanup if we're in interactive mode
 	  if (mode == CTX_MODE_INTERACTIVE) {
 	    context_cleanup(context);
@@ -2813,7 +2813,7 @@ static void yices_check_cmd(void) {
       break;
 
     case STATUS_SEARCHING:
-    case STATUS_INTERRUPTED:
+    case YICES_STATUS_INTERRUPTED:
     default:
       // this should not happen
       freport_bug(stderr,"unexpected context status in 'check'");
@@ -2847,7 +2847,7 @@ static void yices_check_assuming_cmd(uint32_t n, const signed_symbol_t *a) {
     if (status != STATUS_ERROR) {
       print_status(status);
     }
-    if (status == STATUS_INTERRUPTED) {
+    if (status == YICES_STATUS_INTERRUPTED) {
       if (mode == CTX_MODE_INTERACTIVE) {
 	// recover
 	context_cleanup(context);
@@ -2920,7 +2920,7 @@ static void yices_show_unsat_core_cmd(void) {
 
       case STATUS_IDLE:
       case STATUS_SEARCHING:
-      case STATUS_INTERRUPTED:
+      case YICES_STATUS_INTERRUPTED:
       default:
 	freport_bug(stderr, "unexpected context status in 'show-unsat-core'");
 	break;
@@ -2956,7 +2956,7 @@ static void yices_show_unsat_assumptions_cmd(void) {
 
       case STATUS_IDLE:
       case STATUS_SEARCHING:
-      case STATUS_INTERRUPTED:
+      case YICES_STATUS_INTERRUPTED:
       default:
 	freport_bug(stderr, "unexpected context status in 'show-unsat-assumptions'");
 	break;
@@ -3001,7 +3001,7 @@ static bool context_has_model(const char *cmd_name) {
     break;
 
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   default:
     // this should not happen
     freport_bug(stderr,"unexpected context status in '%s'", cmd_name);
@@ -3300,7 +3300,7 @@ static void bitblast_then_export(context_t *ctx, const char *s) {
     do_export(ctx, s);
     break;
 
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     if (context_supports_cleaninterrupt(ctx)) {
       context_cleanup(ctx);
       assert(context_status(ctx) == STATUS_IDLE);
diff --git a/src/include/yices.h b/src/include/yices.h
index b2b369278..8fb3dd269 100644
--- a/src/include/yices.h
+++ b/src/include/yices.h
@@ -52,6 +52,16 @@
 #define __YICES_DLLSPEC__
 #endif
 
+/*
+ * On mingw with the thread-safety option:
+ * STATUS_INTERRUPTED is a defined symbol in windows. 
+ * We have renamed the symbol in yices_types.h and here 
+ * we redefine the STATUS_INTERRUPTED symbol to be backward compatible.
+ * This will be removed in the non-backward compatible release (Yices 2.8).
+ */
+#if !defined(MINGW) || !defined(THREAD_SAFE)
+#define STATUS_INTERRUPTED YICES_STATUS_INTERRUPTED
+#endif
 
 #ifdef __cplusplus
 extern "C" {
diff --git a/src/include/yices_types.h b/src/include/yices_types.h
index dfd28cb79..278fc4980 100644
--- a/src/include/yices_types.h
+++ b/src/include/yices_types.h
@@ -80,7 +80,7 @@ typedef enum smt_status {
   STATUS_UNKNOWN,
   STATUS_SAT,
   STATUS_UNSAT,
-  STATUS_INTERRUPTED,
+  YICES_STATUS_INTERRUPTED, /* renaming because of a clash with windows defined symbol */
   STATUS_ERROR
 } smt_status_t;
 
diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c
index 2ffd9a6af..085cdeed7 100644
--- a/src/mcsat/solver.c
+++ b/src/mcsat/solver.c
@@ -2673,7 +2673,7 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin
 
   if (mcsat->stop_search) {
     if (mcsat->status == STATUS_SEARCHING) {
-      mcsat->status = STATUS_INTERRUPTED;
+      mcsat->status = YICES_STATUS_INTERRUPTED;
     }
     mcsat->stop_search = false;
   }
diff --git a/src/solvers/cdcl/smt_core.c b/src/solvers/cdcl/smt_core.c
index b854af1f4..efdd1a248 100644
--- a/src/solvers/cdcl/smt_core.c
+++ b/src/solvers/cdcl/smt_core.c
@@ -2047,7 +2047,7 @@ void decide_literal(smt_core_t *s, literal_t l) {
   uint32_t k;
   bvar_t v;
 
-  assert(s->status == STATUS_SEARCHING || s->status == STATUS_INTERRUPTED);
+  assert(s->status == STATUS_SEARCHING || s->status == YICES_STATUS_INTERRUPTED);
   assert(literal_is_unassigned(s, l));
 
   // Increase decision level
@@ -4218,7 +4218,7 @@ static bool preprocess_clause(smt_core_t *s, uint32_t *n, literal_t *a) {
 static bool on_the_fly(smt_core_t *s) {
   assert((s->status == STATUS_IDLE && s->decision_level == s->base_level) ||
          (s->status == STATUS_SEARCHING && s->decision_level >= s->base_level) ||
-         (s->status == STATUS_INTERRUPTED && s->decision_level >= s->base_level));
+         (s->status == YICES_STATUS_INTERRUPTED && s->decision_level >= s->base_level));
   return s->status != STATUS_IDLE;
 }
 
@@ -5485,7 +5485,7 @@ void smt_pop(smt_core_t *s) {
    * Abort if push_pop is not enabled or if there's no pushed state
    */
   assert((s->option_flag & PUSH_POP_MASK) != 0 && s->base_level > 0 &&
-         s->status != STATUS_INTERRUPTED && s->status != STATUS_SEARCHING);
+         s->status != YICES_STATUS_INTERRUPTED && s->status != STATUS_SEARCHING);
 
   // We need to backtrack before calling the pop function of th_solver
   backtrack_to_base_level(s);
@@ -5537,7 +5537,7 @@ static void smt_interrupt_pop(smt_core_t *s) {
  * - we just call pop
  */
 void smt_cleanup(smt_core_t *s) {
-  assert((s->status == STATUS_INTERRUPTED || s->status == STATUS_UNSAT)
+  assert((s->status == YICES_STATUS_INTERRUPTED || s->status == STATUS_UNSAT)
          && (s->option_flag & CLEAN_INTERRUPT_MASK) != 0);
   s->status = STATUS_IDLE; // make sure pop does not abort
   smt_interrupt_pop(s);
@@ -5628,7 +5628,7 @@ void smt_clear_unsat(smt_core_t *s) {
  */
 void smt_checkpoint(smt_core_t *s) {
   assert(s->status == STATUS_SEARCHING ||
-         s->status == STATUS_INTERRUPTED);
+         s->status == YICES_STATUS_INTERRUPTED);
   push_checkpoint(&s->checkpoints, s->decision_level, s->nvars);
   s->cp_flag = false;
 }
@@ -6074,7 +6074,7 @@ void start_search(smt_core_t *s, uint32_t n, const literal_t *a) {
  */
 void stop_search(smt_core_t *s) {
   if (s->status == STATUS_SEARCHING) {
-    s->status = STATUS_INTERRUPTED;
+    s->status = YICES_STATUS_INTERRUPTED;
   }
 }
 
@@ -6168,7 +6168,7 @@ bool smt_bounded_process(smt_core_t *s, uint64_t max_conflicts) {
  *   is done.
  */
 void smt_final_check(smt_core_t *s) {
-  assert(s->status == STATUS_SEARCHING || s->status == STATUS_INTERRUPTED);
+  assert(s->status == STATUS_SEARCHING || s->status == YICES_STATUS_INTERRUPTED);
 
   if (s->status == STATUS_SEARCHING) {
     switch (s->th_ctrl.final_check(s->th_solver)) {
@@ -6205,7 +6205,7 @@ bool smt_easy_sat(smt_core_t *s) {
   assert(s->bool_only);
 
   for (;;) {
-    assert(s->status == STATUS_SEARCHING || s->status == STATUS_INTERRUPTED);
+    assert(s->status == STATUS_SEARCHING || s->status == YICES_STATUS_INTERRUPTED);
     smt_propagation(s);
     assert(empty_lemma_queue(&s->lemmas));
     assert(! s->cp_flag);
@@ -6332,7 +6332,7 @@ static void partial_restart(smt_core_t *s, uint32_t k) {
  */
 void smt_restart(smt_core_t *s) {
 
-  assert(s->status == STATUS_SEARCHING || s->status == STATUS_INTERRUPTED);
+  assert(s->status == STATUS_SEARCHING || s->status == YICES_STATUS_INTERRUPTED);
 
 #if TRACE
   printf("\n---> DPLL RESTART\n");
@@ -6354,7 +6354,7 @@ void smt_partial_restart(smt_core_t *s) {
   bvar_t x;
   uint32_t i, k, n;
 
-  assert(s->status == STATUS_SEARCHING || s->status == STATUS_INTERRUPTED);
+  assert(s->status == STATUS_SEARCHING || s->status == YICES_STATUS_INTERRUPTED);
 
 #if TRACE
   printf("\n---> DPLL PARTIAL RESTART\n");
@@ -6406,7 +6406,7 @@ void smt_partial_restart_var(smt_core_t *s) {
   bvar_t x;
   uint32_t i, n;
 
-  assert(s->status == STATUS_SEARCHING || s->status == STATUS_INTERRUPTED);
+  assert(s->status == STATUS_SEARCHING || s->status == YICES_STATUS_INTERRUPTED);
 
 #if TRACE
   printf("\n---> DPLL PARTIAL RESTART (VARIANT)\n");
diff --git a/src/solvers/cdcl/smt_core.h b/src/solvers/cdcl/smt_core.h
index 9a07da0ba..cc58d3b37 100644
--- a/src/solvers/cdcl/smt_core.h
+++ b/src/solvers/cdcl/smt_core.h
@@ -830,7 +830,7 @@ typedef enum smt_status {
   STATUS_UNKNOWN,
   STATUS_SAT,
   STATUS_UNSAT,
-  STATUS_INTERRUPTED,
+  YICES_STATUS_INTERRUPTED,
   STATUS_ERROR, // not used by the context operations/only by yices_api
 } smt_status_t;
 #endif
@@ -1890,12 +1890,12 @@ extern void record_ternary_theory_conflict(smt_core_t *s, literal_t l1, literal_
  * Close the search: mark s as either SAT or UNKNOWN
  */
 static inline void end_search_sat(smt_core_t *s) {
-  assert(s->status == STATUS_SEARCHING || s->status == STATUS_INTERRUPTED);
+  assert(s->status == STATUS_SEARCHING || s->status == YICES_STATUS_INTERRUPTED);
   s->status = STATUS_SAT;
 }
 
 static inline void end_search_unknown(smt_core_t *s) {
-  assert(s->status == STATUS_SEARCHING || s->status == STATUS_INTERRUPTED);
+  assert(s->status == STATUS_SEARCHING || s->status == YICES_STATUS_INTERRUPTED);
   s->status = STATUS_UNKNOWN;
 }
 
diff --git a/src/solvers/cdcl/smt_core_printer.c b/src/solvers/cdcl/smt_core_printer.c
index 2a51c481e..9359407ea 100644
--- a/src/solvers/cdcl/smt_core_printer.c
+++ b/src/solvers/cdcl/smt_core_printer.c
@@ -51,8 +51,8 @@ void print_bval(FILE *f, bval_t b) {
  * Status
  */
 void print_status(FILE *f, smt_status_t s) {
-  if (s > STATUS_INTERRUPTED) {
-    s = STATUS_INTERRUPTED + 1;
+  if (s > YICES_STATUS_INTERRUPTED) {
+    s = YICES_STATUS_INTERRUPTED + 1;
   }
   fputs(status2string[s], f);
 }
diff --git a/tests/unit/test_core2.c b/tests/unit/test_core2.c
index ab2d453b2..73ec8839f 100644
--- a/tests/unit/test_core2.c
+++ b/tests/unit/test_core2.c
@@ -158,7 +158,7 @@ static void sat_search(smt_core_t *core, uint32_t conflict_bound, uint32_t reduc
   uint64_t max_conflicts;
   literal_t l;
 
-  assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == STATUS_INTERRUPTED);
+  assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);
 
   max_conflicts = num_conflicts(core) + conflict_bound;
 
@@ -527,8 +527,8 @@ static const char * const status2string[] = {
 };
 
 static void print_status(FILE *f, smt_status_t s) {
-  if (s > STATUS_INTERRUPTED) {
-    s = STATUS_INTERRUPTED + 1;
+  if (s > YICES_STATUS_INTERRUPTED) {
+    s = YICES_STATUS_INTERRUPTED + 1;
   }
   fputs(status2string[s], f);
 }
diff --git a/tests/unit/test_core3.c b/tests/unit/test_core3.c
index 336393379..3faa8354d 100644
--- a/tests/unit/test_core3.c
+++ b/tests/unit/test_core3.c
@@ -533,8 +533,8 @@ static const char * const status2string[] = {
 };
 
 static void print_status(FILE *f, smt_status_t s) {
-  if (s > STATUS_INTERRUPTED) {
-    s = STATUS_INTERRUPTED + 1;
+  if (s > YICES_STATUS_INTERRUPTED) {
+    s = YICES_STATUS_INTERRUPTED + 1;
   }
   fputs(status2string[s], f);
 }