[Why3-club] how to import a theory ?

[Sandrine Blazy]

Hi,

I have in the same directory a file pair.why and a file matrix.mlw.
The file pair.why is the following.

theory Pair
  function fst (p : ('a, 'b)) : 'a =
match p with
| (a, b) -> a
end
end

The file matrix.mlw looks like the following.

module Matrix
  use import int.Int
  use import map.Map as M
  use import pair.Pair as P

  type matrix 'a model ...
 ...
end  

I've got the following error message when I load the matrix.mlw file, and I 
don't understand why.
File "matrix.mlw", line 4, characters 2-27:
Theory/module not found: pair.Pair

What do I need to do so that Why3 can find my theory called Pair ?

Thanks in advance,

Sandrine Blazy
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club

[Why3-club] Pb. with the matrix library

[Sandrine Blazy]

Hi,

I don't understand the errors I've got when I write the following module.

File "maze.mlw", line 5, characters 2-26:
Symbol set is already defined in the current scope

module Maze
  use import int.Int
  use import bool.Bool
  use import matrix.Matrix as M
  use import matrix.Syntax 

  type board = matrix int

 predicate won (b : board) (x : int) (y : int) = 
b [ (x,y) ] = 2 
end

When I remove the  use import matrix.Syntax line, I've got the following error.

File "maze.mlw", line 9, characters 6-7:
Unbound symbol 'mixfix []'

What's wrong with my b[ (x,y) ] notation ?

Thanks for your help,

Sandrine
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club

[Why3-club] CfP: VSTTE 2016

[Sandrine Blazy]

8th IFIP Working Conference on Verified Software: Theories, Tools, and 
Experiments (VSTTE 2016)
Co-located with 26th Conference on Computer Aided Verification (CAV 2016)
Toronto - Canada
July 17 - 18, 2016


The 8th IFIP Working Conference on Verified Software: Theories, Tools, and 
Experiments follows a successful inaugural working conference at Zurich in 2005 
followed by conferences in Toronto (2008), Edinburgh (2010), Philadelphia 
(2012), Atherton (2013), Vienna (2014), San Francisco (2015). The goal of this 
conference is to advance the state of the art in the science and technology of 
software verification, through the interaction of theory development, tool 
evolution, and experimental validation. 

Important Dates

• Abstract submission:  April 25, 2016, anywhere on Earth (11.59 pm, UTC-12) 
• Full paper submission:May 2, 2015, anywhere on Earth (11.59 pm, 
UTC-12)
• Notification: June 6, 2016
• Conference:   July 17–18, 2016 
• Camera-ready: August 28, 2016 

Scope

We welcome submissions describing significant advances in the production of 
verified software, i.e., software that has been proved to meet its functional 
specifications. We are especially interested in submissions describing 
large-scale verification efforts that involve collaboration, theory 
unification, tool integration, and formalized domain knowledge. We welcome 
papers describing novel experiments and case studies evaluating verification 
techniques and technologies. Topics of interest include, but are not limited 
to, education, requirements modeling, specification languages, 
specification/verification case studies, formal calculi, software design 
methods, automatic code generation, refinement methodologies, compositional 
analysis, verification tools (e.g., static analysis, dynamic analysis, model 
checking, theorem proving, satisfiability), tool integration, benchmarks, 
challenge problems, and integrated verification environments. 


Submissions

We are accepting both long (limited to 16 pages) and short (limited to 10 
pages) paper submissions. Short submissions also cover Verification Pearls 
describing an elegant proof or proof technique. Submitted research papers and 
system descriptions must be original and not submitted for publication 
elsewhere. 

Research paper submissions must be in LNCS format and must include a cogent and 
self-contained description of the ideas, methods, results, and comparison to 
existing work. Submissions of theoretical, practical, and experimental 
contributions are equally encouraged, including those that focus on specific 
problems or problem domains. 

