diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index f1bd9c749..c1fc6a9e1 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2057,8 +2057,8 @@ namespace sat {
             // {false, true},   p => {true, false}
             // {false, true},  !p => {true, false}            
             void add(literal l) {
+                sign = lit == (sign == l.sign());
                 lit = !lit;
-                sign = sign != l.sign();
             }                
         };
         literal_vector lits;