From 3f9b5bce99d0dcbc1b59fdb36d986bd73c2d83bf Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Thu, 17 May 2018 13:22:22 -0700
Subject: [PATCH] Remove debug function

---
 src/muz/spacer/spacer_context.cpp | 17 +++++++++--------
 src/muz/spacer/spacer_context.h   |  2 --
 2 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 7d8ffc0aa..eccc156de 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1001,6 +1001,14 @@ void pred_transformer::init_rules(decl2rel const& pts, expr_ref& init, expr_ref&
     }
 }
 
+static bool is_all_non_null(app_ref_vector const& v)
+{
+    for (unsigned i = 0; i < v.size(); ++i) {
+        if (!v[i]) { return false; }
+    }
+    return true;
+}
+
 void pred_transformer::init_rule(
     decl2rel const&      pts,
     datalog::rule const& rule,
@@ -1035,7 +1043,7 @@ void pred_transformer::init_rule(
         fml = mk_and (tail);
 
         ground_free_vars (fml, var_reprs, aux_vars, ut_size == 0);
-        SASSERT(check_filled(var_reprs));
+        SASSERT(is_all_non_null(var_reprs));
 
         expr_ref tmp(m);
         var_subst (m, false)(fml,
@@ -1074,13 +1082,6 @@ void pred_transformer::init_rule(
           tout << "\n";);
 }
 
-bool pred_transformer::check_filled(app_ref_vector const& v) const
-{
-    for (unsigned i = 0; i < v.size(); ++i) {
-        if (!v[i]) { return false; }
-    }
-    return true;
-}
 
 // create constants for free variables in tail.
 void pred_transformer::ground_free_vars(expr* e, app_ref_vector& vars,
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 9d3456f2b..0d4db2279 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -320,8 +320,6 @@ class pred_transformer {
     void simplify_formulas(tactic& tac, expr_ref_vector& fmls);
 
     // Debugging
-    bool check_filled(app_ref_vector const& v) const;
-
     void add_premises(decl2rel const& pts, unsigned lvl, datalog::rule& rule, expr_ref_vector& r);
 
     expr* mk_fresh_reach_case_var ();