)

The --early-exit flag is now properly handled to ensure that Halmos terminates
immediately after finding the first counterexample, avoiding the reporting of
multiple counterexamples. The previous implementation used a busy-waiting loop
with time.sleep(1) to wait for the first counterexample or all futures to
complete, which was inefficient and allowed multiple counterexamples to accumulate.

The updated code introduces an early_exit flag variable to keep track of whether
an early exit is requested. When a counterexample is found and --early-exit is set,
the early_exit flag is set to True. The future_callback function checks this flag
and immediately returns if it is True, preventing further processing of results.

The thread pool is shut down after all the submitted futures have completed or
been canceled, ensuring a clean termination.

)

The --early-exit flag is now properly handled to ensure that Halmos
terminates immediately after finding the first counterexample, avoiding
unnecessary solver computations.

The previous implementation allowed solver threads to continue running
even after a counterexample was found, leading to inefficient resource
usage and delayed termination.

The updated code introduces the following changes:

- A global list `solver_contexts` is introduced to store the solver
  contexts created in the `solve` function.

- The `solve` function is modified to append the solver context to the
  global list before returning.

- In the `future_callback` function, if `args.early_exit` is true and a
  counterexample is found, all the solver contexts in the global list are
  interrupted using `ctx.interrupt()`.

- Exception handling is added to the interruption process to avoid
  segmentation faults.

- After interrupting the solvers, the global list is cleared to prevent
  memory leaks.

With these changes, when `args.early_exit` is true and a counterexample
is found, the `future_callback` function interrupts all the running
solver contexts, effectively stopping the unnecessary computations and
allowing Halmos to terminate early.

…#243)

The --early-exit flag is now properly handled to ensure that Halmos
terminates immediately after finding the first counterexample, avoiding
unnecessary solver computations.

The previous implementation allowed solver threads to continue running
even after a counterexample was found, leading to inefficient resource
usage and delayed termination.

The updated code introduces the following changes:

- A global list `solver_contexts` is introduced to store the solver
  contexts created in the `solve` function.

- The `solve` function is modified to append the solver context to the
  global list before returning.

- The list of futures is stored in a variable before submitting them to
  the thread pool.

- In the `future_callback` function, if `args.early_exit` is true and a
  counterexample is found:
  - All the solver contexts in the global list are interrupted using
    `ctx.interrupt()`.
  - The remaining futures are canceled using `future.cancel()` to stop
    unnecessary computations.
  - The global lists are cleared to prevent memory leaks.

- Exception handling is added to the interruption process to avoid
  segmentation faults.

With these changes, when `args.early_exit` is true and a counterexample
is found, the `future_callback` function interrupts all the running
solver contexts and cancels the remaining futures, effectively stopping
the unnecessary computations and allowing Halmos to terminate early.

…#243)

The --early-exit flag is now properly handled to ensure that Halmos
terminates immediately after finding the first counterexample, avoiding
unnecessary solver computations.

The previous implementation allowed solver threads to continue running
even after a counterexample was found, leading to inefficient resource
usage and delayed termination.

The updated code introduces the following changes:

- A global list `solver_contexts` is introduced to store the solver
  contexts created in the `solve` function.

- The `solve` function is modified to append the solver context to the
  global list before returning.

- The list of futures is stored in a variable before submitting them to
  the thread pool.

- In the `future_callback` function, if `args.early_exit` is true and a
  counterexample is found:
  - All the solver contexts in the global list are interrupted using
    `ctx.interrupt()`.
  - The remaining futures are canceled using `future.cancel()` to stop
    unnecessary computations.
  - The global lists are cleared to prevent memory leaks.

- Exception handling is added to the interruption process to avoid
  segmentation faults.

With these changes, when `args.early_exit` is true and a counterexample
is found, the `future_callback` function interrupts all the running
solver contexts and cancels the remaining futures, effectively stopping
the unnecessary computations and allowing Halmos to terminate early.