From 6d729f1f158ebc406262dad703b31470a42ea0a9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 11 Dec 2017 10:36:42 -0800
Subject: [PATCH] disable UHLT

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

diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index 8e5e556e3..dbb5ea123 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -208,7 +208,6 @@ namespace sat {
         m_to_delete.reset();
         for (unsigned i = m_pos.size() - 1; i-- > 0; ) {
             literal lit = m_pos[i];
-            SASSERT(scc.get_left(lit) < scc.get_left(last));
             int right2 = scc.get_right(lit);
             if (right2 > right) {
                 // lit => last, so lit can be deleted
@@ -345,10 +344,12 @@ namespace sat {
     bool asymm_branch::process_sampled(scc& scc, clause & c) {
         scoped_detach scoped_d(s, c);
         sort(scc, c);
+#if 0
         if (uhte(scc, c)) {
             scoped_d.del_clause();
             return false;
         }
+#endif
         return uhle(scoped_d, scc, c);        
     }