diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index cc1456ac9..d57cee2a4 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -48,6 +48,7 @@ Notes:
 namespace opt {
 
     void context::scoped_state::push() {
+        m_asms_lim.push_back(m_asms.size());
         m_hard_lim.push_back(m_hard.size());
         m_objectives_lim.push_back(m_objectives.size());        
         m_objectives_term_trail_lim.push_back(m_objectives_term_trail.size());
@@ -55,6 +56,7 @@ namespace opt {
 
     void context::scoped_state::pop() {
         m_hard.resize(m_hard_lim.back());
+        m_asms.resize(m_asms_lim.back());
         unsigned k = m_objectives_term_trail_lim.back();
         while (m_objectives_term_trail.size() > k) {
             unsigned idx = m_objectives_term_trail.back();
@@ -73,6 +75,7 @@ namespace opt {
         }
         m_objectives_lim.pop_back();            
         m_hard_lim.pop_back();   
+        m_asms_lim.pop_back();
     }
     
     void context::scoped_state::add(expr* hard) {
@@ -188,6 +191,12 @@ namespace opt {
         clear_state();
     }
 
+    void context::add_hard_constraint(expr* f, expr* t) {
+        m_scoped_state.m_asms.push_back(t);
+        m_scoped_state.add(m.mk_implies(t, f));
+        clear_state();
+    }
+
     void context::get_hard_constraints(expr_ref_vector& hard) {
         hard.append(m_scoped_state.m_hard);
     }
@@ -253,7 +262,7 @@ namespace opt {
         m_hard_constraints.append(s.m_hard);
     }
 
-    lbool context::optimize(expr_ref_vector const& asms) {
+    lbool context::optimize(expr_ref_vector const& _asms) {
         if (m_pareto) {
             return execute_pareto();
         }
@@ -263,6 +272,8 @@ namespace opt {
         clear_state();
         init_solver(); 
         import_scoped_state(); 
+        expr_ref_vector asms(_asms);
+        asms.append(m_scoped_state.m_asms);
         normalize(asms);
         if (m_hard_constraints.size() == 1 && m.is_false(m_hard_constraints.get(0))) {
             return l_false;
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 796e83535..5959c4d19 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -115,20 +115,23 @@ namespace opt {
             arith_util   m_arith;
             bv_util      m_bv;
             unsigned_vector  m_hard_lim;
+            unsigned_vector  m_asms_lim;
             unsigned_vector  m_objectives_lim;
             unsigned_vector  m_objectives_term_trail;
             unsigned_vector  m_objectives_term_trail_lim;
             map_id           m_indices;
 
         public:
-            expr_ref_vector  m_hard;
+            expr_ref_vector   m_hard;
+            expr_ref_vector   m_asms;
             vector<objective> m_objectives;
 
             scoped_state(ast_manager& m):
                 m(m),
                 m_arith(m),
                 m_bv(m),
-                m_hard(m)
+                m_hard(m),
+                m_asms(m)
             {}
             void push();
             void pop();
@@ -180,6 +183,7 @@ namespace opt {
         unsigned add_soft_constraint(expr* f, rational const& w, symbol const& id);
         unsigned add_objective(app* t, bool is_max);
         void add_hard_constraint(expr* f);
+        void add_hard_constraint(expr* f, expr* t);
         
         void get_hard_constraints(expr_ref_vector& hard);
         expr_ref get_objective(unsigned i);
diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index 5b620ed6e..1b53875d8 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -72,14 +72,36 @@ namespace sat {
     }
 
     void drat::dump(unsigned n, literal const* c, status st) {
-        switch (st) {
-        case status::asserted: return;
-        case status::external: return; // requires extension to drat format.
-        case status::learned: break;
-        case status::deleted: (*m_out) << "d "; break;
+        if (st == status::asserted || st == status::external) {
+            return;
         }
-        for (unsigned i = 0; i < n; ++i) (*m_out) << c[i] << " ";
-        (*m_out) << "0\n";
+
+        char buffer[10000];
+        int len = 0;
+        if (st == status::deleted) {
+            buffer[0] = 'd';
+            buffer[1] = ' ';
+            len = 2;
+        }
+        for (unsigned i = 0; i < n && len >= 0; ++i) {
+            literal lit = c[i];
+            int _lit = lit.var();
+            if (lit.sign()) _lit = -_lit;
+            len += snprintf(buffer + len, sizeof(buffer) - len, "%d ", _lit);
+        }
+        
+        if (len >= 0) {
+            len += snprintf(buffer + len, sizeof(buffer) - len, "0\n");
+        }
+        if (len >= 0) {
+            m_out->write(buffer, len);
+        }
+        else {
+            if (st == status::deleted) (*m_out) << "d ";
+            for (unsigned i = 0; i < n; ++i) (*m_out) << c[i] << " ";
+            (*m_out) << "0\n";
+        }
+        
     }
 
     void drat::bdump(unsigned n, literal const* c, status st) {
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 1a2b432df..8297e2a99 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -1701,6 +1701,7 @@ namespace sat {
                 if (is_fixed_at(lit, c_fixed_truth) || is_true_at(lit, level)) continue;
                 bool unsat = false;
                 if (is_false_at(lit, level)) {
+                    if (lit.sign() && lit.var() == 34523) std::cout << "false at " << lit << "\n";
                     unsat = true;
                 }
                 else {
@@ -1708,7 +1709,9 @@ namespace sat {
                     reset_lookahead_reward(lit);
                     unsigned num_units = push_lookahead1(lit, level);
                     update_lookahead_reward(lit, level);
+                    if (lit.sign() && lit.var() == 34523) std::cout << "num units.1 " << num_units << " " << inconsistent() << "\n";
                     num_units += do_double(lit, dl_lvl);
+                    if (lit.sign() && lit.var() == 34523) std::cout << "num units.2 " << num_units << "\n";
                     if (dl_lvl > level) {
                         base = dl_lvl;
                         //SASSERT(get_level(m_trail.back()) == base + m_lookahead[i].m_offset);