diff --git a/src/ast/converters/generic_model_converter.cpp b/src/ast/converters/generic_model_converter.cpp
index 50c3b071a..9adb9ee4b 100644
--- a/src/ast/converters/generic_model_converter.cpp
+++ b/src/ast/converters/generic_model_converter.cpp
@@ -28,11 +28,6 @@ Notes:
 #include "model/model_v2_pp.h"
 #include "model/model_evaluator.h"
 
-
-generic_model_converter::~generic_model_converter() {
-}
-
-
 void generic_model_converter::add(func_decl * d, expr* e) {
     VERIFY(e);
     VERIFY(d->get_range() == e->get_sort());
diff --git a/src/ast/converters/generic_model_converter.h b/src/ast/converters/generic_model_converter.h
index 0706b181f..cf551c92a 100644
--- a/src/ast/converters/generic_model_converter.h
+++ b/src/ast/converters/generic_model_converter.h
@@ -41,8 +41,6 @@ private:
 public:
     generic_model_converter(ast_manager & m, char const* orig) : m(m), m_orig(orig) {}
     
-    ~generic_model_converter() override;
-    
     void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); }
 
     void hide(func_decl * f) { m_entries.push_back(entry(f, nullptr, m, HIDE)); }
diff --git a/src/smt/tactic/smt_tactic_core.h b/src/smt/tactic/smt_tactic_core.h
index f89b3c649..7c6fa97f7 100644
--- a/src/smt/tactic/smt_tactic_core.h
+++ b/src/smt/tactic/smt_tactic_core.h
@@ -24,7 +24,6 @@ Notes:
 #include "tactic/goal.h"
 
 class tactic;
-class filter_model_converter;
 
 tactic * mk_smt_tactic_core(ast_manager& m, params_ref const & p = params_ref(), symbol const& logic = symbol::null);
 // syntax sugar for using_params(mk_smt_tactic(), p) where p = (:auto_config, auto_config)
diff --git a/src/tactic/filter_model_converter.h b/src/tactic/filter_model_converter.h
deleted file mode 100644
index 56dda91db..000000000
--- a/src/tactic/filter_model_converter.h
+++ /dev/null
@@ -1,50 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
-    filter_model_converter.h
-
-Abstract:
-
-    Filter decls from a model
-
-Author:
-
-    Leonardo (leonardo) 2011-05-06
-
-Notes:
-
---*/
-#pragma once
-
-#include "tactic/model_converter.h"
-
-class filter_model_converter : public model_converter {
-    func_decl_ref_vector  m_decls;
-public:
-    filter_model_converter(ast_manager & m):m_decls(m) {}
-    
-    ~filter_model_converter() override;
-    
-    ast_manager & m() const { return m_decls.get_manager(); }
-    
-    void operator()(model_ref & md, unsigned goal_idx) override;
-
-    virtual void operator()(svector<symbol> & labels, unsigned goal_idx);
-    
-    void operator()(model_ref & md) override { operator()(md, 0); } // TODO: delete
-
-    void cancel() override {}
-
-    void display(std::ostream & out) override;
-
-    void insert(func_decl * d) {
-        m_decls.push_back(d);
-    }
-
-    model_converter * translate(ast_translation & translator) override;
-};
-
-typedef ref<filter_model_converter> filter_model_converter_ref;
-
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index e489a1100..b6fe76f6a 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -159,9 +159,7 @@ void goal::quick_process(bool save_first, expr_ref& f, expr_dependency * d) {
     while (!todo.empty()) {
         if (m_inconsistent)
             return;
-        expr_pol p = todo.back();
-        expr * curr = p.first;
-        bool   pol = p.second;
+        auto [curr, pol] = todo.back();
         todo.pop_back();
         if (pol && m().is_and(curr)) {
             app * t = to_app(curr);