diff --git a/src/sat/smt/tseitin_proof_checker.cpp b/src/sat/smt/tseitin_proof_checker.cpp
index ceecdb719..a257062c0 100644
--- a/src/sat/smt/tseitin_proof_checker.cpp
+++ b/src/sat/smt/tseitin_proof_checker.cpp
@@ -239,6 +239,4 @@ namespace tseitin {
             return x == u && y == z;
         return false;
     }
-
-
 }
diff --git a/src/sat/smt/tseitin_proof_checker.h b/src/sat/smt/tseitin_proof_checker.h
index de5978ac3..677eabfa4 100644
--- a/src/sat/smt/tseitin_proof_checker.h
+++ b/src/sat/smt/tseitin_proof_checker.h
@@ -39,10 +39,9 @@ namespace tseitin {
         bool is_nmarked(expr* a) { return m_nmark.is_marked(a); }
 
         void complement_mark(expr* a) {
+            m_mark.mark(a);
             if (m.is_not(a, a))
                 m_nmark.mark(a);
-            else
-                m_mark.mark(a);
         }
 
         bool is_complement(expr* a) {