status_interrupted -> yices_status_interrupted

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);

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);

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);

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
 

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);

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`
 

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);

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);

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);

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");

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");

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");

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");

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");

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;
 

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;