From a2dddbd7a549e6529b089714210fdf7477367204 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 28 Feb 2019 14:28:03 -0800
Subject: [PATCH] check pb solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_config.cpp          | 20 +++++++-------------
 src/sat/sat_config.h            | 12 ------------
 src/sat/sat_model_converter.cpp |  7 +------
 3 files changed, 8 insertions(+), 31 deletions(-)

diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 6b8181886..78d93880c 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -191,20 +191,14 @@ namespace sat {
 
         // PB parameters
         s = p.pb_solver();
-        if (s == symbol("circuit")) 
-            m_pb_solver = PB_CIRCUIT;
-        else if (s == symbol("sorting")) 
-            m_pb_solver = PB_SORTING;
-        else if (s == symbol("totalizer")) 
-            m_pb_solver = PB_TOTALIZER;
-        else if (s == symbol("solver")) 
-            m_pb_solver = PB_SOLVER;
-        else if (s == symbol("segmented")) 
-            m_pb_solver = PB_SEGMENTED;
-        else if (s == symbol("binary_merge"))
-            m_pb_solver == PB_BINARY_MERGE;        
-        else 
+        if (s != symbol("circuit") &&
+            s != symbol("sorting") && 
+            s != symbol("totalizer") && 
+            s != symbol("solver") &&
+            s != symbol("segmented") &&
+            s != symbol("binary_merge")) {
             throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting, segmented, binary_merge");
+        }
 
         s = p.pb_resolve();
         if (s == "cardinality") 
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index e9895a051..5203b0838 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -52,15 +52,6 @@ namespace sat {
         BH_LRB
     };
 
-    enum pb_solver {
-        PB_SOLVER,
-        PB_CIRCUIT,
-        PB_SORTING,
-        PB_TOTALIZER,
-        PB_SEGMENTED,
-        PB_BINARY_MERGE
-    };
-
     enum pb_resolve {
         PB_CARDINALITY,
         PB_ROUNDING
@@ -183,9 +174,6 @@ namespace sat {
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
 
-    private:
-        pb_solver          m_pb_solver;
-
     };
 };
 
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index 577588305..60b758fec 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -221,12 +221,7 @@ namespace sat {
 
     void model_converter::add_elim_stack(entry & e) {
         e.m_elim_stack.push_back(stackv().empty() ? nullptr : alloc(elim_stack, stackv()));
-#if 0
-        if (!stackv().empty() && e.get_kind() == ATE) {
-            IF_VERBOSE(0, display(verbose_stream(), e) << "\n");
-        }
-#endif
-        for (auto const& s : stackv()) VERIFY(legal_to_flip(s.second.var()));
+        VERIFY(for (auto const& s : stackv()) VERIFY(legal_to_flip(s.second.var())));
         stackv().reset();
     }