diff --git a/src/sat/smt/tseitin_proof_checker.cpp b/src/sat/smt/tseitin_proof_checker.cpp
index cef7f4641..ceecdb719 100644
--- a/src/sat/smt/tseitin_proof_checker.cpp
+++ b/src/sat/smt/tseitin_proof_checker.cpp
@@ -13,7 +13,17 @@ Author:
 
     Nikolaj Bjorner (nbjorner) 2022-10-07
 
+TODOs:
 
+- handle distinct
+- handle other internalization from euf_internalize
+- equiv should be modulo commutativity (the E-graph indexes expressions modulo commutativity of top-level operator)
+
+- should we log rules for root clauses too? Root clauses should follow from input.
+  They may be simplified using Tseitin transformation. For example, (and a b) is clausified into 
+  two clauses a, b.
+
+- Tesitin checking could also be performed by depth-bounded SAT (e.g., using BDDs)
 --*/
 
 #include "ast/ast_pp.h"
@@ -44,7 +54,7 @@ namespace tseitin {
         if (!main_expr)
             return false;
 
-        expr* a, * x, * y, *z;
+        expr* a, * x, * y, *z, *u, *v;
 
         // (or (and a b) (not a) (not b))
         // (or (and (not a) b) a (not b))
@@ -53,10 +63,10 @@ namespace tseitin {
             for (expr* arg : *jst)
                 complement_mark(arg);
 
-            for (expr* arg : *to_app(main_expr)) {
+            for (expr* arg : *to_app(main_expr)) 
                 if (!is_complement(arg))
                     return false;
-            }
+            
             return true;
         }
 
@@ -83,6 +93,16 @@ namespace tseitin {
                 return true;
         }
 
+        if (m.is_eq(main_expr, x, y) && m.is_ite(x, z, u, v)) {
+            scoped_mark sm(*this);
+            for (expr* arg : *jst)
+                complement_mark(arg);
+            if (is_marked(z) && equiv(y, v))
+                return true;
+            if (is_complement(z) && equiv(y, u))
+                return true;
+        }
+
         // (or (if a b c) (not b) (not c))
         // (or (if a b c) a (not c))
         // (or (if a b c) (not a) (not b))
@@ -112,6 +132,21 @@ namespace tseitin {
                 return true;
         }       
 
+        // (or (xor a b c d) a b (not c) (not d))
+        if (m.is_xor(main_expr)) {
+            scoped_mark sm(*this);
+            for (expr* arg : *jst)
+                complement_mark(arg);
+            int parity = 0;
+            for (expr* arg : *to_app(main_expr))
+                if (is_marked(arg))
+                    parity++;
+                else if (is_complement(arg))
+                    parity--;
+            if ((parity % 2) == 0)
+                return true;
+        }
+
         if (m.is_not(main_expr, a)) {
             
             // (or (not a) a')
@@ -174,17 +209,24 @@ namespace tseitin {
                     return true;
             }
 
+            // (or (not (xor a b c d)) a b c (not d))
+            if (m.is_xor(a)) {
+                scoped_mark sm(*this);
+                for (expr* arg : *jst)
+                    complement_mark(arg);
+                int parity = 1;
+                for (expr* arg : *to_app(main_expr))
+                    if (is_marked(arg))
+                        parity++;
+                    else if (is_complement(arg))
+                        parity--;
+                if ((parity % 2) == 0)
+                    return true;
+            }
+
             IF_VERBOSE(0, verbose_stream() << "miss " << mk_pp(main_expr, m) << "\n");
 
-#if 0
-            if (m.is_implies(a))
-                return false;
 
-            if (m.is_ite(a))
-                return false;
-            if (m.is_distinct(a))
-                return false;
-#endif
         }
         return false;
     }
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 48ba17128..ca2f8f8f6 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -142,23 +142,19 @@ struct goal2sat::imp : public sat::sat_internalizer {
 
     bool top_level_relevant() {
         return m_top_level && relevancy_enabled();
-    }
-    
-    void mk_clause(sat::literal l) {
-        mk_clause(1, &l);
-    }
+    }   
 
-    void mk_clause(sat::literal l1, sat::literal l2, euf::th_proof_hint* ph = nullptr) {
+    void mk_clause(sat::literal l1, sat::literal l2, euf::th_proof_hint* ph) {
         sat::literal lits[2] = { l1, l2 };
         mk_clause(2, lits, ph);
     }
 
-    void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3, euf::th_proof_hint* ph = nullptr) {
+    void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3, euf::th_proof_hint* ph) {
         sat::literal lits[3] = { l1, l2, l3 };
         mk_clause(3, lits, ph);
     }
 
-    void mk_clause(unsigned n, sat::literal * lits, euf::th_proof_hint* ph = nullptr) {
+    void mk_clause(unsigned n, sat::literal * lits, euf::th_proof_hint* ph) {
         TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
         if (relevancy_enabled())
             ensure_euf()->add_aux(n, lits);