Properly make solver exit upon errors

[shaobo-he-aws]

Category

Lean formalization

Describe the feature you'd like to request

In the Rust implementation of SymCC, cedar-policy/cedar#1846, cedar-policy/cedar#1849, cedar-policy/cedar#1857 kill the solver process and let OS recollect it when the solver reports a parsing error or reading its output encounters an EOF. Note that it's for CVC5 only.

We can't seem to port these changes readily because Rust uses a trait to represent solvers and Lean uses a type. So I create an issue instead.

Describe alternatives you've considered

N/A

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change