[isabelle-dev] sledgehammer / yices

[Jasmin Blanchette]

Am 19.07.2012 um 12:49 schrieb Sascha Boehme:

> I don't know for sure. It might be that YICES_INSTALLED and friends were added as a sanity check to avoid errors when invoking the solver locally and it doesn't exist. If that's the case, it's probably better to remove YICES_INSTALLED and just test if the file pointed to by YICES_SOLVER does exist.

What I intended to do was much simpler: Check whether "YICES_SOLVER" is set at all, irrespectively of whether it exists. I can't imagine a use case where somebody would bother to set "YICES_SOLVER" to something and not want it to be installed.

Jasmin