diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h
index 219f3ede8..f7a9a8fe9 100644
--- a/src/api/z3_optimization.h
+++ b/src/api/z3_optimization.h
@@ -71,7 +71,6 @@ extern "C" {
     */
     unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id);
 
-
     /**
        \brief Add a maximization constraint.
        \param c - context
@@ -91,7 +90,6 @@ extern "C" {
     */
     unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t);
 
-
     /**
        \brief Create a backtracking point.
 
@@ -198,7 +196,7 @@ extern "C" {
     Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o);
 
     /**
-       \brief Parse an SMT-LIB2 string with assertions, 
+       \brief Parse an SMT-LIB2 string with assertions,
        soft constraints and optimization objectives.
        Add the parsed constraints and objectives to the optimization context.
 
@@ -210,13 +208,11 @@ extern "C" {
     */
     void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s);
 
-
     /**
-       \brief Parse an SMT-LIB2 file with assertions, 
+       \brief Parse an SMT-LIB2 file with assertions,
        soft constraints and optimization objectives.
        Add the parsed constraints and objectives to the optimization context.
 
-
        \param c - context.
        \param o - optimize context.
        \param s - string containing SMT2 specification.
@@ -225,7 +221,6 @@ extern "C" {
     */
     void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s);
 
-
     /**
        \brief Return a string containing a description of parameters accepted by optimize.
 
@@ -240,7 +235,6 @@ extern "C" {
     */
     Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d);
 
-
     /**
        \brief Return the set of asserted formulas on the optimization context.
 
@@ -251,15 +245,14 @@ extern "C" {
     /**
        \brief Return objectives on the optimization context.
        If the objective function is a max-sat objective it is returned
-       as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...)       
-       If the objective function is entered as a maximization objective, then return the corresponding minimizaiton
-       objective. In this way the resulting objective function is always returned as a minimization objective.
+       as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...)
+       If the objective function is entered as a maximization objective, then return
+       the corresponding minimization objective. In this way the resulting objective
+       function is always returned as a minimization objective.
 
        def_API('Z3_optimize_get_objectives', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))
     */
     Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o);
-    
-        
 
     /*@}*/
     /*@}*/
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index b6c85c159..53c20b253 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -183,7 +183,6 @@ private:
             return;
         }
         filter_model_converter filter(m);
-        func_decl_ref_vector const& fns = m_bv_fns;
         for (unsigned i = 0; i < m_bv_fns.size(); ++i) {
             filter.insert(m_bv_fns[i]);
         }