diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg
index 423ce486e..ff4590afa 100644
--- a/src/params/smt_parallel_params.pyg
+++ b/src/params/smt_parallel_params.pyg
@@ -4,5 +4,6 @@ def_module_params('smt_parallel',
                   params=(
                         ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'),
                         ('sls', BOOL, False, 'add sls-tactic as a separate worker thread outside the search tree parallelism'),
+			('failed_literal_backbones', BOOL, False, 'use failed literal backbone test'),
                         ('num_global_bb_threads', UINT, 0, 'default is 0 (off), can configure to 1 (negative mode only) or 2 (negative and positive mode) separate worker thread(s) outside the search tree parallelism'),
               ))
\ No newline at end of file
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index b0c4a88db..6c316fae5 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -66,16 +66,14 @@ namespace smt {
 
 namespace smt {
 
-    static bool is_cancellation_exception(char const* msg) {
-        return msg &&
-            (strstr(msg, "canceled") != nullptr ||
-             strstr(msg, "cancelled") != nullptr);
+    static bool is_cancellation_exception(char const *msg) {
+        return msg && (strstr(msg, "canceled") != nullptr || strstr(msg, "cancelled") != nullptr);
     }
 
     void parallel::sls_worker::run() {
         ptr_vector<expr> assertions;
         p.ctx.get_assertions(assertions);
-        for (expr* e : assertions)
+        for (expr *e : assertions)
             m_sls->assert_expr(m_g2l(e));
 
         lbool res = l_undef;
@@ -83,8 +81,7 @@ namespace smt {
             if (!m.inc())
                 return;
             res = m_sls->check();
-        } 
-        catch (z3_exception& ex) {
+        } catch (z3_exception &ex) {
             // Cancellation is normal in portfolio mode
             if (m.limit().is_canceled()) {
                 IF_VERBOSE(1, verbose_stream() << "SLS worker canceled\n");
@@ -102,7 +99,7 @@ namespace smt {
             return;
         }
 
-        if (res == l_true) {         
+        if (res == l_true) {
             IF_VERBOSE(2, verbose_stream() << "SLS worker found SAT\n");
             model_ref mdl = m_sls->get_model();
             b.set_sat(m_l2g, *mdl);
@@ -110,6 +107,94 @@ namespace smt {
     }
 
     void parallel::backbones_worker::run() {
+        if (m_use_failed_literal_test)
+            run_failed_literal_mode();
+        else 
+            run_batch_mode();
+    }    
+
+    lbool parallel::backbones_worker::check_sat(expr_ref_vector const &asms) {
+        lbool r = l_undef;
+        try {
+            r = ctx->check(asms.size(), asms.data());
+        } catch (z3_error &err) {
+            if (!m.limit().is_canceled())
+                b.set_exception(err.error_code());
+        } catch (z3_exception &ex) {
+            if (!m.limit().is_canceled() && !is_cancellation_exception(ex.what()))
+                b.set_exception(ex.what());
+        } catch (...) {
+            if (!m.limit().is_canceled())
+                b.set_exception("unknown exception");
+        }
+        return r;
+    }
+
+    void parallel::backbones_worker::run_failed_literal_mode() {
+        ctx->get_fparams().m_max_conflicts = 10;
+        auto num_atoms = ctx->get_num_bool_vars();
+        uint_set units;
+        for (unsigned v = 0; v < num_atoms && m.inc(); ++v)
+            if (ctx->get_assignment(v) != l_undef && ctx->get_assign_level(v) == ctx->m_base_lvl)
+                units.insert(v);
+        while (m.inc()) {
+            for (unsigned v = 0; v < num_atoms && m.inc(); ++v) {
+                if (units.contains(v))
+                    continue;
+                expr_ref e(ctx->bool_var2expr(v), m);
+                if (!e)
+                    continue;
+                if (m.is_or(e) || m.is_ite(e))
+                    continue;
+                if (ctx->get_assignment(v) != l_undef && ctx->get_assign_level(v) == ctx->m_base_lvl) {
+                    bool is_true = ctx->get_assignment(v) == l_true;
+                    IF_VERBOSE(2, verbose_stream() << "backbone on trail " << e << "\n");
+                    units.insert(v);
+                    if (!is_true)
+                        e = m.mk_not(e);
+                    if (b.collect_global_backbone(m_l2g, e))
+                        m_stats.m_backbones_found++;                                            
+                    continue;
+                }
+                auto r = probe_literal(v, units, e);
+                if (r != l_undef)
+                    break;
+                if (units.contains(v))
+                    continue;
+                e = mk_not(e);
+                r = probe_literal(v, units, e);
+                if (r != l_undef)
+                    break;
+            }
+        }
+    }
+
+    lbool parallel::backbones_worker::probe_literal(bool_var v, uint_set& units, expr *e) {
+        asms.push_back(e);
+        auto r = check_sat(asms);
+        asms.pop_back();
+        if (r == l_false) {
+            if (!ctx->unsat_core().contains(e)) {
+                b.set_unsat(m_l2g, ctx->unsat_core());
+                return l_false;
+            }
+            IF_VERBOSE(2, verbose_stream() << "failed literal " << mk_bounded_pp(e, m) << "\n");
+            expr_ref not_e(mk_not(m, e), m);
+            if (b.collect_global_backbone(m_l2g, not_e))
+                m_stats.m_backbones_found++;
+            units.insert(v);
+            r = l_undef;
+        }
+        if (r == l_true) {
+            model_ref mdl;
+            ctx->get_model(mdl);
+            b.set_sat(m_l2g, *mdl);
+        }
+        return r;
+    }
+
+
+    void parallel::backbones_worker::run_batch_mode() {
         bb_candidates bb_candidates;
         while (m.inc()) {
             if (!b.wait_for_backbone_job(id, m_g2l, bb_candidates, m.limit()))
@@ -199,20 +284,7 @@ namespace smt {
                     unsigned base_asms_sz = asms.size();
                     for (expr* a : bb_asms)
                         asms.push_back(a);
-
-                    lbool r = l_undef;
-                    try {
-                        r = ctx->check(asms.size(), asms.data());
-                    } catch (z3_error &err) {
-                        if (!m.limit().is_canceled())
-                            b.set_exception(err.error_code());
-                    } catch (z3_exception &ex) {
-                        if (!m.limit().is_canceled() && !is_cancellation_exception(ex.what()))
-                            b.set_exception(ex.what());
-                    } catch (...) {
-                        if (!m.limit().is_canceled())
-                            b.set_exception("unknown exception");
-                    }
+                    lbool r = check_sat(asms);
                     asms.shrink(base_asms_sz);
 
                     if (!m.inc()) 
@@ -506,7 +578,7 @@ namespace smt {
 
         smt_parallel_params pp(p.ctx.m_params);
         m_config.m_inprocessing = pp.inprocessing();
-        m_config.m_global_backbones = pp.num_global_bb_threads() > 0;
+        m_config.m_global_backbones = pp.num_global_bb_threads() > 0 && !pp.failed_literal_backbones();
     }
 
     parallel::sls_worker::sls_worker(parallel& p)
@@ -529,6 +601,7 @@ namespace smt {
 
         smt_parallel_params pp(p.ctx.m_params);
         m_num_global_bb_threads = pp.num_global_bb_threads();
+        m_use_failed_literal_test = pp.failed_literal_backbones();
     }
 
     parallel::bb_candidates parallel::worker::find_backbone_candidates(unsigned k) {
diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h
index 1e4470ec4..abf098de9 100644
--- a/src/smt/smt_parallel.h
+++ b/src/smt/smt_parallel.h
@@ -304,11 +304,16 @@ namespace smt {
             ast_translation m_g2l, m_l2g;
             unsigned m_bb_chunk_size = 20;
             unsigned m_bb_conflicts_per_chunk = 1000;
+            bool m_use_failed_literal_test;
             stats m_stats;
             bb_mode m_mode;
             unsigned m_num_global_bb_threads = 1; // used to toggle behavior when testing bb candidates 
             unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share
             bool check_backbone(expr* bb_candidate);
+            void run_batch_mode();
+            void run_failed_literal_mode();
+            lbool check_sat(expr_ref_vector const &asms);
+            lbool probe_literal(bool_var v, uint_set& units, expr *e);
         public:
             backbones_worker(unsigned id, parallel &p, expr_ref_vector const &_asms);
             void cancel();