[isabelle-dev] AFP: Session AVL-Trees broken
jasmin.blanchette at gmail.com
Wed Jan 2 09:36:29 CET 2013
Am 01.01.2013 um 22:38 schrieb Makarius:
> Anyway, since the "smt" method seems to work right now, I propose to wire up a test where smt_certificates and smt_read_only_certificates are left unchanged if ISABELLE_FULL_TEST is enabled. Does that make sense, according to the meaning of these options? SMT/Z3 should run without any certificates getting in between.
I gave something like this a try:
Datum: Wed Jan 02 09:31:25 2013 +0100
Zusammenfassung: actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
> The conditionioning of the theories can be done with a little bit of ML for the options.
What I have right now (without any "ML conditioning") is that "SMT_Tests" is not run when the full tests are disabled. Then there are already several other files testing that SMT's certificate mechanism works. But I won't stop anybody if they want to change the setup so that "SMT_Tests" runs against certificates in non-full mode.
More information about the isabelle-dev