diff --git a/src/exists_forall/ef_values.c b/src/exists_forall/ef_values.c
index 88368621f..97df22d80 100755
--- a/src/exists_forall/ef_values.c
+++ b/src/exists_forall/ef_values.c
@@ -721,13 +721,12 @@ term_t ef_get_value_rep(ef_table_t *vtable, term_t value, int_hmap_t *requests)
         x = v->data[i];
         p = int_hmap_find(&vtable->generation, x);
         if (p != NULL && p->val < best_gen) {
-	  best_gen = p->val;
-	  best_x = x;
-	}
+          best_gen = p->val;
+          best_x = x;
+        }
         if (best_x == NULL_TERM) best_x = x;
       }
       store_rep(vtable, value, best_x);
-      assert(0);
     }
 
     if (!term_is_composite(vtable->terms, best_x)) {
@@ -756,11 +755,15 @@ term_t ef_get_value_rep(ef_table_t *vtable, term_t value, int_hmap_t *requests)
 
       present = (int_hmap_find(requests, f) != NULL);
       if (present) {
-        printf("Circular dependency encountered while finding a representative for term: %s\n", yices_term_to_string(value, 120, 1, 0));
-        assert(0);
+        // Keep f unchanged if representative construction is cyclic.
+        frep = f;
+      } else {
+        frep = ef_get_value_rep(vtable, f, requests);
+        if (frep == NULL_TERM) {
+          // No representative available: keep the original argument.
+          frep = f;
+        }
       }
-
-      frep = ef_get_value_rep(vtable, f, requests);
       if (f != frep) {
         ivector_push(&args, f);
         ivector_push(&argsrep, frep);
diff --git a/src/exists_forall/efsolver.c b/src/exists_forall/efsolver.c
index 9519af059..208a3a341 100644
--- a/src/exists_forall/efsolver.c
+++ b/src/exists_forall/efsolver.c
@@ -1334,6 +1334,10 @@ static smt_status_t ef_solver_test_exists_model(ef_solver_t *solver, term_t doma
     if (done)
       break;
 
+    if (status == YICES_STATUS_INTERRUPTED) {
+      break;
+    }
+
     uvar_cnstr_old = uvar_cnstr;
     generation++;
     context_pop(forall_ctx);
@@ -1622,3 +1626,5 @@ void ef_solver_check(ef_solver_t *solver, const param_t *parameters,
 
   ef_solver_search(solver);
 }
+
+
diff --git a/src/solvers/cdcl/smt_core.c b/src/solvers/cdcl/smt_core.c
index 82bf986fe..ebd81096d 100644
--- a/src/solvers/cdcl/smt_core.c
+++ b/src/solvers/cdcl/smt_core.c
@@ -5527,6 +5527,11 @@ static void smt_interrupt_push(smt_core_t *s) {
 
 static void smt_interrupt_pop(smt_core_t *s) {
   if (s->interrupt_push) {
+    if (s->status == YICES_STATUS_INTERRUPTED ||
+        s->status == YICES_STATUS_SEARCHING) {
+      // Ensure smt_pop preconditions hold on interrupt cleanup paths.
+      s->status = YICES_STATUS_IDLE;
+    }
     smt_pop(s);
     s->interrupt_push = false;
   }
diff --git a/tests/regress/iss366a.smt2 b/tests/regress/iss366a.smt2
new file mode 100644
index 000000000..639ed925c
--- /dev/null
+++ b/tests/regress/iss366a.smt2
@@ -0,0 +1,7 @@
+(set-logic UF)
+(declare-const x Bool)
+(declare-fun v () Bool)
+(declare-sort S 0)
+(assert (or v (and (not v) (forall ((q Bool)) (exists ((q S)) (forall ((q3 S)) (forall ((q5 Bool)) (and x (distinct q3 q)))))))))
+(assert (or (forall ((q S)) (exists ((q3 S)) (exists ((q5 Bool)) (not (distinct q3 q)))))))
+(check-sat)
diff --git a/tests/regress/iss366a.smt2.gold b/tests/regress/iss366a.smt2.gold
new file mode 100644
index 000000000..a292b3029
--- /dev/null
+++ b/tests/regress/iss366a.smt2.gold
@@ -0,0 +1 @@
+interrupted
diff --git a/tests/regress/iss366a.smt2.options b/tests/regress/iss366a.smt2.options
new file mode 100644
index 000000000..8ae880e0c
--- /dev/null
+++ b/tests/regress/iss366a.smt2.options
@@ -0,0 +1 @@
+--timeout=1
diff --git a/tests/regress/iss366b.smt2 b/tests/regress/iss366b.smt2
new file mode 100644
index 000000000..43128b49a
--- /dev/null
+++ b/tests/regress/iss366b.smt2
@@ -0,0 +1,6 @@
+(set-logic UF)
+(declare-fun v () Bool)
+(declare-sort S 0)
+(assert (or (forall ((q Bool)) (exists ((q2 S)) (forall ((q S)) (distinct v (not (= q2 q))))))))
+(assert (or (forall ((q2 S)) (exists ((q S)) (= q2 q)))))
+(check-sat)
diff --git a/tests/regress/iss366b.smt2.gold b/tests/regress/iss366b.smt2.gold
new file mode 100644
index 000000000..a292b3029
--- /dev/null
+++ b/tests/regress/iss366b.smt2.gold
@@ -0,0 +1 @@
+interrupted
diff --git a/tests/regress/iss366b.smt2.options b/tests/regress/iss366b.smt2.options
new file mode 100644
index 000000000..8ae880e0c
--- /dev/null
+++ b/tests/regress/iss366b.smt2.options
@@ -0,0 +1 @@
+--timeout=1