diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index e91eb86fe..277399b9f 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -189,6 +189,7 @@ def_module_params('fixedpoint', ('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes'), ('spacer.simplify_pob', BOOL, False, 'simplify POBs by removing redundant constraints'), ('spacer.use_quant_generalizer', BOOL, False, 'use quantified lemma generalizer'), + ('spacer.quic_gen_normalize', BOOL, True, 'normalize cube before quantified generalization'), )) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 90103503b..eba51c793 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -2284,8 +2284,10 @@ void context::init_lemma_generalizers(datalog::rule_set& rules) } if (m_params.spacer_use_quant_generalizer()) { - m_lemma_generalizers.push_back(alloc(lemma_bool_inductive_generalizer, *this, 0, true)); - m_lemma_generalizers.push_back(alloc(lemma_quantifier_generalizer, *this)); + m_lemma_generalizers.push_back(alloc(lemma_bool_inductive_generalizer, + *this, 0, true)); + m_lemma_generalizers.push_back(alloc(lemma_quantifier_generalizer, *this, + m_params.spacer_quic_gen_normalize())); } if (get_params().spacer_use_eqclass()) {