fix bug in translation of pbeq into sat

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

src/ast/pb_decl_plugin.cpp

@@ -162,6 +162,9 @@ app * pb_util::mk_eq(unsigned num_args, rational const * coeffs, expr * const *
     if (!m_k.is_int()) {
         return m.mk_false();
     }
+    if (num_args == 0) {
+        return m_k.is_zero() ? m.mk_true() : m.mk_false();
+    }
     m_params.reset();
     m_params.push_back(parameter(m_k));
     for (unsigned i = 0; i < num_args; ++i) {

src/ast/rewriter/pb2bv_rewriter.cpp

@@ -94,12 +94,7 @@ struct pb2bv_rewriter::imp {
             for (unsigned i = 0; i < m_args.size(); ++i) {
                 cas.push_back(std::make_pair(m_coeffs[i], expr_ref(m_args[i].get(), m)));
             }
-            //for (ca const& ca : cas) std::cout << ca.first << " ";
-            //std::cout << "\n";
             std::sort(cas.begin(), cas.end(), compare_coeffs());
-            //std::cout << "post-sort\n";
-            //for (ca const& ca : cas) std::cout << ca.first << " ";
-            //std::cout << "\n";
             m_coeffs.reset();
             m_args.reset();
             for (ca const& ca : cas) {

src/ast/rewriter/pb_rewriter.cpp

@@ -329,7 +329,7 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
           tout << tmp << "\n";
           tout << result << "\n";
           );
-
+    
     TRACE("pb_validate",
           validate_rewrite(f, num_args, args, result););
           

src/cmd_context/basic_cmds.cpp

@@ -110,6 +110,8 @@ public:
     virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; }
     virtual void execute(cmd_context & ctx) {
         model_ref m;
+        if (ctx.ignore_check())
+            return;
         if (!ctx.is_model_available(m) || ctx.get_check_sat_result() == 0)
             throw cmd_exception("model is not available");
         if (m_index > 0 && ctx.get_opt()) {

src/sat/tactic/goal2sat.cpp

@@ -571,6 +571,8 @@ struct goal2sat::imp {
             l.neg();
         }
         m_ext->add_at_least(v2, lits, lits.size() - k.get_unsigned());
+
+
         if (root) {
             m_result_stack.reset();
         }
@@ -582,7 +584,8 @@ struct goal2sat::imp {
             mk_clause(~l, l2);
             mk_clause(~l1, ~l2, l);
             m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
-            m_result_stack.push_back(l);
+            m_result_stack.push_back(sign ? ~l : l);
+
         }
     }