1.1 --- a/NEWS	Sun May 04 18:50:42 2014 +0200
     1.2 +++ b/NEWS	Sun May 04 18:53:58 2014 +0200
     1.3 @@ -352,7 +352,10 @@
     1.4  * New internal SAT solver "dpll_p" that produces models and proof traces.
     1.5    This solver replaces the internal SAT solvers "enumerate" and "dpll".
     1.6    Applications that explicitly used one of these two SAT solvers should
     1.7 -  use "dpll_p" instead. Minor INCOMPATIBILITY.
     1.8 +  use "dpll_p" instead. In addition, "dpll_p" is now the default SAT
     1.9 +  solver for the "sat" and "satx" proof methods and corresponding tactics;
    1.10 +  the old default can be restored using
    1.11 +  "declare [[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY.
    1.12  
    1.13  * SMT module:
    1.14    * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2