tweag / simple-smt

BSD 3-Clause "New" or "Revised" License
0 stars 0 forks source link

`Solver.Z3`: the whole program stops when Z3 throws an error #8

Open qaristote opened 1 year ago

qaristote commented 1 year ago

Currently exceptions thrown by Z3 are not caught by the library. We could decide that this problem is to be dealt with by the end user, but I don't know if that's actually possible: I tried using catchIOError in the test-suite but the program still crashed. I haven't tried using catch but I expect the same behavior as the exception isn't thrown by Haskell itself.

Fixing this probably requires doing exception handling inside the inlined-C code, or switching to the C++ API along with inline-c-cpp which comes with a module for handling exceptions.