Papers can be submitted at https://easychair.org/conferences/?conf=vstte2016 
<https://easychair.org/conferences/?conf=vstte2016> 
Submissions that arrive late, are not in the proper format, or are too long 
will not be considered. The post-conference proceedings of VSTTE 2016 will be 
published by Springer-Verlag in the LNCS series. Authors of accepted papers 
will be requested to sign a form transferring copyright of their contribution 
to Springer-Verlag. The use of LaTeX and the Springer llncs class files, 
obtainable from the Springer website is strongly encouraged. 

Springer website: http://www.springer.de/comp/lncs/authors.html 
<http://www.springer.de/comp/lncs/authors.html>

Program Committee

Sandrine Blazy, (Rennes, France) Co-Chair 
Marsha Chechik (University of Toronto, Canada) Co-Chair 
Ernie Cohen (Amazon, USA) 
Temeghen Kahsai (NASA Ames / CMU , USA) General Chair
Natarajan Shankar (SRI, USA) 
Arie Gurfinkel (CMU / SEI, USA) 
Rustan Leino (Microsoft, USA) 
Natasha Sharygina (Lugano, Switzerland) 
Jean-Christophe Filliâtre (CNRS, France) 
Tiziana Margaria (LERO, Ireland) 
Vijay Ganesh (University of Waterloo, Canada) 
Bill Harris (Georgia Institute of Technology, USA) 
Nadia Polikarpova (MIT, USA) 
Kristin Yvonne Rozier (University of Cincinnati, USA)
Richard Trefler  (University of Waterloo, Canada) 
Mike Whalen  (University of Minnesota, USA) 
June Andronick (NICTA, Australia) 
Frédéric Besson (INRIA, France) 
Nikolaj Bjorner (Microsoft, USA) 
Vladimir Klebanov (Karlsruhe Institute of Technology, Germany) 
David Naumann (Stevens Institute of Technology, USA) 
Deepak D'Souza (Indian Institute of Science, Bangalore, India) 
Naijun Zhan (Chinese Academy of Sciences, China)___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] proof of a test program

[Sandrine Blazy]

Hi,

I am using Why3 0.87.3 to prove the following test program of the selection 
sort given in the gallery of verified programs 
(http://toccata.lri.fr/gallery/selection_sort.en.html 
).

 let test1 () =
   let a = make 3 0 in
   a[0] <- 7; a[1] <- 3; a[2] <- 1;
   selection_sort a;
   assert { a [0] = 1 };
   assert { a [1] = 3 };
   assert { a [2] = 7 };
   a

None of my provers (Alt-Ergo, cvc3, cvc4, Eprover, Z3) is able to prove any of 
these 3 assertions. However, if I choose the "get counter-example" option in 
the preference window, then cvc4 manages to prove this test program.

Does it mean that I should always choose this "get counter-example" option, 
even if I am not using this feature ?

Thanks,

Sandrine


signature.asc
Description: Message signed with OpenPGP
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] defining a type invariant

[Sandrine Blazy]

Hi,

I would like to define a type invariant related to an array type.
If I write for example :
type myarray = array int
invariant { forall i:int. 0 <=i< length self -> my_predicate self[i] }

then I get the following error message:
type aliases cannot have invariants.

So, I changed my definition to the following one :
type tmyarray = { myarray : array int }
invariant { forall i:int. 0 <= i < length self.myarray ->
  my_predicate (self.myarray[i]) }

This definition is ok, but the use of a record requires to construct and
destruct many of such records in my spec and my code. So, I am wondering
if there is a better way to define my type invariant.

Best,

Sandrine



signature.asc
Description: Message signed with OpenPGP
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] trying to use FsetSum.sum

[Sandrine Blazy]

Hi,

I’d like to use the sum function of the set.FsetSum theory:
function sum <> (set  'a) ('a -> int) 
: int

I have a function f : ‘a -> int. When I am defining
function sum_set (s: set ‘a) : int = sum s f

I got the following error message:
This term has type set 'a, but is expected to have type set1 ‘xi

