Add my current why3 config

why3.conf

+[editor pvs]
+command = "%l/why3-call-pvs %l pvs %f"
+name = "PVS"
+
+[editor proofgeneral-coq]
+command = "emacs --eval \"(setq coq-load-path '((\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
+name = "Emacs/ProofGeneral/Coq"
+
+[editor isabelle-jedit]
+command = "isabelle why3 -i %f"
+name = "Isabelle/jEdit"
+
+[editor coqide]
+command = "coqide -R %l/coq Why3 %f"
+name = "CoqIDE"
+
+[editor altgr-ergo]
+command = "altgr-ergo %f"
+name = "AltGr-Ergo"
+
+[ide]
+allow_source_editing = true
+current_tab = 0
+error_color = "red"
+error_color_bg = "yellow"
+error_line_color = "yellow"
+font_size = 10
+goal_color = "gold"
+iconset = "fatcow"
+max_boxes = 16
+neg_premise_color = "pink"
+premise_color = "chartreuse"
+print_attributes = false
+print_coercions = true
+print_locs = false
+print_time_limit = false
+saving_policy = 2
+show_full_context = false
+task_height = 682
+tree_width = 712
+verbose = 0
+window_height = 1017
+window_width = 1920
+
+[main]
+default_editor = "editor %f"
+loadpath = "/usr/share/why3/stdlib"
+magic = 14
+memlimit = 12000
+plugin = "/usr/lib/x86_64-linux-gnu/why3/plugins/hypothesis_selection"
+plugin = "/usr/lib/x86_64-linux-gnu/why3/plugins/tptp"
+plugin = "/usr/lib/x86_64-linux-gnu/why3/plugins/python"
+plugin = "/usr/lib/x86_64-linux-gnu/why3/plugins/genequlin"
+plugin = "/usr/lib/x86_64-linux-gnu/why3/plugins/dimacs"
+running_provers_max = 8
+timelimit = 60
+
+[prover]
+alternative = "noBV"
+command = "z3 -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
+command_steps = "z3 -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
+driver = "z3_432"
+editor = ""
+in_place = false
+interactive = false
+name = "Z3"
+shortcut = "z3-nobv"
+version = "4.4.1"
+
+[prover]
+alternative = "counterexamples"
+command = "z3 -smt2 -t:%t000 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
+command_steps = "z3 -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
+driver = "z3_440_counterexample"
+editor = ""
+in_place = false
+interactive = false
+name = "Z3"
+shortcut = "z3-ce"
+version = "4.4.1"
+
+[prover]
+command = "z3 -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
+command_steps = "z3 -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
+driver = "z3_440"
+editor = ""
+in_place = false
+interactive = false
+name = "Z3"
+shortcut = "z3"
+version = "4.4.1"
+
+[prover]
+command = "eprover -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
+driver = "eprover"
+editor = ""
+in_place = false
+interactive = false
+name = "Eprover"
+shortcut = "eprover"
+version = "2.3"
+
+[prover]
+command = "coqtop -batch -R %l/coq Why3 -l %f"
+driver = "coq"
+editor = "coqide"
+in_place = false
+interactive = true
+name = "Coq"
+shortcut = "coq"
+version = "8.6"
+
+[prover]
+alternative = "noBV"
+command = "cvc4-1.7 --tlimit=%t000 --lang=smt2 %f"
+command_steps = "cvc4-1.7 --stats --rlimit=%S --lang=smt2 %f"
+driver = "cvc4_16_nobv"
+editor = ""
+in_place = false
+interactive = false
+name = "CVC4"
+version = "1.7"
+
+[prover]
+alternative = "noBV"
+command = "cvc4-1.6 --tlimit=%t000 --lang=smt2 %f"
+command_steps = "cvc4-1.6 --stats --rlimit=%S --lang=smt2 %f"
+driver = "cvc4_16_nobv"
+editor = ""
+in_place = false
+interactive = false
+name = "CVC4"
+version = "1.6"
+
+[prover]
+alternative = "counterexamples"
+command = "cvc4-1.6 --tlimit-per=%t000 --lang=smt2 %f"
+command_steps = "cvc4-1.6 --stats --rlimit=%S --lang=smt2 %f"
+driver = "cvc4_16_counterexample"
+editor = ""
+in_place = false
+interactive = false
+name = "CVC4"
+version = "1.6"
+
+[prover]
+command = "cvc4-1.6 --tlimit=%t000 --lang=smt2 %f"
+command_steps = "cvc4-1.6 --stats --rlimit=%S --lang=smt2 %f"
+driver = "cvc4_16"
+editor = ""
+in_place = false
+interactive = false
+name = "CVC4"
+version = "1.6"
+
+[prover]
+alternative = "noBV"
+command = "cvc4 --tlimit=%t000 --lang=smt2 %f"
+command_steps = "cvc4 --stats --rlimit=%S --lang=smt2 %f"
+driver = "cvc4"
+editor = ""
+in_place = false
+interactive = false
+name = "CVC4"
+version = "1.5"
+
+[prover]
+alternative = "counterexamples"
+command = "cvc4 --tlimit-per=%t000 --lang=smt2 %f"
+command_steps = "cvc4 --stats --rlimit=%S --lang=smt2 %f"
+driver = "cvc4_15_counterexample"
+editor = ""
+in_place = false
+interactive = false
+name = "CVC4"
+shortcut = "cvc4-ce"
+version = "1.5"
+
+[prover]
+command = "cvc4 --tlimit=%t000 --lang=smt2 %f"
+command_steps = "cvc4 --stats --rlimit=%S --lang=smt2 %f"
+driver = "cvc4_15"
+editor = ""
+in_place = false
+interactive = false
+name = "CVC4"
+shortcut = "cvc4"
+version = "1.5"
+
+[prover]
+alternative = "noBV"
+command = "cvc4-1.4 --tlimit=%t000 --lang=smt2 %f"
+driver = "cvc4"
+editor = ""
+in_place = false
+interactive = false
+name = "CVC4"
+version = "1.4"
+
+[prover]
+alternative = "Dump"
+command = "cp %f /tmp/cvc4-input"
+driver = "cvc4"
+editor = ""
+in_place = false
+interactive = false
+name = "CVC4"
+version = "1.4"
+
+[prover]
+command = "cvc4-1.4 --tlimit=%t000 --lang=smt2 %f"
+driver = "cvc4_14"
+editor = ""
+in_place = false
+interactive = false
+name = "CVC4"
+version = "1.4"
+
+[prover]
+command = "cvc3 -seed 42 %f"
+driver = "cvc3"
+editor = ""
+in_place = false
+interactive = false
+name = "CVC3"
+shortcut = "cvc3"
+version = "2.4.1"
+
+[prover]
+command = "alt-ergo -timelimit %t %f"
+command_steps = "alt-ergo -steps-bound %S %f"
+driver = "alt_ergo"
+editor = "altgr-ergo"
+in_place = false
+interactive = false
+name = "Alt-Ergo"
+shortcut = "altergo"
+shortcut = "alt-ergo"
+version = "2.0.0"
+
+[strategy]
+code = "t split_vc exit"
+desc = "Split@ the@ VC@ into@ subgoals"
+name = "Split_VC"
+shortcut = "s"
+
+[strategy]
+code = "start:
+c CVC4,1.5 1 1000
+c Z3,4.4.1 1 1000
+c Alt-Ergo,2.0.0 1 1000
+t split_all_full start
+c CVC4,1.5 5 2000
+c Z3,4.4.1 5 2000
+c Alt-Ergo,2.0.0 5 2000
+t introduce_premises afterintro
+afterintro:
+t inline_goal afterinline
+g trylongertime
+afterinline:
+t split_all_full start
+trylongertime:
+c CVC4,1.5 30 4000
+c Z3,4.4.1 30 4000
+c Alt-Ergo,2.0.0 30 4000
+"
+desc = "Automatic@ run@ of@ provers@ and@ most@ useful@ transformations"
+name = "Auto_level_2"
+shortcut = "2"
+
+[strategy]
+code = "start:
+c CVC4,1.5 1 1000
+c Z3,4.4.1 1 1000
+c Alt-Ergo,2.0.0 1 1000
+t split_all_full start
+c CVC4,1.5 10 4000
+c Z3,4.4.1 10 4000
+c Alt-Ergo,2.0.0 10 4000
+"
+desc = "Automatic@ run@ of@ main@ provers"
+name = "Auto_level_1"
+shortcut = "1"
+
+[strategy]
+code = "
+t compute_specified start
+start:
+c CVC4,1.6 1 1000
+c CVC4,1.4 1 1000
+c CVC4,1.4,noBV 1 1000
+c CVC4,1.6,noBV 1 1000
+c Alt-Ergo,2.0.0 1 1000
+c CVC3,2.4.1 1 1000
+t split_vc start
+c CVC4,1.6 5 2000
+c CVC4,1.4 5 2000
+c CVC4,1.4,noBV 5 2000
+c CVC4,1.6,noBV 5 2000
+c Alt-Ergo,2.0.0 5 2000
+c CVC3,2.4.1 5 2000
+t compute_in_goal start
+g trylongertime
+trylongertime:
+c CVC4,1.4,noBV 30 4000
+c CVC4,1.6,noBV 30 4000
+c CVC3,2.4.1 30 4000
+"
+desc = "Automatic@ run@ of@ main@ provers and@ most@ useful@ avr@ transformations"
+name = "Split_and_compute"
+shortcut = "3"
+
+[strategy]
+code = "c CVC4,1.5 1 1000
+c Z3,4.4.1 1 1000
+c Alt-Ergo,2.0.0 1 1000
+"
+desc = "Automatic@ run@ of@ main@ provers"
+name = "Auto_level_0"
+shortcut = "0"
+
+[strategy]
+code = "c CVC4,1.4,noBV 600 20000"
+desc = "10 minute run of cvc4"
+name = "CVC4_Crunch"
+
+[uninstalled_prover policy0]
+alternative = "noBV"
+name = "Z3"
+policy = "upgrade"
+target_alternative = "noBV"
+target_name = "Z3"
+target_version = "4.4.1"
+version = "4.5.0"