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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
