diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index 31ab3a358..981b99de7 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -150,6 +150,8 @@ def_module_params('fp', ('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'), ('spacer.q3', BOOL, True, 'Allow quantified lemmas in frames'), ('spacer.q3.instantiate', BOOL, True, 'Instantiate quantified lemmas'), + ('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'), + ('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'), ('spacer.iuc', UINT, 1, '0 = use old implementation of unsat-core-generation, ' + '1 = use new implementation of IUC generation, ' + @@ -164,8 +166,6 @@ def_module_params('fp', ('spacer.iuc.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging)'), ('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes (debugging)'), ('spacer.simplify_pob', BOOL, False, 'simplify pobs by removing redundant constraints'), - ('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'), - ('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'), ('spacer.p3.share_lemmas', BOOL, False, 'Share frame lemmas'), ('spacer.p3.share_invariants', BOOL, False, "Share invariants lemmas"), ('spacer.min_level', UINT, 0, 'Minimal level to explore'),