diff --git a/src/muz/base/proof_utils.cpp b/src/muz/base/proof_utils.cpp
index 87ecf9985..d4a8ab22b 100644
--- a/src/muz/base/proof_utils.cpp
+++ b/src/muz/base/proof_utils.cpp
@@ -156,12 +156,22 @@ public:
             SASSERT(m.get_num_parents(p) == 1);
             tmp = m.get_parent(p, 0);
             elim(tmp);
-            get_literals(m.get_fact(p));
             expr_set* hyps = m_hypmap.find(tmp);
             expr_set* new_hyps = 0;
             if (hyps) {
                 new_hyps = alloc(expr_set, *hyps);
             }
+            expr* fact = m.get_fact(p);
+            // when hypothesis is a single literal of the form 
+            // (or A B), and the fact of p is (or A B).            
+            if (hyps && hyps->size() == 1 && in_hypotheses(fact, hyps)) {
+                m_literals.reset();
+                m_literals.push_back(fact);
+            }
+            else {
+                get_literals(fact);
+            }
+
             for (unsigned i = 0; i < m_literals.size(); ++i) {
                 expr* e = m_literals[i];
                 if (!in_hypotheses(e, hyps)) {
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index f22ce479e..b98343013 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -533,6 +533,9 @@ namespace opt {
             for (unsigned i = 0; i < sz; i++) {
                 quick_for_each_expr(proc, visited, get_solver().get_assertion(i));
             }
+            for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
+                quick_for_each_expr(proc, visited, m_hard_constraints[i].get());
+            }
         }
         catch (is_bv::found) {
             return false;