fix #4404

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

src/cmd_context/cmd_context.cpp

@@ -473,7 +473,6 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     m_status(UNKNOWN),
     m_numeral_as_real(false),
     m_ignore_check(false),
-    m_processing_pareto(false),
     m_exit_on_error(false),
     m_manager(m),
     m_own_manager(m == nullptr),
@@ -1261,7 +1260,6 @@ void cmd_context::insert_aux_pdecl(pdecl * p) {
 }
 
 void cmd_context::reset(bool finalize) {    
-    m_processing_pareto = false;
     m_logic = symbol::null;
     m_check_sat_result = nullptr;
     m_numeral_as_real = false;
@@ -1307,7 +1305,6 @@ void cmd_context::reset(bool finalize) {
 
 void cmd_context::assert_expr(expr * t) {
     scoped_rlimit no_limit(m().limit(), 0);
-    m_processing_pareto = false;
     if (!m_check_logic(t))
         throw cmd_exception(m_check_logic.get_last_error());
     m_check_sat_result = nullptr;
@@ -1320,7 +1317,6 @@ void cmd_context::assert_expr(expr * t) {
 }
 
 void cmd_context::assert_expr(symbol const & name, expr * t) {
-    m_processing_pareto = false;
     if (!m_check_logic(t))
         throw cmd_exception(m_check_logic.get_last_error());
     if (!produce_unsat_cores() || name == symbol::null) {
@@ -1440,7 +1436,6 @@ static void restore(ast_manager & m, ptr_vector<expr> & c, unsigned old_sz) {
 }
 
 void cmd_context::restore_assertions(unsigned old_sz) {
-    m_processing_pareto = false;
     if (!has_manager()) {
         // restore_assertions invokes m(), so if cmd_context does not have a manager, it will try to create one.
         SASSERT(old_sz == m_assertions.size());
@@ -1460,7 +1455,6 @@ void cmd_context::restore_assertions(unsigned old_sz) {
 
 void cmd_context::pop(unsigned n) {
     m_check_sat_result = nullptr;
-    m_processing_pareto = false;
     if (n == 0)
         return;
     unsigned lvl     = m_scopes.size();
@@ -1507,7 +1501,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         scoped_rlimit _rlimit(m().limit(), rlimit);
         expr_ref_vector asms(m());
         asms.append(num_assumptions, assumptions);
-        if (!m_processing_pareto) {
+        if (!get_opt()->is_pareto()) {
             expr_ref_vector assertions(m());
             unsigned sz = m_assertions.size();
             for (unsigned i = 0; i < sz; ++i) {
@@ -1523,9 +1517,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         }
         try {
             r = get_opt()->optimize(asms);
-            if (r == l_true && get_opt()->is_pareto()) {
-                m_processing_pareto = true;
-            }
         }
         catch (z3_error & ex) {
             throw ex;
@@ -1533,9 +1524,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         catch (z3_exception & ex) {
             throw cmd_exception(ex.msg());
         }
-        if (m_processing_pareto && r != l_true) {
-            m_processing_pareto = false;
-        }
         get_opt()->set_status(r);
     }
     else if (m_solver) {
@@ -1575,10 +1563,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         validate_model();
     }
     validate_check_sat_result(r);
-    if (was_opt && r != l_false && !m_processing_pareto) {
-        // get_opt()->display_assignment(regular_stream());
-    }
-
     model_ref md;
     if (r == l_true && m_params.m_dump_models && is_model_available(md)) {
         display_model(md);

src/cmd_context/cmd_context.h

@@ -192,7 +192,6 @@ protected:
     status                       m_status;
     bool                         m_numeral_as_real;
     bool                         m_ignore_check;      // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
-    bool                         m_processing_pareto; // used when re-entering check-sat for pareto front.
     bool                         m_exit_on_error;
 
     static std::ostringstream    g_error_stream;

src/muz/base/dl_context.cpp

@@ -21,15 +21,15 @@ Revision History:
 #include<limits>
 #include "ast/arith_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
-#include "muz/base/dl_context.h"
 #include "ast/for_each_expr.h"
 #include "ast/ast_smt_pp.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/datatype_decl_plugin.h"
 #include "ast/scoped_proof.h"
-#include "muz/base/fp_params.hpp"
 #include "ast/ast_pp_util.h"
-
+#include "ast/ast_util.h"
+#include "muz/base/dl_context.h"
+#include "muz/base/fp_params.hpp"
 
 namespace datalog {
 
@@ -742,13 +742,7 @@ namespace datalog {
     }
 
     expr_ref context::get_background_assertion() {
-        expr_ref result(m);
-        switch (m_background.size()) {
-        case 0: result = m.mk_true(); break;
-        case 1: result = m_background[0].get(); break;
-        default: result = m.mk_and(m_background.size(), m_background.c_ptr()); break;
-        }
-        return result;
+		return mk_and(m_background);
     }
 
     void context::assert_expr(expr* e) {

src/muz/transforms/dl_mk_subsumption_checker.cpp

@@ -350,7 +350,6 @@ namespace datalog {
             return nullptr;
         }
 
-
         //During the construction of the new set we may discover new total relations
         //(by quantifier elimination on the uninterpreted tails).
         SASSERT(m_new_total_relation_discovery_during_transformation || !m_have_new_total_rule);