From 3d8dd0d783d2a54e36a5fd85e719c5ab2328ee51 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Feb 2026 19:06:06 -0800 Subject: [PATCH] update params Signed-off-by: Nikolaj Bjorner --- src/params/smt_params.cpp | 1 - src/params/smt_params.h | 1 - src/params/smt_params_helper.pyg | 1 - 3 files changed, 3 deletions(-) diff --git a/src/params/smt_params.cpp b/src/params/smt_params.cpp index 399e1e357..a80483d0f 100644 --- a/src/params/smt_params.cpp +++ b/src/params/smt_params.cpp @@ -51,7 +51,6 @@ 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 473d017ef..68ab50ffe 100644 --- a/src/params/smt_params.h +++ b/src/params/smt_params.h @@ -114,7 +114,6 @@ 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/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 001681149..451a07964 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -114,7 +114,6 @@ def_module_params(module_name='smt', ('up.persist_clauses', BOOL, False, 'replay propagated clauses below the levels they are asserted'), ('array.weak', BOOL, False, 'weak array theory'), ('array.extensional', BOOL, True, 'extensional array theory'), - ('finite_set.lattice_refutation', BOOL, True, 'enable lattice refutation for finite set theory'), ('clause_proof', BOOL, False, 'record a clausal proof'), ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'), ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transitivity of equalities'),