diff --git a/doc/manual/manual.tex b/doc/manual/manual.tex
index 886cb7397..038314a28 100644
--- a/doc/manual/manual.tex
+++ b/doc/manual/manual.tex
@@ -4550,7 +4550,7 @@ \subsection*{Building a Context and Checking Satisfiability}
 
  case STATUS_IDLE:
  case STATUS_SEARCHING:
- case STATUS_INTERRUPTED:
+ case YICES_STATUS_INTERRUPTED:
  case STATUS_ERROR:
    fprintf(stderr, "Error in check_context\n");
    yices_print_error(stderr);
diff --git a/doc/sphinx/source/_static/example1.c b/doc/sphinx/source/_static/example1.c
index 06c9f9d65..aae8f23a0 100644
--- a/doc/sphinx/source/_static/example1.c
+++ b/doc/sphinx/source/_static/example1.c
@@ -127,7 +127,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);
diff --git a/doc/sphinx/source/_static/example1b.c b/doc/sphinx/source/_static/example1b.c
index 8456f3a81..0d60d76b1 100644
--- a/doc/sphinx/source/_static/example1b.c
+++ b/doc/sphinx/source/_static/example1b.c
@@ -135,7 +135,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);
diff --git a/doc/sphinx/source/api-types.rst b/doc/sphinx/source/api-types.rst
index e0194090a..f3f7b4db2 100644
--- a/doc/sphinx/source/api-types.rst
+++ b/doc/sphinx/source/api-types.rst
@@ -426,7 +426,7 @@ Contexts
        STATUS_UNKNOWN,
        STATUS_SAT,
        STATUS_UNSAT,
-       STATUS_INTERRUPTED,
+       YICES_STATUS_INTERRUPTED,
        STATUS_ERROR
      } smt_status_t;
 
@@ -470,13 +470,13 @@ Contexts
       asserted (if the inconsistency is detected by formula
       simplification), or when the search terminates.
 
-   .. c:enum:: STATUS_INTERRUPTED
+   .. c:enum:: YICES_STATUS_INTERRUPTED
 
       State entered when the search is interrupted.
 
       When a context is in the state :c:enum:`STATUS_SEARCHING` then the search
       can be interrupted through a call to :c:func:`yices_stop_search`. This
-      moves the context's state to :c:enum:`STATUS_INTERRUPTED`.
+      moves the context's state to :c:enum:`YICES_STATUS_INTERRUPTED`.
 
    .. c:enum:: STATUS_ERROR
 
diff --git a/doc/sphinx/source/basic-usage.rst b/doc/sphinx/source/basic-usage.rst
index 6ca952cbd..8227cf64a 100644
--- a/doc/sphinx/source/basic-usage.rst
+++ b/doc/sphinx/source/basic-usage.rst
@@ -154,7 +154,7 @@ context, assert ``f`` in this context, then call function :c:func:`yices_check_c
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);
diff --git a/doc/sphinx/source/context-operations.rst b/doc/sphinx/source/context-operations.rst
index d8aaff909..412ee498d 100644
--- a/doc/sphinx/source/context-operations.rst
+++ b/doc/sphinx/source/context-operations.rst
@@ -550,7 +550,7 @@ assert formulas, check satisfiability, and query the context's status.
      These are the states after a search completes. :c:enum:`STATUS_UNKNOWN` means
      that the search was inconclusive, which may happen if the solver is not complete.
 
-   - :c:enum:`STATUS_INTERRUPTED`.
+   - :c:enum:`YICES_STATUS_INTERRUPTED`.
 
      This state is entered if a search is interrupted.
 
@@ -596,7 +596,7 @@ assert formulas, check satisfiability, and query the context's status.
 
      -- type1 := bool
 
-   - if *ctx*'s state is :c:enum:`STATUS_INTERRUPTED`
+   - if *ctx*'s state is :c:enum:`YICES_STATUS_INTERRUPTED`
 
      -- error code: :c:enum:`CTX_INVALID_OPERATION`
 
@@ -667,13 +667,13 @@ assert formulas, check satisfiability, and query the context's status.
      - :c:enum:`STATUS_UNKNOWN`: the solver can't prove whether the context is
        satisfiable or not.
 
-     - :c:enum:`STATUS_INTERRUPTED`: the search was interrupted by a
+     - :c:enum:`YICES_STATUS_INTERRUPTED`: the search was interrupted by a
        call to :c:func:`yices_stop_search`.
 
      This returned value is also stored as the context's status flag, with the following exception:
 
      - If the context is configured for mode *interactive* and the search is interrupted,
-       then the function returns :c:enum:`STATUS_INTERRUPTED` but the context's state is
+       then the function returns :c:enum:`YICES_STATUS_INTERRUPTED` but the context's state is
        restored to what it was before the call to :c:func:`yices_check_context`, and the
        internal status flag is reset to  :c:enum:`STATUS_IDLE`.
 
@@ -698,7 +698,7 @@ assert formulas, check satisfiability, and query the context's status.
 
    .. note:: If the search is interrupted and the context's mode is
              not *interactive* then the context's enters state
-             :c:enum:`STATUS_INTERRUPTED`. The only way to recover is
+             :c:enum:`YICES_STATUS_INTERRUPTED`. The only way to recover is
              then to call :c:func:`yices_reset_context` or
              :c:func:`yices_pop` (assuming the context supports push and pop).
 
@@ -782,7 +782,7 @@ be removed by :c:func:`yices_pop`.
      -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED`
 
    - if *ctx* supports push and pop but its status is :c:enum:`STATUS_UNSAT`,
