- correct bv test output

- add "map" to the smtv2 printer blacklist (from z3)
- change smtv2 driver so that errors (in particular z3's) are correctly reported

drivers/smt-libv2.drv

@@ -4,11 +4,12 @@ prelude ";;; this is a prelude for smt-lib v2"
 
 printer "smtv2"
 filename "%f-%t-%g.smt2"
-valid "^unsat"
 unknown "^\\(unknown\\|sat\\|Fail\\)" ""
-outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+outofmemory "^(error \".*out of memory\")\\|Cannot allocate memory"
+fail "^(error \"\\(.*\\)\")" "Error: \1"
 timeout "interrupted by timeout"
 time "why3cpulimit time : %s s"
+valid "^unsat"
 
 (* À discuter *)
 transformation "inline_trivial"

examples/tests-provers/bv/why3session.xml

@@ -7,7 +7,7 @@
 <prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
 <prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
 <file name="../bv.why" expanded="true">
-<theory name="CheckBV64" sum="fe7139da2eda649fe69da9f64adc83de">
+<theory name="CheckBV64" sum="fe7139da2eda649fe69da9f64adc83de" expanded="true">
  <goal name="ok_zero">
  <proof prover="0"><result status="valid" time="0.02" steps="66"/></proof>
  <proof prover="1"><result status="valid" time="0.02"/></proof>
@@ -151,8 +151,7 @@
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
- <goal name="ok24">
- <proof prover="0"><result status="valid" time="0.85" steps="342"/></proof>
+ <goal name="ok24" expanded="true">
  <proof prover="1"><result status="valid" time="0.45"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
@@ -723,8 +722,7 @@
  <proof prover="2"><result status="valid" time="0.03"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
- <goal name="ok24">
- <proof prover="0"><result status="valid" time="3.36" steps="332"/></proof>
+ <goal name="ok24" expanded="true">
  <proof prover="1"><result status="valid" time="0.59"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
@@ -943,8 +941,7 @@
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
- <goal name="ok24">
- <proof prover="0"><result status="valid" time="3.82" steps="332"/></proof>
+ <goal name="ok24" expanded="true">
  <proof prover="1"><result status="valid" time="0.64"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>

src/printer/smtv2.ml

@@ -63,7 +63,10 @@ let ident_printer =
       "Bool"; "true"; "false";
       "Array";"const";
       "abs";
-      "BitVec"; "extract"; "bv2nat"; "nat2bv"
+      "BitVec"; "extract"; "bv2nat"; "nat2bv";
+
+      (** From Z3 *)
+      "map"
       ]
   in
   let san = sanitizer char_to_alpha char_to_alnumus in