2014-06-12 blanchet 2014-06-12 adapted examples to changes in SMT triggers
2014-04-25 blanchet 2014-04-25 use Z3 4.3.2 to fix most FIXMEs
2014-03-13 blanchet 2014-03-13 updated SMT2 certificates
2014-03-13 blanchet 2014-03-13 updated SMT example certificates
2014-03-13 blanchet 2014-03-13 use 'smt2' in SMT examples as much as currently possible
2014-02-14 blanchet 2014-02-14 merged '' and ''
2013-01-02 blanchet 2013-01-02 actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
2012-06-04 boehmes 2012-06-04 restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
2012-03-27 boehmes 2012-03-27 dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
2012-03-27 blanchet 2012-03-27 renamed "smt_fixed" to "smt_read_only_certificates"
2012-03-26 blanchet 2012-03-26 reintroduced broken proofs and regenerated certificates
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-01-03 blanchet 2012-01-03 regenerate SMT example certificates, to reflect "set" type constructor
2011-12-24 haftmann 2011-12-24 commented out examples which choke on strict set/pred distinction
2011-11-07 boehmes 2011-11-07 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
2011-07-18 boehmes 2011-07-18 allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
2011-04-08 boehmes 2011-04-08 fixed eta-expansion: use correct order to apply new bound variables
2011-04-08 boehmes 2011-04-08 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
2011-04-08 boehmes 2011-04-08 corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
2011-02-21 boehmes 2011-02-21 added test cases with quantifier occurring in first-order term positions
2011-01-17 boehmes 2011-01-17 made Z3 the default SMT solver again
2010-12-20 boehmes 2010-12-20 updated SMT certificates
2010-12-19 boehmes 2010-12-19 updated SMT certificates
2010-12-15 boehmes 2010-12-15 updated SMT certificates
2010-11-24 boehmes 2010-11-24 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
2010-11-12 boehmes 2010-11-12 look for certificates relative to the theory
2010-10-29 boehmes 2010-10-29 introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
2010-10-26 boehmes 2010-10-26 changed SMT configuration options; updated SMT certificates
2010-05-27 boehmes 2010-05-27 use Z3's builtin support for div and mod
2010-05-26 boehmes 2010-05-26 hide constants and types introduced by SMT, simplified SMT patterns syntax, added examples for SMT patterns
2010-05-12 boehmes 2010-05-12 updated SMT certificates
2010-05-12 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-05-12 boehmes 2010-05-12 integrated SMT into the HOL image