bug fixes reported by Miguel

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

src/sat/ba_solver.cpp

@@ -2396,7 +2396,7 @@ namespace sat {
             init_use_lists();
             remove_unused_defs();
             set_non_external();
-            elim_pure();
+            if (get_config().m_elim_vars) elim_pure();
             for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]);
             for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]);
             cleanup_clauses();

src/sat/sat_config.cpp

@@ -19,6 +19,8 @@ Revision History:
 #include "sat/sat_config.h"
 #include "sat/sat_types.h"
 #include "sat/sat_params.hpp"
+#include "sat/sat_simplifier_params.hpp"
+
 
 namespace sat {
 
@@ -39,6 +41,7 @@ namespace sat {
         m_local_search = 0;
         m_lookahead_search = false;
         m_lookahead_simplify = false;
+        m_elim_vars = false;
         updt_params(p); 
     }
 
@@ -188,6 +191,9 @@ namespace sat {
         }
         m_dimacs_display  = p.dimacs_display();
         m_dimacs_inprocess_display  = p.dimacs_inprocess_display();
+
+        sat_simplifier_params sp(_p);
+        m_elim_vars = sp.elim_vars();
     }
 
     void config::collect_param_descrs(param_descrs & r) {

src/sat/sat_config.h

@@ -133,6 +133,10 @@ namespace sat {
         double             m_step_size_min;
         double             m_reward_multiplier;
         double             m_reward_offset;
+
+        // simplifier configurations used outside of sat_simplifier
+        bool               m_elim_vars;
+
         config(params_ref const & p);
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);

src/sat/sat_solver/inc_sat_solver.cpp

@@ -510,7 +510,6 @@ public:
         }
         m_internalized_fmls.reset();
         g.get_formulas(m_internalized_fmls);
-        // g.display(std::cout);
         m_internalized_converted = true;
         // if (mc) mc->display(std::cout << "mc");
         // if (m_mc) m_mc->display(std::cout << "m_mc\n");

src/sat/tactic/goal2sat.cpp

@@ -1063,7 +1063,7 @@ struct sat2goal::imp {
         for (sat::literal l : c) {
             lits.push_back(lit2expr(l));
         }
-        expr_ref fml(pb.mk_at_most_k(c.size(), lits.c_ptr(), c.k()), m);
+        expr_ref fml(pb.mk_at_least_k(c.size(), lits.c_ptr(), c.k()), m);
         
         if (c.lit() != sat::null_literal) {
             fml = m.mk_eq(lit2expr(c.lit()), fml);            
@@ -1110,6 +1110,7 @@ struct sat2goal::imp {
             r.assert_expr(m.mk_false());
             return;
         }
+        IF_VERBOSE(1, verbose_stream() << "solver2goal " << s.num_vars() << " " << s.clauses().size() << "\n";);
         init_lit2expr(s, map, mc, r.models_enabled());
         // collect units
         unsigned num_vars = s.num_vars();
@@ -1135,7 +1136,6 @@ struct sat2goal::imp {
         }
         // collect clauses
         assert_clauses(s, s.clauses(), r, true);
-        assert_clauses(s, s.learned(), r, false);
 
         sat::ba_solver* ext = get_ba_solver(s);
         if (ext) {

src/solver/tactic2solver.cpp

@@ -173,6 +173,10 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
             m_result->set_status(l_undef);
             if (reason_unknown != "")
                 m_result->m_unknown = reason_unknown;
+            if (num_assumptions == 0) {
+                m_assertions.reset();
+                g->get_formulas(m_assertions);
+            }
             break;
         }
     }