Hi, With changeset 3214c39777ab, the SMT solvers have been turned into components.
As a consequence, the now obsolete environment variables (in settings files) CVC3_SOLVER, YICES_SOLVER, and Z3_SOLVER should be removed. This only applies if you have used the smt method so before. Prior to their usage, SMT solvers need to be added to the components list -- more precisely, the paths to SMT solver bundles need to be added to $ISABELLE_HOME_USER/etc/components. SMT solver bundles can be found at TU Muenchen servers in the directories ~isabelle/cvc3 (without support for Darwin-based systems for now, this will be fixed within the next days) and ~isabelle/z3. Note the provided LICENSE files (e.g., Z3 is restricted for non-commercial usage only). The reward for this rather clumsy setup is a more powerful sledgehammer command. Sascha _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
