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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
