new tests from bugs reported in the BTS. Bug 16972 fixed

ROADMAP

@@ -147,6 +147,24 @@ and no epsilon
    chaque instance necessaires. plutot qu'un seul symbole _match
    polymorphe.
 
+==================== Roadmap for release 0.87 ========================
+
+DATE : ?
+
+Release Notes (details in file CHANGES):
+
+== TODO ==
+
+* Coq realization of bitvector theory
+
+* make counter-examples feature more robust
+
+* support for both isabelle 2014 and 2015
+
+* review support for division operators by SMT provers
+
+* take some time to fix some bugs of the BTS: 18029 at least
+
 ==================== Roadmap for release 0.86 ========================
 
 DATE : fin avril / début mai

examples/bts/16972.mlw

+
+module M
+
+  use import HighOrd
+
+  type t = A | B
+  type s = { field1 : t -> t ; field2 : t -> t }
+
+  function const (x:'b) : 'a -> 'b = \y:'a.x
+
+  predicate p (u:s) (a b:t) = u.field1 = const a /\ u.field2 = const b
+
+  let fail (u:s) : unit
+    requires { p u A A }
+    ensures { u.field1 = u.field2 }
+  = ()
+
+end

examples/bts/16972/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
+<file name="../16972.mlw" expanded="true">
+<theory name="M" sum="9422b749a767ddf788c2af5b11303c86" expanded="true">
+ <goal name="WP_parameter fail" expl="VC for fail" expanded="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>

examples/bts/17184.mlw

+
+(*
+
+
+Error message: This expression has type t <> 'a 'b, but is expected to have type t 'a1 'a2
+
+Clone substitute every occurence of the type by the logic version, while
+we expect to use the program version in add.
+
+*)
+
+module A
+
+  type t
+
+  val add t : unit
+
+end
+
+module B
+
+  type t = { ghost a : unit }
+
+  clone A with type t = t
+
+  let sub (x:t) : unit = A.add x
+
+end

tests/test-claude.why

@@ -235,4 +235,13 @@ theory TestPVSRealAbs
 
   lemma l: A.abs (-. 1.0) = 1.0
 
-end
\ No newline at end of file
+end
+
+theory TestTransform
+
+ predicate a int
+ predicate b int
+
+ lemma L: a 1 /\ b 2
+
+end