Fix EF value-rep assertion crash (issue #366)

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

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

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

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)

tests/regress/iss366a.smt2.gold

@@ -0,0 +1 @@
+interrupted

tests/regress/iss366a.smt2.options

@@ -0,0 +1 @@
+--timeout=1

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)

tests/regress/iss366b.smt2.gold

@@ -0,0 +1 @@
+interrupted

tests/regress/iss366b.smt2.options

@@ -0,0 +1 @@
+--timeout=1