[isabelle-dev] sledgehammer / yices
jasmin.blanchette at gmail.com
Thu Jul 19 13:28:52 CEST 2012
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.
More information about the isabelle-dev