What’s wrong with s in this definition ?

Best,
Sandrine



signature.asc
Description: Message signed with OpenPGP
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] Why3-club Digest, Vol 87, Issue 13

[Sandrine Blazy]

> Le 13 mars 2018 à 12:00, why3-club-requ...@lists.gforge.inria.fr a écrit :
> 
> Le 12/03/2018 à 16:23, Sandrine Blazy a écrit :
> 
>> I have a function f : ‘a -> int. When I am defining
>> function sum_set (s: set ‘a) : int = sum s f
>> 
>> I got the following error message:
>> This term has type set 'a, but is expected to have type set1 ‘xi
>> 
>> What’s wrong with s in this definition ?
> 
> Given the error message, I would say that the "set" type used in "sum"
> later got shadowed by another type with the same name.
> 
Thanks !
Indeed, I was importing too many modules.

Best,

Sandrine


signature.asc
Description: Message signed with OpenPGP
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] using bool values in why3 1.1.0

[Sandrine Blazy]

Hi, 

the following example worked fine using why3 version 0.87.3.
How should I write it so that it becomes accepted by why3 version 1.1.0 ?

module M
  use int.Int
  use bool.Bool
  use array.Array

predicate p (a: array int) (i:int) = (a[i]=0)

let f (a: array int) (i: int) : bool
requires { 0 <= i < length a }
ensures { result <-> p i}
=
a[i] = 0

end
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] Why3-club Digest, Vol 95, Issue 2

[Sandrine Blazy]

Sorry for the noise.
Here is the example that is not accepted by why3 anymore.
I don’t understand why a[i] is expected to have type int.

Best,

Sandrine

-

module Mt
  use int.Int
  use bool.Bool
  use array.Array

type cell = A | B | C

predicate p (a: array cell) (i:int) = (a[i] = A)

let f (a: array cell) (i: int) : bool
requires {  0 <= i < length a }
ensures { result <-> p a i }
=
a [i] = A
(* This expression has type Mt.cell, but is expected to have type int *)

end

> Le 10 nov. 2018 à 12:00, why3-club-requ...@lists.gforge.inria.fr a écrit :
> 
> It looks like you forgot the first parameter "a" of "p" in "result <-> p
> i". When I add it, this is accepted (and proved) with the most recent
> version of Why3.
> 
> --
> Jean-Christophe
> 
> On 11/9/18 6:20 PM, Sandrine Blazy wrote:
>> Hi, 
>> 
>> the following example worked fine using why3 version 0.87.3.
>> How should I write it so that it becomes accepted by why3 version 1.1.0 ?
>> 
>> module M
>>  use int.Int
>>  use bool.Bool
>>  use array.Array
>> 
>> predicate p (a: array int) (i:int) = (a[i]=0)
>> 
>> let f (a: array int) (i: int) : bool
>> requires { 0 <= i < length a }
>> ensures { result <-> p i}
>> =
>> a[i] = 0
>> 
>> end

___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] pb. with cloning

[Sandrine Blazy]

Hello,

I would like to reuse the insertion sort from the Why3 gallery.
The following code was working in version 0.87, but it is not accepted anymore 
by version 1.1.0.
What is wrong with my lecolor predicate ?

Best,

Sandrine

module InsertionSort (* from Why3 gallery *)

  type elt
  val predicate le elt elt

  clone relations.TotalPreOrder with
type t = elt, predicate rel = le, axiom .
  clone export list.Sorted with
type t = elt, predicate le  = le, goal Transitive.Trans

  use list.List
  use list.Permut

  let rec insert (x: elt) (l: list elt) : list elt
requires { sorted l }
ensures  { sorted result }
ensures  { permut (Cons x l) result }
variant  { l }
  = match l with
| Nil -> Cons x Nil
| Cons y r -> if le x y then Cons x l else Cons y (insert x r)
end

  let rec insertion_sort (l: list elt) : list elt
ensures { sorted result }
ensures { permut l result }
variant { l }
  = match l with
