fixes for #6577

- the literal false should not appear in clauses
- the literal true forces a tautology
- fix early return in is_cnf check. It should check all clauses for nested Booleans.

src/api/api_goal.cpp

@@ -198,7 +198,7 @@ extern "C" {
         RESET_ERROR_CODE();
         std::ostringstream buffer;
         if (!to_goal_ref(g)->is_cnf()) { 
-            SET_ERROR_CODE(Z3_INVALID_ARG, "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf");
+            SET_ERROR_CODE(Z3_INVALID_ARG, "Goal is not converted into CNF. Preprocess by optional bit-blasting and applying tseitin-cnf");
             RETURN_Z3(nullptr);
         }
         to_goal_ref(g)->display_dimacs(buffer, include_names);

src/ast/display_dimacs.cpp

@@ -47,6 +47,8 @@ struct dimacs_pp {
         }
         for (unsigned j = 0; j < num_lits; j++) {
             expr * l = lits[j];
+            if (m.is_false(l))
+                continue;
             if (m.is_not(l))
                 l = to_app(l)->get_arg(0);
             if (!is_uninterp_const(l)) 
@@ -101,6 +103,12 @@ struct dimacs_pp {
         }
         for (unsigned j = 0; j < num_lits; j++) {
             expr * l = lits[j];
+            if (m.is_false(l))
+                continue;
+            if (m.is_true(l)) {
+                out << "1 -1 ";
+                continue;
+            }
             if (m.is_not(l)) {
                 out << "-";
                 l = to_app(l)->get_arg(0);

src/tactic/goal.cpp

@@ -692,28 +692,23 @@ bool goal::is_cnf() const {
     for (unsigned i = 0; i < size(); i++) {
         expr * f = form(i);
         if (m_manager.is_or(f)) {
-            for (expr* lit : *to_app(f)) {
-                if (!is_literal(lit)) {
+            for (expr* lit : *to_app(f)) 
+                if (!is_literal(lit)) 
                     return false;
-                }
-            }
-            return true;
         }
-        if (!is_literal(f)) {
+        if (!is_literal(f)) 
             return false;
-        }
     }
     return true;
 }
 
 bool goal::is_literal(expr* f) const {
     m_manager.is_not(f, f);
-    if (!is_app(f)) return false;
-    if (to_app(f)->get_family_id() == m_manager.get_basic_family_id()) {
+    if (!is_app(f)) 
+        return false;
+    if (to_app(f)->get_family_id() == m_manager.get_basic_family_id()) 
         for (expr* arg : *to_app(f)) 
-            if (m_manager.is_bool(arg)) {
+            if (m_manager.is_bool(arg)) 
                 return false;
-            }
-    }
     return true;
 }