diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp
index 6c5f90f0e..50561ef60 100644
--- a/src/cmd_context/extra_cmds/proof_cmds.cpp
+++ b/src/cmd_context/extra_cmds/proof_cmds.cpp
@@ -42,6 +42,7 @@ Proof checker for clauses created during search.
 
 #include "util/small_object_allocator.h"
 #include "ast/ast_util.h"
+#include "ast/ast_ll_pp.h"
 #include "smt/smt_solver.h"
 #include "sat/sat_solver.h"
 #include "sat/sat_drat.h"
@@ -181,9 +182,9 @@ public:
         }
         m_solver->pop(1);
         std::cout << "(verified-smt"; 
-        if (proof_hint) std::cout << " " << mk_pp(proof_hint, m);
+        if (proof_hint) std::cout << " " << mk_bounded_pp(proof_hint, m, 4);
         for (expr* arg : clause)
-            std::cout << " " << mk_pp(arg, m);
+            std::cout << " " << mk_bounded_pp(arg, m);
         std::cout << ")\n";
         add_clause(clause);
     }
diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp
index ad929e71a..5061ad88c 100644
--- a/src/sat/smt/euf_proof_checker.cpp
+++ b/src/sat/smt/euf_proof_checker.cpp
@@ -293,17 +293,13 @@ namespace euf {
     }
 
     bool proof_checker::check(expr* e) {
-        if (m_checked_clauses.contains(e))
-            return true;        
         if (!e || !is_app(e))
             return false;
+        if (m_checked_clauses.contains(e))
+            return true;        
         app* a = to_app(e);
         proof_checker_plugin* p = nullptr;
-        if (!m_map.find(a->get_decl()->get_name(), p))
-            return false;
-        if (!p->check(a)) 
-            return false;        
-        return true;
+        return m_map.find(a->get_decl()->get_name(), p) && p->check(a);
     }
 
     expr_ref_vector proof_checker::clause(expr* e) {
diff --git a/src/sat/smt/tseitin_proof_checker.cpp b/src/sat/smt/tseitin_proof_checker.cpp
index a257062c0..df0d60435 100644
--- a/src/sat/smt/tseitin_proof_checker.cpp
+++ b/src/sat/smt/tseitin_proof_checker.cpp
@@ -234,9 +234,15 @@ namespace tseitin {
     bool proof_checker::equiv(expr* a, expr* b) {
         if (a == b)
             return true;
-        expr* x, *y, *z, *u;
-        if (m.is_eq(a, x, y) && m.is_eq(b, z, u))
-            return x == u && y == z;
-        return false;
+        if (!is_app(a) || !is_app(b))
+            return false;
+        if (to_app(a)->get_decl() != to_app(b)->get_decl())
+            return false;
+        if (!to_app(a)->get_decl()->is_commutative())
+            return false;
+        if (to_app(a)->get_num_args() != 2)
+            return false;
+        return to_app(a)->get_arg(0) == to_app(b)->get_arg(1) &&
+            to_app(a)->get_arg(1) == to_app(b)->get_arg(0);
     }
 }