Update news (cvc5#10434)

In preparation for 1.1.2.

Author: ajreynol

NEWS.md

@@ -1,21 +1,45 @@
 This file contains a summary of important user-visible changes.
 
+cvc5 1.1.2
+==========
+
 ## New Features
 
-- Added support for nullable sorts and lift operator to the theory of datatypes.
+- Added support for **nullable** sorts and lift operator to the theory of **datatypes**.
+- Adds a new strategy `--sub-cbqi` (disabled by default) for **quantifier
+  instantiation** which uses subsolvers to compute unsat cores of instantiations
+  that are used in proofs of unsatisfiability.
 
 ## Changes
 
+- SAT clauses are no longer marked as removable in MiniSat. This change
+  **improves performance** overall on quantifier-free logics with arithmetic and
+  strings.
 - **API**
   * Functions `kindToString(Kind)` and `sortKindToString(SortKind)` are now
     deprecated and replaced by `std::to_string(Kind)` and
     `std::to_string(SortKind)`. They will be removed in the next minor release.
-
+- Minor changes to the output format for proofs. Proofs in the AletheLF
+  proof format generated by cvc5 now correspond directly to their representation
+  in proof objects obtained in via the API (the `Proof` class). Moreover,
+  proofs now use SMT-LIB compliant syntax for quantified formulas and unary
+  arithmetic negation.
+- The option `--safe-options` now disallows cases where more than one regular
+  option is used.
+- Fixes the parsing of `define-fun-rec` and `define-funs-rec` in interactive
+  mode.
 - Renamed `bag.duplicate_removal` to `bag.setof`.
 
 cvc5 1.1.1
 ==========
 
+## New Features
+
+- Added support for **forward declarations** (feature `:fwd-decls`) in **SyGuS**
+  inputs. This allows functions-to-synthesize to include previous
+  functions-to-synthesize in their grammars. This feature is enabled by default
+  for all SyGuS inputs.
+
 ## Changes
 
 - Fixed a bug when piping input from stdin, which caused cvc5 to have degraded