fix smtv2 printer

also, remove all customization from the Z3 3.x section in prover detection.
I find it morally wrong to chase magic options of a closed-source program.
We should add an option for a prover only when we have clear understanding
of what it does and good reasons to believe that it is useful in our case.

share/provers-detection-data.conf.in

@@ -31,6 +31,19 @@ version_old = "0.8"
 command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
 driver = "drivers/alt_ergo.drv"
 
+[ATP cvc3]
+name = "CVC3"
+exec = "cvc3"
+version_switch = "-version"
+version_regexp = "This is CVC3 version \\([^ \n]+\\)"
+version_ok = "2.4.1"
+version_ok = "2.4"
+version_bad = "2.2"
+version_bad = "2.1"
+# the -timeout option is unreliable in CVC3 2.4.1
+command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
+driver = "drivers/cvc3.drv"
+
 [ATP cvc3]
 name = "CVC3"
 exec = "cvc3"
@@ -62,7 +75,7 @@ name = "Eprover"
 exec = "eprover"
 version_switch = "--version"
 version_regexp = "E \\([^\n]+\\)"
-version_ok = "1.4 Namring"   
+version_ok = "1.4 Namring"
 # we pass time 0 to why3-cpulimit to avoid race
 command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
 driver = "drivers/tptp.drv"
@@ -144,17 +157,8 @@ version_bad = "2.2"
 version_bad = "2.1"
 version_bad = "1.3"
 driver = "drivers/z3.drv"
-command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smtc \
--rs:42 \
-PHASE_SELECTION=0 \
-RESTART_STRATEGY=0 \
-RESTART_FACTOR=1.5 \
-QI_EAGER_THRESHOLD=100 \
-ARITH_RANDOM_INITIAL_VALUE=true \
-CASE_SPLIT=3 \
-DELAY_UNITS=true \
-DELAY_UNITS_THRESHOLD=16 \
-%f"
+# the -T is unreliable in Z3 3.2
+command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt2 -rs:42 %f"
 
 [ATP z3]
 name = "Z3"

src/printer/smtv2.ml

@@ -206,10 +206,10 @@ and print_fmla info fmt f = match f.t_node with
   | Tbinop (Tor, f1, f2) ->
       fprintf fmt "@[(or@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
   | Tbinop (Timplies, f1, f2) ->
-      fprintf fmt "@[(implies@ %a@ %a)@]"
+      fprintf fmt "@[(=>@ %a@ %a)@]"
         (print_fmla info) f1 (print_fmla info) f2
   | Tbinop (Tiff, f1, f2) ->
-      fprintf fmt "@[(iff@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
+      fprintf fmt "@[(=@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
   | Tnot f ->
       fprintf fmt "@[(not@ %a)@]" (print_fmla info) f
   | Ttrue ->
@@ -217,7 +217,7 @@ and print_fmla info fmt f = match f.t_node with
   | Tfalse ->
       fprintf fmt "false"
   | Tif (f1, f2, f3) ->
-      fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
+      fprintf fmt "@[(ite %a@ %a@ %a)@]"
         (print_fmla info) f1 (print_fmla info) f2 (print_fmla info) f3
   | Tlet (t1, tb) ->
       let v, f2 = t_open_bound tb in
@@ -231,7 +231,7 @@ and print_fmla info fmt f = match f.t_node with
 and print_expr info fmt =
   TermTF.t_select (print_term info fmt) (print_fmla info fmt)
 
-and print_trigger info fmt e = fprintf fmt "(%a)" (print_expr info) e
+and print_trigger info fmt e = fprintf fmt "%a" (print_expr info) e
 
 and print_triggers info fmt = function
   | [] -> ()