From bcbc774b797be40b5b7725faf519f04dfe8f689d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Apr 2020 15:18:26 -0700 Subject: [PATCH] fix #3790 Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.cpp | 2 +- src/muz/base/fp_params.pyg | 2 -- src/muz/rel/dl_mk_explanations.cpp | 5 +---- 3 files changed, 2 insertions(+), 7 deletions(-) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index c722f8196..a69c40f1d 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -299,7 +299,7 @@ namespace datalog { bool context::xform_coi() const { return m_params->xform_coi(); } bool context::xform_slice() const { return m_params->xform_slice(); } bool context::xform_bit_blast() const { return m_params->xform_bit_blast(); } - bool context::karr() const { return m_params->xform_karr(); } + bool context::karr() const { return false; } bool context::scale() const { return m_params->xform_scale(); } bool context::magic() const { return m_params->xform_magic(); } bool context::compress_unbound() const { return m_params->xform_compress_unbound(); } diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index d9f89ce14..098922b1b 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -104,8 +104,6 @@ def_module_params('fp', ('xform.unfold_rules', UINT, 0, "unfold rules statically using iterative squaring"), ('xform.slice', BOOL, True, "simplify clause set using slicing"), - ('xform.karr', BOOL, False, - "Add linear invariants to clauses using Karr's method"), ('spacer.use_euf_gen', BOOL, False, 'Generalize lemmas and pobs using implied equalities'), ('xform.transform_arrays', BOOL, False, "Rewrites arrays equalities and applies select over store"), diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index f10cdd87b..73abd850d 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -838,10 +838,7 @@ namespace datalog { m_e_fact_relation = static_cast(expl_singleton); } func_decl_set predicates(m_context.get_predicates()); - decl_set::iterator it = predicates.begin(); - decl_set::iterator end = predicates.end(); - for (; it!=end; ++it) { - func_decl * orig_decl = *it; + for (func_decl* orig_decl : predicates) { TRACE("dl", tout << mk_pp(orig_decl, m_manager) << "\n";); func_decl * e_decl = get_e_decl(orig_decl);