let cmd_line logic produce_assignments produce_proofs produce_cores produce_interpolants = let open TermLib in (* Path and name of CVC4 executable *) let cvc4_bin = Flags.Smt.cvc4_bin () in let incr_mode = "--incremental" in (* "--tear-down-incremental=1" *) let fmfint_flags = [||] in (* [| "--fmf-bound-int"; "--fmf-inst-engine"; "--quant-cf"; "--uf-ss-fair"|] in*) let fmfrec_flags = [||] in (* [| "--finite-model-find"; "--macros-quant"; "--fmf-inst-engine"; "--fmf-fun"; "--quant-cf"; "--uf-ss-fair"|] in*) let inst_flags = match logic, Flags.Arrays.recdef () with | `Inferred l, true when FeatureSet.mem A l -> fmfrec_flags | `Inferred l, false when FeatureSet.mem A l -> fmfint_flags | `Inferred _, _ -> [||] | _, true -> fmfrec_flags | _, false -> fmfint_flags in let default_cmd = [| cvc4_bin; "--lang"; "smt2"; "--rewrite-divk" |] in Array.concat [default_cmd; [|incr_mode|]; inst_flags]