NEWS
changeset 57241 7fca4159117f
parent 57237 bc51864c2ac4
child 57245 f6bf6d5341ee
     1.1 --- a/NEWS	Thu Jun 12 17:02:03 2014 +0200
     1.2 +++ b/NEWS	Thu Jun 12 17:02:03 2014 +0200
     1.3 @@ -382,9 +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". CVC3 is also supported as an oracle. Yices is no longer
     1.8 -    supported, because no version of the solver can handle both SMT-LIB 2 and
     1.9 -    quantifiers.
    1.10 +    called "smt2". CVC3 and CVC4 are also supported as oracles. Yices is no
    1.11 +    longer supported, because no version of the solver can handle both
    1.12 +    SMT-LIB 2 and quantifiers.
    1.13  
    1.14  * Sledgehammer:
    1.15    - New prover "z3_new" with support for Isar proofs