From 9912b2cd67def9fab10a81dcd9e5bc6490b69d1a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 23 May 2015 18:01:00 +0100 Subject: [PATCH] Re-enabled the smt.arith.greatest_error_pivot parameter. --- src/smt/params/smt_params_helper.pyg | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 240d45f15..8be6110d5 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -44,7 +44,8 @@ def_module_params(module_name='smt', ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'), - ('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'), + ('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'), + ('arith.greatest_error_pivot', BOOL, False, 'Pivoting strategy'), ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'), ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'), ('pb.enable_compilation', BOOL, True, 'enable compilation into sorting circuits for Pseudo-Boolean'),