NEWS
changeset 57237 bc51864c2ac4
parent 57212 f25dad3d6144
child 57241 7fca4159117f
     1.1 --- a/NEWS	Thu Jun 12 17:02:02 2014 +0200
     1.2 +++ b/NEWS	Thu Jun 12 17:02:03 2014 +0200
     1.3 @@ -382,7 +382,9 @@
     1.4  * SMT module:
     1.5    * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
     1.6      and supports recent versions of Z3 (e.g., 4.3). The new proof method is
     1.7 -    called "smt2".
     1.8 +    called "smt2". CVC3 is also supported as an oracle. Yices is no longer
     1.9 +    supported, because no version of the solver can handle both SMT-LIB 2 and
    1.10 +    quantifiers.
    1.11  
    1.12  * Sledgehammer:
    1.13    - New prover "z3_new" with support for Isar proofs