From 8d0d123a4c99aa08a166bdff619d8220ca991eed Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 2 Jan 2014 01:45:34 -0800
Subject: [PATCH] pareto take 3

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/pb_preprocess_tactic.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp
index 0103c16cc..ae203b9c8 100644
--- a/src/tactic/core/pb_preprocess_tactic.cpp
+++ b/src/tactic/core/pb_preprocess_tactic.cpp
@@ -306,12 +306,15 @@ private:
     }
 
     void decompose(goal_ref const& g) {
+#if 0
+        // TBD
         for (unsigned i = 0; !g->inconsistent() && i < g->size(); ++i) {
             expr* e = g->form(i);
             if (pb.is_ge(e) && to_app(e)->get_num_args() > 20) {
                 // TBD: decompose inequality int smaller ones.
             }
         }
+#endif
     }
 
     void process_vars(unsigned i, goal_ref const& g) {