diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 5fdd05884..3c97a985f 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -348,11 +348,11 @@ namespace sat {
     }
 
     void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
-        if (find_binary_watch(get_wlist(~l1), ~l2)) {
+        if (find_binary_watch(get_wlist(~l1), ~l2) && value(l1) == l_undef) {
             assign_core(l1, 0, justification(l2));
             return;
         }
-        if (find_binary_watch(get_wlist(~l2), ~l1)) {
+        if (find_binary_watch(get_wlist(~l2), ~l1) && value(l2) == l_undef) {
             assign_core(l2, 0, justification(l1));
             return;
         }