fix: parsing unsat core output variants

[daejunpark]

smt queries generated for assertion solving include three commands at the end:

...
(check-sat)
(get-model)
(get-unsat-core)

when the result is unsat, the (get-model) command is not applicable. in that case, some solvers (e.g., yices2) generate an error message, while other solvers (e.g., bitwuzla) silently ignore it.

this pr handles both behaviors when parsing the unsat core output.

[daejunpark]

note: there is another diverging behavior in interpreting smt-lib queries among different solvers. specifically, bitwuzla explicitly requires (set-option :produce-models true) to be provided in the query if the (get-model) command is to be executed later, while other solvers (e.g., z3, yices2, cvc5) don't require that.

i attempted to add the set-option explicitly in this commit 0746c58, but it led to unexpected performance degradation in yices2, so i reverted it for now to investigate further.

in the meantime, when using solvers that require the explicit option, you need to add a cli option flag to set the option separately, e.g., bitwuzla -m.

[karmacoma-eth]

note: there is another diverging behavior in interpreting smt-lib queries among different solvers. specifically, bitwuzla explicitly requires (set-option :produce-models true) to be provided in the query if the (get-model) command is to be executed later, while other solvers (e.g., z3, yices2, cvc5) don't require that.

i attempted to add the set-option explicitly in this commit 0746c58, but it led to unexpected performance degradation in yices2, so i reverted it for now to investigate further.

in the meantime, when using solvers that require the explicit option, you need to add a cli option flag to set the option separately, e.g., bitwuzla -m.

this is indeed tricky, this is how I currently invoke the various solvers:

SOLVERS = {
    "bitwuzla": "bitwuzla --produce-models".split(),
    "boolector": "boolector --model-gen --output-number-format=hex".split(),
    "cvc4": "cvc4 --produce-models".split(),
    "cvc5": "cvc5 --produce-models".split(),
    "stp": "stp --print-counterex --SMTLIB2".split(),
    "yices-smt2": "yices-smt2".split(),  # needs to include (get-model) in the SMT2 file to generate the model
    "z3": "z3 --model".split(),
}

[karmacoma-eth]

thanks for providing the extra context! I'm going to take your word that the regex does what it says :)