diff --git a/src/sat/sat_aig_finder.cpp b/src/sat/sat_aig_finder.cpp
index ff822eca3..c4a96a0f9 100644
--- a/src/sat/sat_aig_finder.cpp
+++ b/src/sat/sat_aig_finder.cpp
@@ -75,6 +75,7 @@ namespace sat {
                 for (literal tail : c) 
                     if (tail != head) 
                         m_ands.push_back(~tail);
+                // DEBUG_CODE(validate_and(head, m_ands, c););
                 m_on_aig(head, m_ands);
                 break;
             }
@@ -202,6 +203,7 @@ namespace sat {
                         if (c1) c1->mark_used();
                         if (c2) c2->mark_used();
                         if (c3) c3->mark_used();
+                        // DEBUG_CODE(validate_if(~x, ~y, z, u, c, c1, c2, c3););
                         m_on_if(~x, ~y, z, u);
                         return true;
                     }
@@ -223,5 +225,67 @@ namespace sat {
         clauses.filter_update(not_used);        
     }
 
+    void aig_finder::validate_clause(literal_vector const& clause, vector<literal_vector> const& clauses) {
+        solver vs(s.params(), s.rlimit());
+        for (unsigned i = 0; i < s.num_vars(); ++i) {
+            vs.mk_var();
+        }
+        svector<solver::bin_clause> bins;
+        s.collect_bin_clauses(bins, true, false);
+        for (auto b : bins) {
+            vs.mk_clause(b.first, b.second);
+        }
+        for (auto const& cl : clauses) {
+            vs.mk_clause(cl);
+        }
+        for (literal l : clause) {
+            literal nl = ~l;
+            vs.mk_clause(1, &nl);
+        }
+        lbool r = vs.check();
+        if (r != l_false) {
+            vs.display(verbose_stream());
+            UNREACHABLE();
+        }
+    }
+
+    void aig_finder::validate_clause(literal x, literal y, literal z, vector<literal_vector> const& clauses) {
+        literal_vector clause;
+        clause.push_back(x);
+        clause.push_back(y);
+        clause.push_back(z);
+        validate_clause(clause, clauses);
+    }
+
+    void aig_finder::validate_and(literal head, literal_vector const& ands, clause const& c) {
+        IF_VERBOSE(2, verbose_stream() << "validate and: " << head << " == " << ands << "\n");
+        vector<literal_vector> clauses;
+        clauses.push_back(literal_vector(c.size(), c.begin()));
+        literal_vector clause;
+        clause.push_back(head);
+        for (literal l : ands) clause.push_back(~l);
+        validate_clause(clause, clauses);
+        for (literal l : ands) {
+            clause.reset();
+            clause.push_back(~head);
+            clause.push_back(l);
+            validate_clause(clause, clauses);
+        }
+    }
+
+    void aig_finder::validate_if(literal x, literal c, literal t, literal e, clause const& c0, clause const* c1, clause const* c2, clause const* c3) {
+        IF_VERBOSE(2, verbose_stream() << "validate if: " << x << " == " << c << " ? " << t << " : " << e << "\n");
+        vector<literal_vector> clauses;
+        clauses.push_back(literal_vector(c0.size(), c0.begin()));
+        if (c1) clauses.push_back(literal_vector(c1->size(), c1->begin()));
+        if (c2) clauses.push_back(literal_vector(c2->size(), c2->begin()));
+        if (c3) clauses.push_back(literal_vector(c3->size(), c3->begin()));
+        literal_vector clause;
+        validate_clause(~x, ~c, t, clauses);
+        validate_clause(~x,  c, e, clauses);
+        validate_clause(~t, ~c, x, clauses);
+        validate_clause(~e,  c, x, clauses);
+    }
+
 
 }
diff --git a/src/sat/sat_aig_finder.h b/src/sat/sat_aig_finder.h
index cb89a4b54..4a5784cc9 100644
--- a/src/sat/sat_aig_finder.h
+++ b/src/sat/sat_aig_finder.h
@@ -44,6 +44,10 @@ namespace sat {
         bool find_aig(clause& c);
         void find_ifs(clause_vector& clauses);
         void find_aigs(clause_vector& clauses);
+        void validate_and(literal head, literal_vector const& ands, clause const& c);
+        void validate_if(literal x, literal c, literal t, literal e, clause const& c0, clause const* c1, clause const* c2, clause const* c3);
+        void validate_clause(literal x, literal y, literal z, vector<literal_vector> const& clauses);
+        void validate_clause(literal_vector const& clause, vector<literal_vector> const& clauses);
 
     public:
         aig_finder(solver& s) : s(s), m_big(s.rand()) {}