Marco Gario

Was there one or two tests with tactics that were disabled? I changed only one.

This seems to have been fixed in Z3 https://github.com/Z3Prover/z3/issues/6034 .

The problem seems to be that even if `a` is a symbol and not a constant array. We do have the simplifications for handling the slightly different case: ```a =...

Thanks for the PR. We had not gotten around to extend the installer to OSX, but this seems to cover most of the obstacles. As you probably already guessed, we...

:wave: Thanks for reporting this! This sounds reasonable. As a general principle, we want to be strict when type-checking expressions. Therefore, this conversion should live completely in the parser, and...

:wave: Is this something that we still want to do? If so, I would probably separate the "cosmetic" breaking change of renaming `environment` to `env` from the "correctness" change of...

This seems like either a bug in the logic detection, or Z3 not being decorated with a logic combining both arrays and strings. I assume you were using the branch...

As far as I am aware, no one is planning to extend support for those theories. Happy to support you in opening a PR to do so.

That's great! > However, this conflicts with PySMT's custom logic QF_NRAt, since logic names are compared lowercase. I have not thought about this deeply but I think the `t` at...

Doesn't mathsat support some type of timeout? In general, I'd rather fix this in the solver / solver interface than in a test, as users might run exactly into this...