| Nil -> Nil
| Cons x r -> insert x (insertion_sort r)
end

end

 module M
  use list.List

type color = B | W | R

val (=) (x y : color) : bool
ensures { result <-> x=y}

predicate lecolor (e1 e2: color) =
match e1 with
   B -> True
 | W -> not (e2 = B)
 | R -> e2 = R
end

clone InsertionSort with type elt = color, predicate le  = lecolor
  
(*  Illegal instantiation for symbol le *)

(* … *)
end 

___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] pb. with cloning

[Sandrine Blazy]

Thanks for your prompt answer.
Unfortunately, in the instantiation, Why3 complains that "val le = lecolor"  is 
a syntax error.

Sandrine

> Le 13 nov. 2018 à 14:08, Andrei Paskevich  a écrit :
> 
> Hi Sandrine,
> 
> you try to instantiate a "val predicate" with a purely logical predicate.  
> You should declare "lecolor" as "let predicate" and instantiate using "val le 
> = lecolor".
> 
> Hope it helps,
> Andrei
> 
> On 13 November 2018 at 14:04, Sandrine Blazy  <mailto:sandrine.bl...@irisa.fr>> wrote:
> Hello,
> 
> I would like to reuse the insertion sort from the Why3 gallery.
> The following code was working in version 0.87, but it is not accepted 
> anymore by version 1.1.0.
> What is wrong with my lecolor predicate ?
> 
> Best,
> 
> Sandrine
> 
> module InsertionSort (* from Why3 gallery *)
> 
>   type elt
>   val predicate le elt elt
> 
>   clone relations.TotalPreOrder with
> type t = elt, predicate rel = le, axiom .
>   clone export list.Sorted with
> type t = elt, predicate le  = le, goal Transitive.Trans
> 
>   use list.List
>   use list.Permut
> 
>   let rec insert (x: elt) (l: list elt) : list elt
> requires { sorted l }
> ensures  { sorted result }
> ensures  { permut (Cons x l) result }
> variant  { l }
>   = match l with
> | Nil -> Cons x Nil
> | Cons y r -> if le x y then Cons x l else Cons y (insert x r)
> end
> 
>   let rec insertion_sort (l: list elt) : list elt
> ensures { sorted result }
> ensures { permut l result }
> variant { l }
>   = match l with
> | Nil -> Nil
> | Cons x r -> insert x (insertion_sort r)
> end
> 
> end
> 
>  module M
>   use list.List
> 
> type color = B | W | R
> 
> val (=) (x y : color) : bool
> ensures { result <-> x=y}
> 
> predicate lecolor (e1 e2: color) =
> match e1 with
>B -> True
>  | W -> not (e2 = B)
>  | R -> e2 = R
> end
> 
> clone InsertionSort with type elt = color, predicate le  = lecolor
> 
> (*  Illegal instantiation for symbol le *)
> 
> (* … *)
> end 
> 
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr <mailto:Why3-club@lists.gforge.inria.fr>
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club 
> <https://lists.gforge.inria.fr/mailman/listinfo/why3-club>
> 

___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] pb. with cloning

[Sandrine Blazy]

Thanks for your help.
I have removed the « predicate » keyword and it works.

Sandrine

