From bd162588b28c1ca38980bfd0df040539df176370 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Apr 2015 17:09:01 -0700 Subject: [PATCH] enable SAT solver by default for MaxSAT constraints Signed-off-by: Nikolaj Bjorner --- src/opt/opt_params.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 13049986a..ef92af54b 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -8,7 +8,7 @@ def_module_params('opt', ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('print_model', BOOL, False, 'display model for satisfiable constraints'), ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'), - ('enable_sat', BOOL, False, 'enable the new SAT core for propositional constraints'), + ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'), ('elim_01', BOOL, True, 'eliminate 01 variables'), ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'), ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'),