Merge branch 'master' into itp

.gitignore

@@ -51,6 +51,7 @@ why3.conf
 /bench/programs/good/loops/
 /bench/programs/good/po/
 /bench/valid/list/
+/bench/ce/*.out
 
 # /bin/
 /bin/why3.byte

bench/ce-bench

+#!/bin/sh
+
+dir=`dirname $0`
+
+case "$1" in
+  "-update-oracle")
+        updateoracle=true;;
+  "")
+        updateoracle=false;;
+  *)
+        echo "$0: Unknown option '$1'"
+        exit 2
+esac
+
+
+run_cvc4_15 () {
+  echo -n "  $1... "
+  $dir/../bin/why3prove.opt -P "CVC4,1.5-prerelease" --get-ce $1 > $1.out
+  if cmp $1.oracle $1.out > /dev/null 2>&1 ; then
+     echo "ok"
+  else
+     if $updateoracle; then
+        echo "Updating oracle for $1"
+        mv $1.out $1.oracle
+     else
+       echo "FAILED!"
+       echo "diff is the following:"
+       diff $1.oracle $1.out
+     fi
+  fi
+}
+
+
+
+
+
+for f in $dir/ce/*.mlw; do
+    run_cvc4_15 $f
+done

bench/ce/logic.mlw

+
+theory T
+
+  use import int.Int
+
+  goal g0 : forall x "model":int. ("model" x >= 42) -> ("model" x + 3 <= 50)
+
+  constant g : int
+
+  goal g1 : forall x "model":int. ("model" g >= x)
+
+  goal g2 : forall x1 "model" "model_trace:X" x2 "model" x3 "model" x4 "model" x5 "model" x6 "model" x7 "model" x8 "model".
+  ("model" "model_trace: X1 + 1 = 2" x1 + 1 = 2) ->
+  ("model" x2 + 1 = 2) ->
+  ("model" x3 + 1 = 2) ->
+  ("model" x4 + 1 = 2) ->
+  ("model" x5 + 1 = 2) ->
+  ("model" x6 + 1 = 2) ->
+  ("model" x7 + 1 = 2) ->
+  ("model" x8 + 1 = 2) ->
+  ("model" x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 = 2)
+
+end

bench/ce/logic.mlw.oracle

+bench/ce/logic.mlw T g0 : Invalid (0.00s)
+Counter-example model:File bench/ce/logic.mlw:
+Line 6:
+x = {"type" : "Integer" ,
+"val" : "48" }
+
+bench/ce/logic.mlw T g1 : Invalid (0.00s)
+Counter-example model:File bench/ce/logic.mlw:
+Line 10:
+x = {"type" : "Integer" ,
+"val" : "0" }
+
+bench/ce/logic.mlw T g2 : Invalid (0.00s)
+Counter-example model:File bench/ce/logic.mlw:
+Line 12:
+X = {"type" : "Integer" , "val" : "1" }
+x2 = {"type" : "Integer" ,
+"val" : "1" }
+x3 = {"type" : "Integer" ,
+"val" : "1" }
+x4 = {"type" : "Integer" ,
+"val" : "1" }
+x5 = {"type" : "Integer" ,
+"val" : "1" }
+x6 = {"type" : "Integer" ,
+"val" : "1" }
+x7 = {"type" : "Integer" ,
+"val" : "1" }
+x8 = {"type" : "Integer" ,
+"val" : "1" }
+

examples/nightly-bench.sh

@@ -136,6 +136,16 @@ else
     echo "Make bench succeeded. " >> $REPORT
 fi
 
+# run regression bench for counterexamples
+bench/ce-bench &> $OUT
+if test "$?" != "0" ; then
+    echo "Counterexample regression tests FAILED" >> $REPORT
+    cat $OUT >> $REPORT
+    SUBJECT="$SUBJECT (CE regression failed)"
+else
+    echo "Counterexample regression tests succeeded. " >> $REPORT
+fi
+
 
 # replay proofs
 examples/regtests.sh &> $OUT

examples/tests-provers/bv/why3session.xml

@@ -9,7 +9,7 @@
 <prover id="4" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Alt-Ergo" version="1.01" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../bv.why" expanded="true">
-<theory name="CheckBV64" sum="a69e7936e9b3736b53a1a06d1557d503" expanded="true">
+<theory name="CheckBV64" sum="a69e7936e9b3736b53a1a06d1557d503">
  <goal name="ok_zero" expl="">
  <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
  <proof prover="1"><result status="valid" time="0.02"/></proof>
@@ -208,19 +208,19 @@
  <proof prover="3"><result status="timeout" time="0.92"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke6" expl="" expanded="true">
+ <goal name="smoke6" expl="">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
  <proof prover="1"><result status="unknown" time="0.46"/></proof>
  <proof prover="2"><result status="unknown" time="0.00"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke7" expl="" expanded="true">
+ <goal name="smoke7" expl="">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof>
  <proof prover="1"><result status="unknown" time="0.51"/></proof>
  <proof prover="2"><result status="unknown" time="0.01"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke8" expl="" expanded="true">
+ <goal name="smoke8" expl="">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
  <proof prover="1"><result status="unknown" time="0.44"/></proof>
  <proof prover="2"><result status="unknown" time="0.00"/></proof>
@@ -382,7 +382,7 @@
  <proof prover="4"><result status="valid" time="0.02"/></proof>
  </goal>
 </theory>
-<theory name="CheckBV32" sum="9a0215c8a7245c48b487371f67df8950">
+<theory name="CheckBV32" sum="9a0215c8a7245c48b487371f67df8950" expanded="true">
  <goal name="ok_zero" expl="">
  <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
  <proof prover="1"><result status="valid" time="0.03"/></proof>
@@ -596,15 +596,14 @@
  <proof prover="3"><result status="timeout" time="0.96"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke8" expl="">
+ <goal name="smoke8" expl="" expanded="true">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof>
  <proof prover="1"><result status="unknown" time="0.44"/></proof>
  <proof prover="2"><result status="unknown" time="0.00"/></proof>
- <proof prover="3"><result status="timeout" time="0.92"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
 </theory>
-<theory name="CheckBV16" sum="b944f76414b884563c0502c12ba6dc16">
+<theory name="CheckBV16" sum="b944f76414b884563c0502c12ba6dc16" expanded="true">
  <goal name="ok_zero" expl="">
  <proof prover="0"><result status="valid" time="0.04" steps="87"/></proof>
  <proof prover="1"><result status="valid" time="0.04"/></proof>
@@ -784,7 +783,7 @@
  <proof prover="3"><result status="timeout" time="0.96"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke3" expl="">
+ <goal name="smoke3" expl="" expanded="true">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
  <proof prover="1"><result status="unknown" time="0.48"/></proof>
  <proof prover="2"><result status="unknown" time="0.01"/></proof>
@@ -818,15 +817,14 @@
  <proof prover="3"><result status="timeout" time="0.95"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke8" expl="">
+ <goal name="smoke8" expl="" expanded="true">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
  <proof prover="1"><result status="unknown" time="0.43"/></proof>
  <proof prover="2"><result status="unknown" time="0.00"/></proof>
- <proof prover="3"><result status="timeout" time="0.97"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
 </theory>
-<theory name="CheckBV8" sum="05518dc91aa5666cf77ec6c0d7299767">
+<theory name="CheckBV8" sum="05518dc91aa5666cf77ec6c0d7299767" expanded="true">
  <goal name="ok_zero" expl="">
  <proof prover="0"><result status="valid" time="0.04" steps="87"/></proof>
  <proof prover="1"><result status="valid" time="0.05"/></proof>
@@ -1040,11 +1038,10 @@
  <proof prover="3"><result status="timeout" time="0.94"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke8" expl="">
+ <goal name="smoke8" expl="" expanded="true">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof>
  <proof prover="1"><result status="unknown" time="0.45"/></proof>
  <proof prover="2"><result status="unknown" time="0.01"/></proof>
- <proof prover="3"><result status="timeout" time="0.94"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="0.99"/></proof>
  </goal>
 </theory>

share/provers-detection-data.conf

@@ -13,7 +13,6 @@ command = "%e -timelimit %t %f"
 command_steps = "%e -steps-bound %S %f"
 driver = "alt_ergo"
 editor = "altgr-ergo"
-use_at_auto_level = 1
 
 [ATP alt-ergo]
 name = "Alt-Ergo"
@@ -28,6 +27,7 @@ command = "%e -timelimit %t %f"
 command_steps = "%e -steps-bound %S %f"
 driver = "alt_ergo"
 editor = "altgr-ergo"
+use_at_auto_level = 1
 
 [ATP alt-ergo]
 name = "Alt-Ergo"

src/driver/prove_client.ml

@@ -17,16 +17,27 @@ exception InvalidAnswer of string
 
 let is_connected () = !socket <> None
 
-let client_connect socket_name =
+let client_connect ~fail socket_name =
   if !socket <> None then raise AlreadyConnected;
-  if Sys.os_type = "Win32" then begin
+  try
+    let sock =
+      if Sys.os_type = "Win32" then
         let name = "\\\\.\\pipe\\" ^ socket_name in
-    socket := Some (Unix.openfile name [Unix.O_RDWR] 0)
-  end else begin
+        Unix.openfile name [Unix.O_RDWR] 0
+      else
       let sock = Unix.socket Unix.PF_UNIX Unix.SOCK_STREAM 0 in
       Unix.connect sock (Unix.ADDR_UNIX socket_name);
+      sock
+    in
     socket := Some sock
-  end
+  with
+  | Unix.Unix_error(err, func, arg) when fail ->
+     Format.eprintf "client_connect: connection failed: %s (%s,%s) (socket_name=%s)@." (Unix.error_message err) func arg socket_name;
+     exit 2
+  | e when fail ->
+     Format.eprintf "client_connect failed for some unexpected reason: %s@\nAborting.@."
+                    (Printexc.to_string e);
+     exit 2
 
 let client_disconnect () =
   match !socket with
@@ -86,7 +97,7 @@ let recv_buf : Buffer.t = Buffer.create 1024
 let connect_external socket_name =
   if is_connected () then raise AlreadyConnected;
   Buffer.clear recv_buf;
-  client_connect socket_name
+  client_connect ~fail:true socket_name
 
 let connect_internal () =
   if is_connected () then raise AlreadyConnected;
@@ -104,11 +115,11 @@ let connect_internal () =
   Unix.chdir cwd;
   (* sleep before connecting, or the server will not be ready yet *)
   let rec try_connect n d =
-    if n <= 0 then client_connect socket_name else
-    try client_connect socket_name with _ ->
+    if n <= 0 then client_connect ~fail:true socket_name else
+    try client_connect ~fail:false socket_name with _ ->
       ignore (Unix.select [] [] [] d);
       try_connect (pred n) (d *. 4.0) in
-  try_connect 4 0.1; (* 0.1, 0.4, 1.6, 6.4 *)
+  try_connect 5 0.1; (* 0.1, 0.4, 1.6, 6.4, 25.6 *)
   at_exit (fun () -> (* only if succesfully connected *)
     (try client_disconnect () with NotConnected -> ());
     ignore (Unix.waitpid [] pid))