diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index e8e8471c0..4d7377c3b 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -41,6 +41,8 @@ namespace polysat {
         scoped_ptr<std::ostream> m_out = nullptr;
         unsigned m_conflicts = 0;
 
+        friend class conflict;
+
         std::ostream& out() {
             SASSERT(m_out);
             return *m_out;
@@ -52,13 +54,15 @@ namespace polysat {
 
     public:
         void begin_conflict() {
+            ++m_conflicts;
+            LOG("Begin CONFLICT #" << m_conflicts);
             m_used_constraints.reset();
             m_used_vars.reset();
             if (!m_out)
                 m_out = alloc(std::ofstream, "conflicts.txt");
             else
                 out() << "\n\n\n\n\n\n\n\n\n\n\n\n";
-            out() << "CONFLICT #" << ++m_conflicts << "\n";
+            out() << "CONFLICT #" << m_conflicts << "\n";
         }
 
         void log_inference(conflict const& core, inference const* inf) {
@@ -72,6 +76,8 @@ namespace polysat {
             for (auto const& c : core) {
                 out_indent() << c.blit() << ": " << c << '\n';
                 m_used_constraints.insert(c.blit().index());
+                for (pvar v : c->vars())
+                    m_used_vars.insert(v);
             }
             for (auto v : core.vars()) {
                 out_indent() << "v" << v << " := " << core.s.get_value(v) << "\n";
@@ -86,12 +92,17 @@ namespace polysat {
             out().flush();
         }
 
-        void log_lemma(clause_builder const& cb) {
+        void log_lemma(solver const& s, clause_builder const& cb) {
             out() << hline() << "\nLemma:";
             for (auto const& lit : cb)
                 out() << " " << lit;
             out() << "\n";
+            for (auto const& lit : cb)
+                out_indent() << lit << ": " << s.lit2cnstr(lit) << '\n';
             out().flush();
+
+            // if (m_conflicts == 9)
+            //     std::exit(0);
         }
 
         void end_conflict(search_state const& search, viable const& v) {
@@ -104,6 +115,7 @@ namespace polysat {
             for (pvar var : m_used_vars)
                 out_indent() << "v" << std::setw(3) << std::left << var << ": " << viable::var_pp(v, var) << "\n";
             out().flush();
+            LOG("End CONFLICT #" << m_conflicts);
         }
 
         bool is_relevant(search_item const& item) const {
@@ -118,6 +130,11 @@ namespace polysat {
         }
     };
 
+    void conflict::log_var(pvar v) {
+        if (m_logger)
+            m_logger->m_used_vars.insert(v);
+    }
+
     conflict::conflict(solver& s): s(s) {
         ex_engines.push_back(alloc(ex_polynomial_superposition, s));
         ex_engines.push_back(alloc(eq_explain, s));
@@ -177,6 +194,7 @@ namespace polysat {
             unset_mark(c);
         m_literals.reset();
         m_vars.reset();
+        m_var_occurrences.reset();
         m_bail_vars.reset();
         m_conflict_var = null_var;
         m_bailout = false;
@@ -252,6 +270,11 @@ namespace polysat {
         SASSERT(!c->vars().empty());
         set_mark(c);
         m_literals.insert(c.blit().index());
+        for (pvar v : c->vars()) {
+            if (v >= m_var_occurrences.size())
+                m_var_occurrences.resize(v + 1, 0);
+            m_var_occurrences[v]++;
+        }
     }
 
     void conflict::propagate(signed_constraint c) {
@@ -302,6 +325,10 @@ namespace polysat {
     void conflict::remove(signed_constraint c) {
         unset_mark(c);       
         m_literals.remove(c.blit().index());
+        for (pvar v : c->vars()) {
+            if (v < m_var_occurrences.size())
+                m_var_occurrences[v]--;
+        }
     }
 
     void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises) {
@@ -314,6 +341,7 @@ namespace polysat {
     }
 
     bool conflict::contains(sat::literal lit) const {
+        SASSERT(lit != sat::null_literal);
         return m_literals.contains(lit.index());
     }
 
@@ -337,8 +365,6 @@ namespace polysat {
         //       clause: x \/ u \/ v
         //       resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v
 
-        SASSERT(lit != sat::null_literal);
-        SASSERT(~lit != sat::null_literal);
         SASSERT(contains(lit));
         SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
         SASSERT(!contains(~lit));
@@ -368,8 +394,6 @@ namespace polysat {
         // The reason for lit is conceptually:
         //    x1 = v1 /\ ... /\ xn = vn ==> lit
 
-        SASSERT(lit != sat::null_literal);
-        SASSERT(~lit != sat::null_literal);
         SASSERT(contains(lit));
         SASSERT(!contains(~lit));
 
@@ -411,7 +435,7 @@ namespace polysat {
         s.decay_activity();
 
         if (m_logger)
-            m_logger->log_lemma(lemma);
+            m_logger->log_lemma(s, lemma);
 
         return lemma;
     }
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index 109ef701c..ef7f4e137 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -101,8 +101,8 @@ namespace polysat {
     /** Conflict state, represented as core (~negation of clause). */
     class conflict {
         solver& s;
-        // signed_constraints m_constraints;   // new constraints used as premises
         indexed_uint_set m_literals;        // set of boolean literals in the conflict
+        unsigned_vector m_var_occurrences;  // for each variable, the number of constraints in m_literals that contain it
         uint_set m_vars;                    // variable assignments used as premises
         uint_set m_bail_vars;
 
@@ -137,6 +137,7 @@ namespace polysat {
         /// Log inference at the current state.
         void log_inference(inference const& inf);
         void log_inference(char const* name) { log_inference(inference_named(name)); }
+        void log_var(pvar v);
         /// Log relevant part of search state and viable.
         void end_conflict();
 
@@ -149,6 +150,8 @@ namespace polysat {
         bool empty() const;
         void reset();
 
+        bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; }
+
         bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
         bool is_marked(signed_constraint c) const;
         bool is_marked(sat::bool_var b) const;
diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index a902a7c63..eb3c9417c 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -150,7 +150,9 @@ namespace polysat {
         signed_constraint reducer;
         inference_sup(const char* name, pvar var, signed_constraint reduced, signed_constraint reducer) : name(name), var(var), reduced(reduced), reducer(reducer) {}
         std::ostream& display(std::ostream& out) const override {
-            return out << "Superposition " << name << ", reduced v" << var << " in   " << reduced << "   by   " << reducer;
+            return out << "Superposition " << name << ", reduced v" << var
+                << " in " << reduced.blit() << ": " << reduced
+                << " by " << reducer.blit() << ": " << reducer;
         }
     };
 
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 3c3599d37..a747e4cab 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -559,7 +559,7 @@ namespace polysat {
     /**
      * Conflict resolution.
      */
-    void solver::resolve_conflict() {        
+    void solver::resolve_conflict() {
         LOG_H2("Resolve conflict");
         LOG("\n" << *this);
         LOG(search_state_pp(m_search, true));
@@ -572,8 +572,9 @@ namespace polysat {
             pvar v = m_conflict.conflict_var();
             // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
             // TODO: use unsat core from m_viable_fallback if the conflict is from there
-            // TODO: we could try simpler backtracking loop if we get a lemma from forbidden intervals
             VERIFY(m_viable.resolve(v, m_conflict));
+            backtrack_fi();
+            return;
         }
         
         search_iterator search_it(m_search);
@@ -630,6 +631,74 @@ namespace polysat {
         report_unsat();
     }
 
+    /**
+     * Simpler backracking for forbidden interval lemmas:
+     * since forbidden intervals already gives us a lemma where the conflict variable has been eliminated,
+     * we can backtrack to the last relevant decision and learn this lemma.
+     */
+    void solver::backtrack_fi() {
+        uint_set relevant_vars;
+        search_iterator search_it(m_search);
+        while (search_it.next()) {
+            auto& item = *search_it;
+            search_it.set_resolved();
+            if (item.is_assignment()) {
+                // Resolve over variable assignment
+                pvar v = item.var();
+                if (!m_conflict.pvar_occurs_in_constraints(v) && !relevant_vars.contains(v)) {
+                    m_search.pop_assignment();
+                    continue;
+                }
+                LOG_H2("Working on " << search_item_pp(m_search, item));
+                LOG(m_justification[v]);
+                LOG("Conflict: " << m_conflict);
+                inc_activity(v);
+                justification& j = m_justification[v];
+                if (j.level() > base_level() && j.is_decision()) {
+                    m_conflict.end_conflict();
+                    revert_decision(v);
+                    return;
+                }
+                SASSERT(j.is_propagation());
+                // If a variable was propagated:
+                // we don't really care about the constraints in this case, but just about the variables it depends on
+                for (auto const& c : m_viable.get_constraints(v))
+                    for (pvar v : c->vars()) {
+                        relevant_vars.insert(v);
+                        m_conflict.log_var(v);
+                    }
+                m_search.pop_assignment();
+            }
+            else {
+                // Resolve over boolean literal
+                SASSERT(item.is_boolean());
+                sat::literal const lit = item.lit();
+                sat::bool_var const var = lit.var();
+                if (!m_conflict.is_marked(var))
+                    continue;
+                LOG_H2("Working on " << search_item_pp(m_search, item));
+                LOG(bool_justification_pp(m_bvars, lit));
+                LOG("Literal " << lit << " is " << lit2cnstr(lit));
+                LOG("Conflict: " << m_conflict);
+                if (m_bvars.is_assumption(var))
+                    continue;
+                else if (m_bvars.is_decision(var)) {
+                    m_conflict.end_conflict();
+                    revert_bool_decision(lit);
+                    return;
+                }
+                else if (m_bvars.is_bool_propagation(var))
+                    m_conflict.resolve(lit, *m_bvars.reason(lit));
+                else {
+                    SASSERT(m_bvars.is_value_propagation(var));
+                    continue;
+                }
+            }
+        }
+        m_conflict.end_conflict();
+        report_unsat();
+    }
+
     /**
     * Variable activity accounting.
     * As a placeholder we increment activity 
@@ -706,8 +775,6 @@ namespace polysat {
 
     void solver::decide_on_lemma(clause& lemma) {
         LOG_H3("Guessing literal in lemma: " << lemma);
-        IF_LOGGING(m_viable.log());
-        LOG("Boolean assignment: " << m_bvars);
 
         // To make a guess, we need to find an unassigned literal that is not false in the current model.
 
@@ -717,6 +784,7 @@ namespace polysat {
         for (sat::literal lit : lemma) {
             switch (m_bvars.value(lit)) {
             case l_true:
+                LOG("Already satisfied because literal " << lit << " is true");
                 return;
             case l_false:
                 break;
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index ae9e26755..aa489acda 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -72,6 +72,7 @@ namespace polysat {
         friend class restart;
         friend class explainer;
         friend class inference_engine;
+        friend class inference_logger;
         friend class forbidden_intervals;
         friend class linear_solver;
         friend class viable;
@@ -203,7 +204,7 @@ namespace polysat {
         unsigned base_level() const;
 
         void resolve_conflict();
-        void resolve_bool(sat::literal lit);
+        void backtrack_fi();
         void revert_decision(pvar v);
         void revert_bool_decision(sat::literal lit);
 
diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index cf041e2e9..eb292ff06 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -176,7 +176,7 @@ namespace polysat {
     }
 
     bool ule_constraint::is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const { 
-        return false; 
+        return is_currently_false(s, sub, !is_positive);
     }
 
     bool ule_constraint::is_currently_true(solver& s, bool is_positive) const {