From 8c95dff33b10aed6b8931d7c0d00fb730027d608 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 22 May 2022 09:10:26 -0400
Subject: [PATCH] cnf

---
 src/sat/sat_solver/inc_sat_solver.cpp | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index cf46b1f27..3d46ec643 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -792,7 +792,6 @@ private:
             m_is_cnf &= is_literal(get_assumption(i));
 
         if (m_is_cnf) {
-            //            std::cout << "assumptions " << sz << " " << get_num_assumptions() << " " << m_fmls_head << " " <<  m_fmls.size() << "\n";
             expr_ref_vector fmls(m);
             fmls.append(sz, asms);
             for (unsigned i = 0; i < get_num_assumptions(); ++i)
@@ -923,18 +922,19 @@ private:
     }
 
     bool is_clause(expr* fml) {
-        if (is_literal(fml)) {
+        if (get_depth(fml) > 4)
+            return false;
+
+        if (is_literal(fml)) 
+            return true;
+        
+        if (m.is_or(fml) || m.is_and(fml) || m.is_implies(fml) || m.is_not(fml) || m.is_iff(fml)) {
+            for (expr* n : *to_app(fml)) 
+                if (!is_clause(n)) 
+                    return false;                            
             return true;
         }
-        if (!m.is_or(fml)) {
-            return false;
-        }
-        for (expr* n : *to_app(fml)) {
-            if (!is_literal(n)) {
-                return false;
-            }
-        }
-        return true;
+        return false;
     }
 
     lbool internalize_formulas() {
@@ -944,7 +944,6 @@ private:
         lbool res;
         
         if (m_is_cnf) {
-            std::cout << "cnf\n";
             res = internalize_goal(m_fmls.size() - m_fmls_head, m_fmls.data() + m_fmls_head);
         }
         else {