#17155 
Fix stdlib w.r.t. why3 import

PierreYves Strub

defect

4

pre1.x

major

#17339 
`anomaly: EcLowGoal.InvalidProofTerm.` on `/>`

PierreYves Strub

defect

4

pre1.x

major

#15106 
Consider probability quantities as realvalued expressions


enhancement

2

pre1.x

normal

#15520 
request for more loop manipulation tactics

PierreYves Strub

enhancement

3

pre1.x

normal

#15647 
Can't extract easily function from tuple

PierreYves Strub

defect

3

pre1.x

normal

#15738 
Typing functor applications inside modules

PierreYves Strub

defect

3

pre1.x

normal

#15742 
Strange error raised during a call to trivial

PierreYves Strub

defect

3

pre1.x

normal

#15908 
Unification variables appear

PierreYves Strub

defect

3

pre1.x

normal

#15922 
if tactic for bd_hoare doesn't work with precondition true

Santiago ZanellaBéguelin

defect

3

pre1.x

normal

#15924 
Assertion failed in otherwise provable goal

PierreYves Strub

defect

3

pre1.x

normal

#15962 
Rewrite Fails because it didn't manage to infer type whereas it could

PierreYves Strub

defect

3

pre1.x

normal

#15966 
Something wrong with installation script?

PierreYves Strub

defect

3

pre1.x

normal

#15968 
assertion failure when fun tactic for abstract function isn't given argument

Benjamin Grégoire

defect

3

pre1.x

normal

#15996 
rewriting when using intro patterns to eliminate existentials

PierreYves Strub

defect

2

pre1.x

normal

#15998 
Problem in cloning

PierreYves Strub

defect

3

pre1.x

normal

#16001 
Instantiating an internal theory when cloning fails

PierreYves Strub

defect

3

pre1.x

normal

#16055 
confusion of x{1} and x{2} with x in cut

PierreYves Strub

enhancement

3

pre1.x

normal

#16073 
Syntax to have ={} working for explicitly quantified memory

PierreYves Strub

enhancement

1

pre1.x

normal

#16115 
Subst failed

PierreYves Strub

defect

3

pre1.x

normal

#16116 
rewrite /op failed with lambda

PierreYves Strub

defect

3

pre1.x

normal

#16138 
assertion failure when call tactic not given { ... } module restriction

Benjamin Grégoire

defect

3

pre1.x

normal

#16141 
Not catched error in split

PierreYves Strub

defect

3

pre1.x

normal

#16149 
printer bug: parentheses in types

PierreYves Strub

defect

3

pre1.x

normal

#16174 
Bug in bdhoare call

ckunz

defect

3

pre1.x

normal

#16228 
glob M computation problem with functors and inner modules for {*}

Benjamin Grégoire

defect

3

pre1.x

normal

#16264 
Bug in rewrite with let

PierreYves Strub

defect

3

pre1.x

normal

#16416 
FEL completeness  initialization

Benjamin Grégoire

enhancement

3

pre1.x

normal

#16457 
try tactic not catching case failure

PierreYves Strub

defect

2

pre1.x

normal

#16468 
try fails to catch some callrelated exceptions


defect

3

pre1.x

normal

#16628 
making nested sections work


enhancement

3

pre1.x

normal

#16629 
cloning within sections

PierreYves Strub

enhancement

3

pre1.x

normal

#16648 
Make notations and tactics on distributions and functions a bit more uniform.


enhancement

3

pre1.x

normal

#16692 
bug in apply.

PierreYves Strub

defect

4

pre1.x

normal

#16725 
Intro pattern for substitution

PierreYves Strub

enhancement

3

pre1.x

normal

#16726 
Stack overflow during unification

PierreYves Strub

defect

3

pre1.x

normal

#16737 
"declare op"

PierreYves Strub

enhancement

3

pre1.x

normal

#16751 
hoare should work on fun.

Benjamin Grégoire

defect

3

pre1.x

normal

#16772 
Weird error with inductives when aliasing constructors

PierreYves Strub

defect

3

pre1.x

normal

#16786 
Nicer treatment of datatype constructors

PierreYves Strub

enhancement

3

pre1.x

normal

#16788 
Another stack overflow during unification

PierreYves Strub

defect

3

pre1.x

normal

#16811 
inline * should not try to inline abstract function

PierreYves Strub

defect

3

pre1.x

normal

#16963 
op/pred nosmt ...

PierreYves Strub

enhancement

3

pre1.x

normal

#16964 
Warn when a variable is used before being initialized

PierreYves Strub

enhancement

3

pre1.x

normal