> Le 13 nov. 2018 à 18:25, Andrei Paskevich  a écrit :
> 
> Hmm, the following works for me in master:
> =
> let predicate lecolor (e1 e2: color) =
> match e1 with
>B -> True
>  | W -> not (e2 = B)
>  | R -> e2 = R
> end
> 
> clone InsertionSort with type elt = color, val le  = lecolor
> =
> 
> What version do you currenly use?
> 
> A.
> 
> 
> On 13 November 2018 at 14:22, Sandrine Blazy  <mailto:sandrine.bl...@irisa.fr>> wrote:
> Thanks for your prompt answer.
> Unfortunately, in the instantiation, Why3 complains that "val le = lecolor"  
> is a syntax error.
> 
> Sandrine
> 
> 
>> Le 13 nov. 2018 à 14:08, Andrei Paskevich > <mailto:andrei.paskev...@lri.fr>> a écrit :
>> 
>> Hi Sandrine,
>> 
>> you try to instantiate a "val predicate" with a purely logical predicate.  
>> You should declare "lecolor" as "let predicate" and instantiate using "val 
>> le = lecolor".
>> 
>> Hope it helps,
>> Andrei
>> 
>> On 13 November 2018 at 14:04, Sandrine Blazy > <mailto:sandrine.bl...@irisa.fr>> wrote:
>> Hello,
>> 
>> I would like to reuse the insertion sort from the Why3 gallery.
>> The following code was working in version 0.87, but it is not accepted 
>> anymore by version 1.1.0.
>> What is wrong with my lecolor predicate ?
>> 
>> Best,
>> 
>> Sandrine
>> 
>> module InsertionSort (* from Why3 gallery *)
>> 
>>   type elt
>>   val predicate le elt elt
>> 
>>   clone relations.TotalPreOrder with
>> type t = elt, predicate rel = le, axiom .
>>   clone export list.Sorted with
>> type t = elt, predicate le  = le, goal Transitive.Trans
>> 
>>   use list.List
>>   use list.Permut
>> 
>>   let rec insert (x: elt) (l: list elt) : list elt
>> requires { sorted l }
>> ensures  { sorted result }
>> ensures  { permut (Cons x l) result }
>> variant  { l }
>>   = match l with
>> | Nil -> Cons x Nil
>> | Cons y r -> if le x y then Cons x l else Cons y (insert x r)
>> end
>> 
>>   let rec insertion_sort (l: list elt) : list elt
>> ensures { sorted result }
>> ensures { permut l result }
>> variant { l }
>>   = match l with
>> | Nil -> Nil
>> | Cons x r -> insert x (insertion_sort r)
>> end
>> 
>> end
>> 
>>  module M
>>   use list.List
>> 
>> type color = B | W | R
>> 
>> val (=) (x y : color) : bool
>> ensures { result <-> x=y}
>> 
>> predicate lecolor (e1 e2: color) =
>> match e1 with
>>B -> True
>>  | W -> not (e2 = B)
>>  | R -> e2 = R
>> end
>> 
>> clone InsertionSort with type elt = color, predicate le  = lecolor
>> 
>> (*  Illegal instantiation for symbol le *)
>> 
>> (* … *)
>> end 
>> 
>> ___
>> Why3-club mailing list
>> Why3-club@lists.gforge.inria.fr <mailto:Why3-club@lists.gforge.inria.fr>
>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club 
>> <https://lists.gforge.inria.fr/mailman/listinfo/why3-club>
>> 
> 
> 

___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] keyboard shortcut for provers

[Sandrine Blazy]

Hello,

In my why3 IDE, there is no keyboard shortcut for my installed provers.
Instead of a shortcut, I see « VoidSymbol » for each of my provers.
Is there a way to define a shortcut for a given prover ?

Best,

Sandrine

___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] strange loops in the sequence library

[Sandrine Blazy]

Hello,

in the library of sequences, several definitions use a while loop that is never 
executed.
For instance, the function set <> (s:seq 
 'a) (i:int) (v:'a) : seq 
 'a starts with
while false do variant { 0 } () done;
Are these loops mandatory ?

Sandrine___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] Why3-club Digest, Vol 95, Issue 7

[Sandrine Blazy]

Dear Claude,

> Le 15 nov. 2018 à 12:01, why3-club-requ...@lists.gforge.inria.fr a écrit :
> 
> Since Why3 1.0 we wanted to disencourage users to intentionally choose a 
> particular prover to discharge a goal. We want to encourage instead the 
> use of the shortcut "0" "1" and "2" that selects a "strategy" which will 
> try several provers.
> 
> In essence, for begineers we suggest to try first "0", if it fails use 
> "s" to split, then "0" again on subgoals. Then on each specific unproved 
> subgoals, an option is to try "1" or "2 ».

