diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 607335055..117c9c6f8 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2615,8 +2615,9 @@ namespace sat {
 
         // pre-condition is that the literals, except c.lit(), in c are unwatched.
         if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n";
+        // IF_VERBOSE(0, verbose_stream() << c << "\n";);
         m_weights.resize(2*s().num_vars(), 0);
-
+        // for (unsigned w : m_weights) VERIFY(w == 0);
         for (literal l : c) {
             ++m_weights[l.index()];
         }
@@ -2673,6 +2674,36 @@ namespace sat {
             return;
         }
 
+        if (sz == 0) {
+            if (c.lit() == null_literal) {
+                if (k > 0) {
+                    s().mk_clause(0, nullptr, true);
+                }
+            }
+            else if (k > 0) {
+                literal lit = ~c.lit();
+                s().mk_clause(1, &lit, c.learned());
+            }
+            else {
+                literal lit = c.lit();
+                s().mk_clause(1, &lit, c.learned());
+            }
+            remove_constraint(c, "recompiled to clause");
+            return;
+        }
+        if (all_units && sz < k) {
+            // IF_VERBOSE(0, verbose_stream() << "all units " << sz << " " << k << "\n");
+            if (c.lit() == null_literal) {
+                s().mk_clause(0, nullptr, true);            
+            }
+            else {
+                literal lit = ~c.lit();
+                s().mk_clause(1, &lit, c.learned());
+            }
+            remove_constraint(c, "recompiled to clause");
+            return;            
+        }
+        // IF_VERBOSE(0, verbose_stream() << "csz: " << c.size() << " ck:" << c.k() << " sz:" << sz << " k:" << k << "\n");
         VERIFY(!all_units || c.size() - c.k() >= sz - k);
         c.set_size(sz);
         c.set_k(k);    
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index 9509db760..1d5efdd82 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -29,24 +29,24 @@ static unsigned_vector g_handles;
 
 
 static void display_results() {
-    if (g_opt) {
-        model_ref mdl;
-        g_opt->get_model(mdl);
-        if (mdl) {
-            model_smt2_pp(std::cout, g_opt->get_manager(), *mdl, 0); 
-        }
-
-        for (unsigned h : g_handles) {
-            expr_ref lo = g_opt->get_lower(h);
-            expr_ref hi = g_opt->get_upper(h);
-            if (lo == hi) {
-                std::cout << "   " << lo << "\n";
-            }
-            else {
-                std::cout << "  [" << lo << ":" << hi << "]\n";
-            }
-        }
-    }
+    IF_VERBOSE(1, 
+               if (g_opt) {
+                   model_ref mdl;
+                   g_opt->get_model(mdl);
+                   if (mdl) {
+                       model_smt2_pp(verbose_stream(), g_opt->get_manager(), *mdl, 0); 
+                   }
+                   for (unsigned h : g_handles) {
+                       expr_ref lo = g_opt->get_lower(h);
+                       expr_ref hi = g_opt->get_upper(h);
+                       if (lo == hi) {
+                           std::cout << "   " << lo << "\n";
+                       }
+                       else {
+                           std::cout << "  [" << lo << ":" << hi << "]\n";
+                       }
+                   }
+               });
 }
 
 static void display_statistics() {