[isabelle-dev] AFP: Session AVL-Trees broken

[Jasmin Blanchette]

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:

    Änderung:        50666:6f48853f08d5
    Marke:           tip
    Nutzer:          blanchet
    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.

Jasmin