From dff50715985ba2cb6ef0161c96b23b203582f40e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Apr 2020 17:03:26 -0700
Subject: [PATCH] compile

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/fp/horn_tactic.cpp     |  4 +---
 src/muz/spacer/spacer_util.cpp | 42 +++++++++++++++++-----------------
 src/util/min_cut.h             |  1 -
 3 files changed, 22 insertions(+), 25 deletions(-)

diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index 636de9075..a95fae07a 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -340,9 +340,7 @@ class horn_tactic : public tactic {
             g->reset();
             result.push_back(g.get());
             datalog::rule_set const& rules = m_ctx.get_rules();
-            datalog::rule_set::iterator it = rules.begin(), end = rules.end();
-            for (; it != end; ++it) {
-                datalog::rule* r = *it;
+            for (datalog::rule* r : rules) {
                 m_ctx.get_rule_manager().to_formula(*r, fml);
                 (*rep)(fml);
                 g->assert_expr(fml);
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 97a7262c2..dd7e2a6ab 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -28,44 +28,44 @@ Notes:
 #include <sstream>
 #include <algorithm>
 
+#include "util/util.h"
 #include "ast/ast.h"
 #include "ast/occurs.h"
 #include "ast/ast_pp.h"
-#include "ast/rewriter/bool_rewriter.h"
-#include "muz/base/dl_util.h"
-#include "ast/for_each_expr.h"
-#include "smt/params/smt_params.h"
-#include "model/model.h"
-#include "model/model_evaluator.h"
-#include "util/ref_vector.h"
-#include "ast/rewriter/rewriter.h"
-#include "ast/rewriter/rewriter_def.h"
-#include "util/util.h"
-#include "muz/spacer/spacer_manager.h"
-#include "muz/spacer/spacer_util.h"
-#include "ast/rewriter/expr_replacer.h"
-#include "model/model_smt2_pp.h"
 #include "ast/scoped_proof.h"
-#include "qe/qe_lite.h"
-#include "muz/spacer/spacer_qe_project.h"
-#include "model/model_pp.h"
+#include "ast/for_each_expr.h"
+#include "ast/rewriter/bool_rewriter.h"
 #include "ast/rewriter/expr_safe_replace.h"
-
 #include "ast/array_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/datatype_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
+#include "ast/rewriter/rewriter.h"
+#include "ast/rewriter/rewriter_def.h"
+#include "ast/rewriter/factor_equivs.h"
+#include "ast/rewriter/expr_replacer.h"
 
-#include "muz/spacer/spacer_legacy_mev.h"
+
+#include "smt/params/smt_params.h"
+#include "model/model.h"
+#include "model/model_evaluator.h"
+#include "model/model_smt2_pp.h"
+#include "model/model_pp.h"
+
+#include "qe/qe_lite.h"
 #include "qe/qe_mbp.h"
+#include "qe/qe_term_graph.h"
 
 #include "tactic/tactical.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/arith/propagate_ineqs_tactic.h"
 #include "tactic/arith/arith_bounds_tactic.h"
 
-#include "ast/rewriter/factor_equivs.h"
-#include "qe/qe_term_graph.h"
+#include "muz/base/dl_util.h"
+#include "muz/spacer/spacer_legacy_mev.h"
+#include "muz/spacer/spacer_qe_project.h"
+#include "muz/spacer/spacer_manager.h"
+#include "muz/spacer/spacer_util.h"
 
 namespace spacer {
 
diff --git a/src/util/min_cut.h b/src/util/min_cut.h
index 433670786..85b48e7a2 100644
--- a/src/util/min_cut.h
+++ b/src/util/min_cut.h
@@ -44,7 +44,6 @@ public:
     
 private:
 
-    typedef bool_vector bool_vector;
     struct edge { unsigned node; unsigned weight; edge(unsigned n, unsigned w): node(n), weight(w) {} edge(): node(0), weight(0) {} };
     typedef svector<edge> edge_vector;