diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index a99ec6b1e..67aa3d810 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -1,5 +1,36 @@
 RELEASE NOTES
 
+Version 4.8.0
+=============
+
+- New requirements:
+  - A breaking change to the API is that parsers for SMT-LIB2 formulas return a vector of 
+    formulas as opposed to a conjunction of formulas. The vector of formulas correspond to 
+    the set of "assert" instructions in the SMT-LIB input.
+
+- New features
+   - A parallel mode is available for select theories, including QF_BV. 
+     By setting parallel.enable=true Z3 will spawn a number of worker threads proportional to the 
+     number of available CPU cores to apply cube and conquer solving on the goal.
+   - The SAT solver by default handle cardinality and PB constraints using a custom plugin 
+     that operates directly on cardinality and PB constraints.
+   - A "cube" interface is exposed over the solver API. 
+   - Model conversion is first class over the textual API, such that subgoals created from running a 
+     solver can be passed in text files and a model for the original formula can be recreated from the result.
+   - This has also led to changes in how models are tracked over tactic subgoals. The API for 
+     extracting models from apply_result have been replaced.
+   - An optional mode handles xor constraints using a custom xor propagator. 
+     It is off by default and its value not demonstrated.
+   - The SAT solver includes new inprocessing technques that are available during simplification. 
+     It performs asymmetric tautology elimination by default, and one can turn on more powerful inprocessing techniques 
+     (known as ACCE, ABCE, CCE). Asymmetric branching also uses features introduced in Lingeling by exploiting binary implication graphs.
+     Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged
+     as lemmas (redundant) and are garbage collected if their glue level is high.
+
+- Removed features:
+  - long deprecated API functions have been removed from z3_api.h
+
+
 Version 4.7.1
 =============
 
diff --git a/src/util/lp/bound_propagator.h b/src/util/lp/bound_propagator.h
deleted file mode 100644
index 128973c12..000000000
--- a/src/util/lp/bound_propagator.h
+++ /dev/null
@@ -1,27 +0,0 @@
-/*
-  Copyright (c) 2017 Microsoft Corporation
-  Author: Lev Nachmanson
-*/
-#pragma once
-#include "util/lp/lp_settings.h"
-namespace lp {
-class lar_solver;
-class bound_propagator {
-    std::unordered_map<unsigned, unsigned> m_improved_low_bounds; // these maps map a column index to the corresponding index in ibounds
-    std::unordered_map<unsigned, unsigned> m_improved_upper_bounds;
-    lar_solver & m_lar_solver;
-public:
-    vector<implied_bound> m_ibounds;
-public:
-    bound_propagator(lar_solver & ls);
-    column_type get_column_type(unsigned) const;
-    const impq & get_low_bound(unsigned) const;
-    const impq & get_upper_bound(unsigned) const;
-    void try_add_bound(mpq  v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict);
-    virtual bool bound_is_interesting(unsigned vi,
-                                      lp::lconstraint_kind kind,
-                                      const rational & bval) {return true;}
-    unsigned number_of_found_bounds() const { return m_ibounds.size(); }
-    virtual void consume(mpq const& v, unsigned j) { std::cout << "doh\n"; }
-};
-}