diff --git a/src/params/smt_params.cpp b/src/params/smt_params.cpp index a80483d0f..399e1e357 100644 --- a/src/params/smt_params.cpp +++ b/src/params/smt_params.cpp @@ -51,6 +51,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_core_validate = p.core_validate(); m_sls_enable = p.sls_enable(); m_sls_parallel = p.sls_parallel(); + m_finite_set_lattice_refutation = p.finite_set_lattice_refutation(); m_logic = _p.get_sym("logic", m_logic); m_string_solver = p.string_solver(); m_up_persist_clauses = p.up_persist_clauses(); diff --git a/src/params/smt_params.h b/src/params/smt_params.h index 68ab50ffe..473d017ef 100644 --- a/src/params/smt_params.h +++ b/src/params/smt_params.h @@ -114,6 +114,7 @@ struct smt_params : public preprocessor_params, symbol m_proof_log; bool m_sls_enable = false; bool m_sls_parallel = true; + bool m_finite_set_lattice_refutation = true; // ----------------------------------- // diff --git a/src/smt/theory_finite_set_lattice_refutation.cpp b/src/smt/theory_finite_set_lattice_refutation.cpp index 0f467aaa9..f80bb4a01 100644 --- a/src/smt/theory_finite_set_lattice_refutation.cpp +++ b/src/smt/theory_finite_set_lattice_refutation.cpp @@ -12,7 +12,7 @@ Module Name: #include "smt/smt_theory.h" #include "smt/theory_finite_set.h" #include "smt/smt_context.h" -#include "iostream" +#include const int NUM_WORDS = 5; // some example have shown, the introduction of large conflict clauses can severely slow down refutation