From 412eee0dace45c2d7c13a6fbdc0a6d83e7a021d2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 22 Jan 2019 18:12:39 -0800
Subject: [PATCH] throttle number of rounds of ba simplification

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/ba_solver.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 47fc2c27f..7315f913b 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2837,7 +2837,7 @@ namespace sat {
 
     void ba_solver::simplify() {        
         if (!s().at_base_lvl()) s().pop_to_base_level();
-        unsigned trail_sz;
+        unsigned trail_sz, count = 0;
         do {
             trail_sz = s().init_trail_size();
             m_simplify_change = false;
@@ -2855,8 +2855,9 @@ namespace sat {
             cleanup_clauses();
             cleanup_constraints();
             update_pure();
+            ++count;
         }        
-        while (m_simplify_change || trail_sz < s().init_trail_size());
+        while (count < 10 && (m_simplify_change || trail_sz < s().init_trail_size()));
 
         IF_VERBOSE(1, verbose_stream() << "(ba.simplify"
                    << " :vars " << s().num_vars() - trail_sz