diff --git a/src/ast/proofs/proof_utils.cpp b/src/ast/proofs/proof_utils.cpp
index b6c8b58d7..58500cb79 100644
--- a/src/ast/proofs/proof_utils.cpp
+++ b/src/ast/proofs/proof_utils.cpp
@@ -20,10 +20,10 @@ Revision History:
 #include "ast/ast_pp.h"
 #include "ast/proofs/proof_utils.h"
 #include "ast/proofs/proof_checker.h"
+#include "ast/rewriter/var_subst.h"
 #include "util/container_util.h"
 
 
-
 proof_post_order::proof_post_order(proof* root, ast_manager& manager) : m(manager)
 {m_todo.push_back(root);}
 
@@ -336,7 +336,6 @@ void reduce_hypotheses(proof_ref &pr) {
 
 
 #include "ast/ast_smt2_pp.h"
-#include "ast/rewriter/var_subst.h"
 
 class reduce_hypotheses0 {
     typedef obj_hashtable<expr> expr_set;
diff --git a/src/ast/proofs/proof_utils.h b/src/ast/proofs/proof_utils.h
index 4152bca92..9823acb92 100644
--- a/src/ast/proofs/proof_utils.h
+++ b/src/ast/proofs/proof_utils.h
@@ -20,6 +20,7 @@ Revision History:
 #ifndef PROOF_UTILS_H_
 #define PROOF_UTILS_H_
 #include "ast/ast.h"
+#include "ast/rewriter/bool_rewriter.h"
 
 /*
  * iterator, which traverses the proof in depth-first post-order.
@@ -66,7 +67,6 @@ public:
 
 };
 
-#include "ast/rewriter/bool_rewriter.h"
 class elim_aux_assertions {
 
     static bool matches_fact(expr_ref_vector &args, expr* &match) {
diff --git a/src/muz/spacer/spacer_virtual_solver.cpp b/src/muz/spacer/spacer_virtual_solver.cpp
index 891256eed..89b9fb531 100644
--- a/src/muz/spacer/spacer_virtual_solver.cpp
+++ b/src/muz/spacer/spacer_virtual_solver.cpp
@@ -244,7 +244,6 @@ void virtual_solver::refresh()
     m_head = 0;
 }
 
-#ifdef NOT_USED_ANYWHERE
 void virtual_solver::reset()
 {
     SASSERT(!m_pushed);
@@ -252,7 +251,6 @@ void virtual_solver::reset()
     m_assertions.reset();
     m_factory.refresh();
 }
-#endif
 
 void virtual_solver::get_labels(svector<symbol> &r)
 {
diff --git a/src/muz/spacer/spacer_virtual_solver.h b/src/muz/spacer/spacer_virtual_solver.h
index 3ccd89ef5..fed64c589 100644
--- a/src/muz/spacer/spacer_virtual_solver.h
+++ b/src/muz/spacer/spacer_virtual_solver.h
@@ -91,9 +91,7 @@ public:
     virtual void set_produce_models(bool f);
     virtual bool get_produce_models();
     virtual smt_params &fparams();
-#ifdef NOT_USED_ANYWHERE
     virtual void reset();
-#endif
     virtual void set_progress_callback(progress_callback *callback)
     {UNREACHABLE();}
 
@@ -135,6 +133,9 @@ private:
 
 
     void refresh();
+
+    smt_params &fparams() { return m_fparams; }
+
 public:
     virtual_solver_factory(ast_manager &mgr, smt_params &fparams);
     virtual ~virtual_solver_factory();
@@ -145,7 +146,6 @@ public:
     void collect_param_descrs(param_descrs &r) { /* empty */ }
     void set_produce_models(bool f) { m_fparams.m_model = f; }
     bool get_produce_models() { return m_fparams.m_model; }
-    smt_params &fparams() { return m_fparams; }
 };
 
 }
diff --git a/src/util/container_util.h b/src/util/container_util.h
new file mode 100644
index 000000000..7bbc3fb08
--- /dev/null
+++ b/src/util/container_util.h
@@ -0,0 +1,121 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    container_util.h
+
+Abstract:
+
+    Useful functions for containers
+
+Author:
+
+    Krystof Hoder, Nikolaj Bjorner 2017-10-24
+
+Revision History:
+
+    Extracted from dl_util.h
+
+--*/
+
+#ifndef CONTAINUR_UTIL_H
+#define CONTAINER_UTIL_H_
+
+// -----------------------------------
+//
+// container functions
+//
+// -----------------------------------
+
+template<class Set1, class Set2>
+    void set_intersection(Set1 & tgt, const Set2 & src) {
+    svector<typename Set1::data> to_remove;
+    for (Set1::data itm : tgt) 
+        if (!src.contains(itm)) 
+            to_remove.push_back(itm);
+    while (!to_remove.empty()) {
+        tgt.remove(to_remove.back());
+        to_remove.pop_back();
+    }
+}
+
+template<class Set>
+void set_difference(Set & tgt, const Set & to_remove) {
+    for (auto const& itm : to_remove) 
+        tgt.remove(itm);
+}
+
+template<class Set1, class Set2>
+void set_union(Set1 & tgt, const Set2 & to_add) {
+    for (auto const& itm : to_add) 
+        tgt.insert(itm);
+}
+
+template<class T>
+void unite_disjoint_maps(T & tgt, const T & src) {
+    for (auto const& kv : src) {
+        SASSERT(!tgt.contains(kv.m_key));
+        tgt.insert(kv.m_key, kv.m_value);
+    }
+}
+
+template<class T, class U>
+void collect_map_range(T & acc, const U & map) {
+    for (auto const& kv : map) 
+        acc.push_back(kv.m_value);
+}
+
+
+template<class T>
+void print_container(const T & begin, const T & end, std::ostream & out) {
+    T it = begin;
+    out << "(";
+    bool first = true;
+    for(; it!=end; ++it) {
+        if(first) { first = false; } else { out << ","; }
+        out << (*it);
+    }
+    out << ")";
+}
+
+template<class T>
+void print_container(const T & cont, std::ostream & out) {
+    print_container(cont.begin(), cont.end(), out);
+}
+
+template<class T, class M>
+void print_container(const ref_vector<T,M> & cont, std::ostream & out) {
+    print_container(cont.c_ptr(), cont.c_ptr() + cont.size(), out);
+}
+
+template<class T>
+void print_map(const T & cont, std::ostream & out) {
+    out << "(";
+    bool first = true;
+    for (auto const& kv : cont) {
+        if (first) { first = false; } else { out << ","; }
+        out << kv.m_key << "->" << kv.m_value;
+    }
+    out << ")";
+}
+
+template<class It, class V> 
+unsigned find_index(const It & begin, const It & end, const V & val) {
+    for (unsigned idx = 0, It it = begin; it != end; it++, idx++) {
+        if (*it == val) {
+            return idx;
+        }
+    }
+    return UINT_MAX;
+}
+
+template<class T, class U>
+bool containers_equal(const T & begin1, const T & end1, const U & begin2, const U & end2) {
+    T it1 = begin1;
+    U it2 = begin2;
+    for (; it1 != end1 && it2 != end2 && *it1 == *it2; ++it1, ++it2) {};
+    return it1 == end1 && it2 == end2;
+}
+
+#endif