Thanks for the advice; we asked our students to follow this strategy which 
worked very well until now.
However, the proof window shows that  "s" calls the transformation
split_vc, and strategy   « 1 » uses the transformation split_all_full.

What is the difference between both transformations, and when should I try
to split again instead of using strategy 1 ? Indeed, on some examples, 
« 1 » followed by « 2 » does not help, but splitting again followed by « 0 » 
is enough to prove the VCs.

Sandrine

> - Claude
> 
> Le 14/11/2018 à 18:55, Sandrine Blazy a écrit :
>> Hello,
>> 
>> In my why3 IDE, there is no keyboard shortcut for my installed provers.
>> Instead of a shortcut, I see « VoidSymbol » for each of my provers.
>> Is there a way to define a shortcut for a given prover ?

___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] Problem installing why3 using opam

[Sandrine Blazy]

Hi,
can anyone help with this installation failure? 
Thanks,
Sandrine

% opam install why3
The following actions will be performed:
  ∗ install why3 1.3.1

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫 
[why3.1.3.1] found in cache

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫 
[ERROR] The compilation of why3 failed at 
"/Users/blazy/.opam/opam-init/hooks/sandbox.sh build make -j15 all opt byte".

#=== ERROR while compiling why3.1.3.1 =#
# context 2.0.7 | macos/x86_64 | ocaml-system.4.09.0 | 
https://opam.ocaml.org#3b3a3c0d 
# path~/.opam/default/.opam-switch/build/why3.1.3.1
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j15 all opt byte
# exit-code   2
# env-file~/.opam/log/why3-97766-d2c37b.env
# output-file ~/.opam/log/why3-97766-d2c37b.out
### output ###
# src/server/server-unix.c:244:3: error: implicitly declaring library function 
'memcpy' with type 'void *(void *, const void *, unsigned long)' 
[-Werror,-Wimplicit-function-declaration]
# [...]
#   ^
# src/server/server-unix.c:244:3: note: include the header  or 
explicitly provide a declaration for 'memcpy'
# src/server/server-unix.c:356:37: error: implicitly declaring library function 
'strerror' with type 'char *(int)' [-Werror,-Wimplicit-function-declaration]
#   unix_argv[0],unix_argv[0],strerror(errno));
# ^
# src/server/server-unix.c:356:37: note: include the header  or 
explicitly provide a declaration for 'strerror'
# Ocamlopt src/util/mlmpfr_wrapper.ml
# 6 errors generated.
# Ocamlopt src/util/util.ml
# make: *** [src/server/server-unix.o] Error 1
# make: *** Waiting for unfinished jobs___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] provers triggered by proof strategies

[Sandrine Blazy]

Hello,

I am using why3 version 1.3.3 and would like to add the Z3 and E provers to the 
list of installed provers, so that they are triggered by proof strategies 0, 1 
and more. I tried several versions (among those listed in 
provers-detection-data.conf), including Z3 version 4.8.4 (that is mentioned in 
the documentation for proof strategies). However, none of them is triggered by 
strategies 0 and 1. Which version of Z3 and E should I use?

My other question is about TryWhy3: which version of why3 does it use ?

Thanks,
Sandrine___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] Why3-club Digest, Vol 119, Issue 2

[Sandrine Blazy]

> Le 4 déc. 2020 à 12:00, why3-club-requ...@lists.gforge.inria.fr a écrit :
> 
> 
> Le 03/12/2020 à 09:24, Sandrine Blazy a écrit :
> 
>> My other question is about TryWhy3: which version of why3 does it use?
> 
> I am updating it at the time of release. So, it should be 1.3.3.


Thanks!

I managed to solve my other issue: I used why3 config —detect-provers 
(instead of why3 config --add-prover …) to install all the provers. 
Now all provers are detected by the proof strategies.

Best,
Sandrine___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club