fix #1729

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_goal.cpp

@@ -199,8 +199,8 @@ extern "C" {
         RESET_ERROR_CODE();
         std::ostringstream buffer;
         if (!to_goal_ref(g)->is_cnf()) { 
-            warning_msg("goal is not in CNF. This will produce a propositional abstraction. "
+            SET_ERROR_CODE(Z3_INVALID_ARG, "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf");
-                        "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf");
+            RETURN_Z3(nullptr);
         }
         to_goal_ref(g)->display_dimacs(buffer);
         // Hack for removing the trailing '\n'

src/api/z3_api.h

@@ -5525,6 +5525,11 @@ extern "C" {
 
     /**
        \brief Convert a goal into a DIMACS formatted string.
+       The goal must be in CNF. You can convert a goal to CNF
+       by applying the tseitin-cnf tactic. Bit-vectors are not automatically
+       converted to Booleans either, so the caller intends to 
+       preserve satisfiability, it should apply bit-blasting tactics.
+       Quantifiers and theory atoms will not be encoded.
 
        def_API('Z3_goal_to_dimacs_string', STRING, (_in(CONTEXT), _in(GOAL)))
     */

src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp

@@ -89,6 +89,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
     expr_ref_vector                          m_out;
     obj_map<func_decl, expr*>                m_const2bits;
     expr_ref_vector                          m_bindings;
+    unsigned_vector                          m_shifts;
     func_decl_ref_vector                     m_keys;
     expr_ref_vector                          m_values;
     unsigned_vector                          m_keyval_lim;
@@ -579,19 +580,36 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
             }
             SASSERT(new_bindings.size() == q->get_num_decls());
             i = q->get_num_decls();
+            unsigned shift = j;
+            if (!m_shifts.empty()) shift += m_shifts.back();
             while (i > 0) {
                 i--;
                 m_bindings.push_back(new_bindings[i]);
+                m_shifts.push_back(shift);
             }
         }
         return true;
     }
 
     bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
-        if (m_blast_quant) {
+        if (m_blast_quant) {   
-            if (t->get_idx() >= m_bindings.size())
+            if (m_bindings.empty())
                 return false;
-            result = m_bindings.get(m_bindings.size() - t->get_idx() - 1);
+            unsigned shift = m_shifts.back();
+            if (t->get_idx() >= m_bindings.size()) {
+                if (shift == 0)
+                    return false;
+                result = m_manager.mk_var(t->get_idx() + shift, t->get_sort());
+            }
+            else {
+                unsigned offset = m_bindings.size() - t->get_idx() - 1; 
+                result = m_bindings.get(offset);
+                shift = shift - m_shifts[offset];
+                if (shift > 0) {
+                    var_shifter vs(m_manager);
+                    vs(result, shift, result);
+                }
+            }
             result_pr = nullptr;
             return true;
         }
@@ -641,6 +659,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
                                    old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
         result_pr = nullptr;
         m_bindings.shrink(old_sz);
+        m_shifts.shrink(old_sz);
         return true;
     }
 };

src/tactic/goal.cpp

@@ -733,7 +733,9 @@ bool goal::is_cnf() const {
 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 (to_app(f)->get_family_id() == m_manager.get_basic_family_id()) {
-        !m_manager.is_false(f) && !m_manager.is_true(f)) return false;
+        for (expr* arg : *to_app(f)) 
+            if (m_manager.is_bool(arg)) return false;
+    }
     return true;
 }