#16966 
Many lexer errors related to the universal projector notation (.'n)

PierreYves Strub

defect

3

pre1.x

normal

#16986 
"while >=" generates invalid goals

ckunz

defect

3

pre1.x

normal

#16990 
Generalization does not cross tuple projections.

PierreYves Strub

defect

3

pre1.x

normal

#17005 
Higherorder pattern matching


enhancement

3

pre1.x

normal

#17006 
Instantiating an abstract procedure taking nuple with a nary concrete procedure

PierreYves Strub

defect

3

pre1.x

normal

#17009 
1.x error messages

PierreYves Strub

defect

3

pre1.x

normal

#17011 
Prettyprinter in adding too much scoping annotation

PierreYves Strub

defect

2

pre1.x

normal

#17016 
Make elim and case work on tuples and records. Retire the special lemmas

PierreYves Strub

enhancement

3

pre1.x

normal

#17021 
Some judgmentcombining variants of conseq do not apply to procedures

Benjamin Grégoire

defect

3

pre1.x

normal

#17026 
EasyCrypt does not compile on Windows (win32 / cygwin)

PierreYves Strub

defect

2

pre1.x

normal

#17038 
Message with anomaly

PierreYves Strub

defect

3

pre1.x

normal

#17046 
possible tactic renaming: [proc *] > [eager proc *]

Benjamin Grégoire

enhancement

3

pre1.x

normal

#17050 
elim/let anomaly

PierreYves Strub

defect

3

pre1.x

normal

#17052 
Parse error on (**)

PierreYves Strub

defect

3

pre1.x

normal

#17053 
Bogus goal when variable shadows a module

PierreYves Strub

defect

3

pre1.x

normal

#17057 
Add the possibility to rule out the prover filtering mecanism from the command line.

PierreYves Strub

enhancement

3

pre1.x

normal

#17059 
Negative line selectors in program logic tactics

PierreYves Strub

enhancement

3

pre1.x

normal

#17065 
Invalid priority of `by` w.r.t `;`

PierreYves Strub

defect

3

pre1.x

normal

#17066 
Better error message when operator selection failed.

PierreYves Strub

enhancement

3

pre1.x

normal

#17067 
Syntax for chained case analysis of the topassumption

PierreYves Strub

enhancement

3

pre1.x

normal

#17069 
Improve error messages of the (P?R)HL tactics

PierreYves Strub

enhancement

3

pre1.x

normal

#17072 
Pretty Printer Glitches for !(_ = _)

PierreYves Strub

defect

3

pre1.x

normal

#17073 
`case` intropattern does not try to headreduce if the goal is not subject to intro.

PierreYves Strub

defect

3

pre1.x

normal

#17075 
[sp] should fail when given code positions that cannot be reached

PierreYves Strub

enhancement

3

pre1.x

normal

#17082 
SMT tactic should be interruptable.

PierreYves Strub

enhancement

4

pre1.x

normal

#17083 
Missing etareduction in conversion

Benjamin Grégoire

enhancement

3

pre1.x

normal

#17084 
syntax for nonflat proofterms

PierreYves Strub

enhancement

3

pre1.x

normal

#17087 
[conseq*] should be the default behaviour of [conseq]

PierreYves Strub

enhancement

4

pre1.x

normal

#17089 
anomaly in [sim]

Benjamin Grégoire

defect

4

pre1.x

normal

#17095 
anomaly raised by invariant form of [call upto]


defect

3

pre1.x

normal

#17096 
Unfolding should work even in the presence of several matching operators.

PierreYves Strub

enhancement

3

pre1.x

normal

#17097 
Bad prettyprinting of lists.

PierreYves Strub

defect

3

pre1.x

normal

#17099 
Forward `apply` should be accessible for the topassumption in intropatterns

PierreYves Strub

enhancement

3

pre1.x

normal

#17100 
Forward `apply` should be accessible for the topassumption in intropatterns

PierreYves Strub

enhancement

3

pre1.x

normal

#17101 
[anomaly] when defining an operator over a concrete module's globals

PierreYves Strub

defect

3

pre1.x

normal

#17102 
[anomaly] when pHL => pRHL variant of conseq is used with a bound different from [=1%r]

PierreYves Strub

defect

3

pre1.x

normal

#17106 
Unification should work modulo deltaunfolding / simplification.


enhancement

3

pre1.x

normal

#17107 
Potential mismatch between spec and lemma versions of the "pHL + HL => pHL" variant of [conseq]


defect

3

pre1.x

normal

#17108 
require clone


enhancement

3

pre1.x

normal

#17109 
Hoare adversary rule introducess references to nonexistent memories in postconditions

Benjamin Grégoire

defect

5

pre1.x

normal

#17110 
[anomaly] on using [call] with a lemma referring to the wrong procedure

PierreYves Strub

defect

2

pre1.x

normal

#17118 
Add the ability to print the axioms of the environment


enhancement

3

pre1.x

normal

#17119 
Give the ability to print subgoals

PierreYves Strub

enhancement

3

pre1.x

normal

#17120 
[rnd] allows to prove false

PierreYves Strub

defect

4

pre1.x

normal

#17122 
Clone ignores provided proof

PierreYves Strub

defect

3

pre1.x

normal

#17123 
Bad parsing on call (_: B, I)

PierreYves Strub

defect

3

pre1.x

normal

#17124 
allows to specify timeout only for smt.

PierreYves Strub

defect

3

pre1.x

normal

#17125 
Cannot clear variables referring to memory

PierreYves Strub

defect

3

pre1.x

normal

#17126 
Command and command line option for global timeout multiplier.

PierreYves Strub

enhancement

3

pre1.x

normal

#17128 
assert false in rnd.

Benjamin Grégoire

defect

3

pre1.x

normal

#17129 
bug in alias, the introduced variable has not the good type.

Benjamin Grégoire

defect

3

pre1.x

normal

#17130 
"alias i" works only on random instruction.

Benjamin Grégoire

enhancement

3

pre1.x

normal

#17133 
seq for phoare do not check the type of the arguments.

Benjamin Grégoire

defect

3

pre1.x

normal

#17134 
is_lossless F(M).f generate a parse error.

PierreYves Strub

defect

3

pre1.x

normal

#17136 
variant of seq to deal with large preconditions


enhancement

3

pre1.x

normal

#17137 
More tactical about goal selections

PierreYves Strub

enhancement

3

pre1.x

normal

#17142 
Anomaly (related to SMT and memories)

Benjamin Grégoire

defect

3

pre1.x

normal

(more results for this group on next page)
