remove disjunctions by default

We don't want to rely on PCSat, and thus, it is preferable to make an order n nuHFL formula tractable by translating it to an order (n + 1) formula.

lib/options/rethfl_options.ml

@@ -60,7 +60,7 @@ type params =
   (* Preprocess *)
   ; no_inlining : bool [@default false]
     (** Disable inlining *)
-  ; remove_disjunction: bool [@default false]
+  ; no_remove_disjunction: bool [@default false]
     (** Remove disjunction *)
 
   (* Logging *)
@@ -103,7 +103,7 @@ let set_up_params params =
   set_module_log_level Info                params.log_info;
   set_ref oneshot                          params.oneshot;
   set_ref Preprocess.inlining              (not params.no_inlining);
-  set_ref Preprocess.remove_disjunction    params.remove_disjunction;
+  set_ref Preprocess.remove_disjunction    (not params.no_remove_disjunction);
   set_ref Abstraction.max_I                params.abst_max_I;
   set_ref Abstraction.max_ands             params.abst_max_ands;
   set_ref Abstraction.modify_pred_by_guard (not params.abst_no_modify_pred_by_guard);