diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index ee74e90a2..acc7dc777 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1177,6 +1177,7 @@ namespace sat {
 
         do {
 
+
             if (m_overflow || offset > (1 << 12)) {
                 IF_VERBOSE(20, verbose_stream() << "offset: " << offset << "\n";
                            DEBUG_CODE(active2pb(m_A); display(verbose_stream(), m_A);););
@@ -1214,7 +1215,7 @@ namespace sat {
             case justification::TERNARY:
                 inc_bound(offset); 
                 SASSERT (consequent != null_literal);
-                inc_coeff(consequent, offset);
+                inc_coeff(consequent, offset);				
                 process_antecedent(js.get_literal1(), offset);
                 process_antecedent(js.get_literal2(), offset);
                 break;
diff --git a/src/sat/sat_justification.h b/src/sat/sat_justification.h
index 0357621f9..602767d27 100644
--- a/src/sat/sat_justification.h
+++ b/src/sat/sat_justification.h
@@ -23,7 +23,7 @@ namespace sat {
     
     class justification {
     public:
-        enum kind { NONE, BINARY, TERNARY, CLAUSE, EXT_JUSTIFICATION };
+        enum kind { NONE = 0, BINARY = 1, TERNARY = 2, CLAUSE = 3, EXT_JUSTIFICATION = 4};
     private:
         unsigned m_level;
         size_t m_val1;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 2a28f5233..a788f7ee7 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -429,21 +429,13 @@ namespace sat {
 
     bool solver::propagate_bin_clause(literal l1, literal l2) {
         if (value(l2) == l_false) {
-            if (value(l1) == l_false) {
-                TRACE("sat", tout << "conflict " << l1 << " " << l2 << "\n";);
-                set_conflict(justification(std::max(lvl(l1), lvl(l2)), l1, l2));
-            }
-            else {
-                m_stats.m_bin_propagate++;
-                //TRACE("sat", tout << "propagate " << l1 << " <- " << ~l2 << "\n";);
-                assign(l1, justification(lvl(l2), l2));
-            }
+            m_stats.m_bin_propagate++;
+            assign(l1, justification(lvl(l2), l2));            
             return true;
         }
-        else if (value(l1) == l_false) {
+        if (value(l1) == l_false) {
             m_stats.m_bin_propagate++;
-            //TRACE("sat", tout << "propagate " << l2 << " <- " << ~l1 << "\n";);
-            assign(l2, justification(lvl(l1), l1) );
+            assign(l2, justification(lvl(l1), l1));
             return true;
         }
         return false;