From ffeb8f45726334bce148ad4869e46d471e3c87bb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 11 Oct 2022 09:21:36 +0200
Subject: [PATCH] wip - tseitin check

```
(set-option :sat.euf true)
(set-option :sat.smt.proof tseitinproof.smt2)
(set-option :tactic.default_tactic smt)

(declare-const a1 Bool)
(declare-const a2 Bool)
(declare-const a3 Bool)
(declare-const a4 Bool)
(declare-const a5 Bool)
(declare-const a6 Bool)
(declare-const a7 Bool)
(declare-const a8 Bool)
(declare-const a9 Bool)

(declare-const a10 Bool)
(declare-const a11 Bool)
(declare-const a12 Bool)
(declare-const a13 Bool)
(declare-const a14 Bool)
(declare-const a15 Bool)
(declare-const a16 Bool)
(declare-const a17 Bool)
(declare-const a18 Bool)
(declare-const a19 Bool)

(declare-const x1 Bool)
(declare-const x2 Bool)
(declare-const x3 Bool)
(declare-const x4 Bool)
(declare-const x5 Bool)
(declare-const x6 Bool)
(declare-const x7 Bool)
(declare-const x8 Bool)
(declare-const x9 Bool)

(declare-const b1 Int)
(declare-const b2 Int)
(declare-const b3 Int)
(declare-const b4 Int)

(assert (= x1 (and a1 a2)))
(assert (= x2 (or a3 a4)))
(assert (= x3 (=> a5 a6)))
(assert (= x4 (=  a7 a8)))
(assert (= x5 (if a9 a10 a11)))
(assert (= x6 (=> a12 a13)))
(assert (= x7 (xor a1 a2 a3)))
(assert (= x7 (xor a1 a2 a3 a4 a5 (not a6))))
(assert (= x8 (= (ite a1 b1 b2) b3)))
(check-sat)
(exit)

```
---
 src/sat/smt/tseitin_proof_checker.cpp | 2 --
 src/sat/smt/tseitin_proof_checker.h   | 3 +--
 2 files changed, 1 insertion(+), 4 deletions(-)

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) {