-     :c:enum:`STATUS_SEARCHING`, or :c:enum:`STATUS_INTERRUPTED`:
+     :c:enum:`STATUS_SEARCHING`, or :c:enum:`YCIES_STATUS_INTERRUPTED`:
 
      -- error code: :c:enum:`CTX_INVALID_OPERATION`
 
diff --git a/examples/example1.c b/examples/example1.c
index 3c71372b1..8f81f39ac 100644
--- a/examples/example1.c
+++ b/examples/example1.c
@@ -145,7 +145,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);
diff --git a/examples/example1b.c b/examples/example1b.c
index 766863df1..4d70d0dce 100644
--- a/examples/example1b.c
+++ b/examples/example1b.c
@@ -157,7 +157,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);
diff --git a/examples/example1c.c b/examples/example1c.c
index d12b3dcca..7815807b6 100644
--- a/examples/example1c.c
+++ b/examples/example1c.c
@@ -150,7 +150,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error_fd(2);
diff --git a/examples/example2.c b/examples/example2.c
index b7fce722c..b3510f3ce 100644
--- a/examples/example2.c
+++ b/examples/example2.c
@@ -104,7 +104,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");
diff --git a/examples/example2b.c b/examples/example2b.c
index 7d192fde8..0880deb06 100644
--- a/examples/example2b.c
+++ b/examples/example2b.c
@@ -124,7 +124,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");
diff --git a/examples/example2c.c b/examples/example2c.c
index 25e928b87..208f7d8b6 100644
--- a/examples/example2c.c
+++ b/examples/example2c.c
@@ -124,7 +124,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");
diff --git a/examples/example2d.c b/examples/example2d.c
index 6c0c2ae2a..6f5dead0c 100644
--- a/examples/example2d.c
+++ b/examples/example2d.c
@@ -117,7 +117,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");
diff --git a/examples/example2e.c b/examples/example2e.c
index 020ba53a1..5dc587cf1 100644
--- a/examples/example2e.c
+++ b/examples/example2e.c
@@ -117,7 +117,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");
diff --git a/examples/example_unsat_core.c b/examples/example_unsat_core.c
index de31ce5df..75ff13661 100644
--- a/examples/example_unsat_core.c
+++ b/examples/example_unsat_core.c
@@ -109,7 +109,7 @@ static void check_and_get_core(context_t *ctx, uint32_t n, const term_t *a) {
     yices_delete_term_vector(&core);
     break;
 
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     printf("the check was interrupted\n");
     break;
 
diff --git a/tests/unit/test_core3.c b/tests/unit/test_core3.c
index 3faa8354d..a18538631 100644
--- a/tests/unit/test_core3.c
+++ b/tests/unit/test_core3.c
@@ -168,7 +168,7 @@ static void sat_search(smt_core_t *core, uint32_t conflict_bound, uint32_t *redu
   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;