#17185 
Anomalies should give rise to a "This is a bug, please report."type message.

PierreYves Strub

enhancement

1

pre1.x

trivial

#17187 
anomaly when invalid memory is referenced  should be proper error message

PierreYves Strub

defect

3

pre1.x

normal

#17189 
Syntax for referring to *local* variables by their long name

PierreYves Strub

enhancement

3

pre1.x

normal

#17190 
progress and progress => //. should be equivalent...

PierreYves Strub

defect

3

pre1.x

normal

#17191 
Assert failure

PierreYves Strub

defect

3

pre1.x

normal

#17193 
Obscure failure on lazy smt with higherorder stuff and booleans

PierreYves Strub

defect

3

pre1.x

normal

#17196 
Vernacular command for dumping env. as a Why3 task.

PierreYves Strub

enhancement

3

pre1.x

normal

#17198 
Spurious failure of rewrite

PierreYves Strub

defect

3

pre1.x

normal

#17200 
Parse error in required theories are incorrectly located.

PierreYves Strub

defect

3

pre1.x

minor

#17201 
`xy` and `x + y` should be convertible

PierreYves Strub

enhancement

3

pre1.x

normal

#17203 
Rewrite strangely failling

PierreYves Strub

defect

3

pre1.x

normal

#17204 
Syntax for ignoring the return value of a procedure call

PierreYves Strub

enhancement

1

pre1.x

normal

#17205 
New syntax for assignments should be available in immediate definitions

PierreYves Strub

defect

3

pre1.x

normal

#17206 
Missing parens in the pretty printer

PierreYves Strub

defect

3

pre1.x

normal

#17208 
`rewrite ... in ...`

PierreYves Strub

defect

3

pre1.x

normal

#17211 
split causes anomaly when given equality between constructors

PierreYves Strub

defect

3

pre1.x

normal

#17212 
Circular [require] dependencies should be caught instead of blowing up computers

PierreYves Strub

defect

3

pre1.x

normal

#17214 
Wrong printed for memory

PierreYves Strub

defect

3

pre1.x

normal

#17219 
operators don't print the way they are declared

PierreYves Strub

defect

3

pre1.x

normal

#17220 
Shorthand "by" syntax should be supported for "realize"

PierreYves Strub

enhancement

3

pre1.x

normal

#17221 
parsing change allowing lemma ... by tactics

PierreYves Strub

enhancement

3

pre1.x

normal

#17223 
use of ' and ` in operator names causes anomaly rather than error message

PierreYves Strub

defect

3

pre1.x

normal

#17224 
type declarations with bad type variables yield anomalies rather than error messages

PierreYves Strub

defect

3

pre1.x

normal

#17226 
some weirdness with operators of form :+

PierreYves Strub

defect

3

pre1.x

normal

#17227 
Procedures with unit return type should be allowed to return `tt'

PierreYves Strub

enhancement

2

pre1.x

minor

#17228 
pretty printer uses bad syntax for type constructors

PierreYves Strub

defect

3

pre1.x

normal

#17229 
pretty printer errors with inductive datatypes

PierreYves Strub

defect

3

pre1.x

normal

#17230 
unhelpful error message when there are two matching operators with needed type

PierreYves Strub

enhancement

3

pre1.x

normal

#17231 
check for datatype being inhabited isn't complete, but error message suggests it is

PierreYves Strub

enhancement

3

pre1.x

normal

#17233 
pretty printing issues with _?_:_ and modules

PierreYves Strub

defect

3

pre1.x

normal

#17234 
Allow omission of a procedure's return type when it can be inferred

PierreYves Strub

enhancement

3

pre1.x

normal

#17235 
rewrite ... in ... should allow rewriting in uident not just lident

PierreYves Strub

defect

3

pre1.x

normal

#17237 
failure of rewrite ... in ...

PierreYves Strub

defect

3

pre1.x

normal

#17238 
anomaly with autorevert intro pattern

PierreYves Strub

defect

3

pre1.x

normal

#17241 
`clone import` not working when realizing axioms.

PierreYves Strub

defect

3

pre1.x

normal

#17242 
`print` should display `nosmt` info

PierreYves Strub

enhancement

3

pre1.x

normal

#17243 
Internal error (anomaly) on proof script

PierreYves Strub

defect

3

pre1.x

normal

#17244 
Imprecise "uninitialized local variables" warning

PierreYves Strub

defect

3

pre1.x

normal

#17247 
Interactive proof realisation for `instance`

PierreYves Strub

enhancement

3

pre1.x

normal

#17248 
More precise error messages when noninteractive realization fails

PierreYves Strub

enhancement

3

pre1.x

normal

#17249 
`AlgTactic` && `Ring` should agree on their axioms.

PierreYves Strub

enhancement

2

pre1.x

normal

#17258 
Intro pattern for hypothesis duplication

PierreYves Strub

enhancement

3

pre1.x

normal

#17260 
pragma +option should fail gracefully.

PierreYves Strub

defect

3

pre1.x

normal

#17269 
Add notations for >/>=

PierreYves Strub

enhancement

3

pre1.x

normal

#17270 
`done` should close a goal when `false` is a local hyp.

PierreYves Strub

enhancement

5

pre1.x

normal

#17274 
Collision in names, local variables unreachable

PierreYves Strub

defect

3

pre1.x

blocker

#17275 
[congr] should apply to iff

PierreYves Strub

defect

3

pre1.x

normal

#17276 
the pretty printer is getting the relative precedences of unary  and %% wrong

PierreYves Strub

defect

3

pre1.x

normal

#17277 
Higherorder patternmatching with quantifiers

PierreYves Strub

defect

3

pre1.x

normal

#17280 
Parseonly abbreviations

PierreYves Strub

enhancement

3

pre1.x

normal

#17284 
Support for `={<expr>}` in equiv contracts

PierreYves Strub

enhancement

3

pre1.x

normal

#17291 
`move: x` should keep the body of `x` if any.

PierreYves Strub

defect

3

pre1.x

normal

#17293 
Looping behaviour in reduction/simplification. Probably related to reals.

PierreYves Strub

defect

3

pre1.x

normal

#17294 
`Self` (and `Top`) should be allowed in module restrictions

PierreYves Strub

defect

1

pre1.x

minor

#17304 
Regression on anonymous procedure arguments support

PierreYves Strub

defect

3

pre1.x

normal

#17306 
Operator folding and unfolding not checking type parameters

PierreYves Strub

defect

3

pre1.x

normal

#17308 
`rewrite !(A,B)` loops when `B` is not known about

PierreYves Strub

defect

3

pre1.x

normal

#17310 
Toplevel command to print various databases (exact, rewrite, ...)

PierreYves Strub

defect

2

pre1.x

minor

#17312 
cloning can create illformed definitions

PierreYves Strub

defect

3

pre1.x

normal

#17313 
module types with multiple occurrences of same procedure should not be accepted

PierreYves Strub

defect

3

pre1.x

normal

#17314 
Syntax variants of multiple argument module types don't match ones for parameterized modules

PierreYves Strub

enhancement

3

pre1.x

normal

#17318 
clonetime regexp substitution should apply in the specified order

PierreYves Strub

defect

3

pre1.x

normal

#17320 
anomaly when cloning theory with inductive predicate

PierreYves Strub

defect

3

pre1.x

normal

#17321 
`case @[ambient]` needs its syntax unified with that of ambient `case`

PierreYves Strub

enhancement

3

pre1.x

trivial

#17323 
> ip anomaly

PierreYves Strub

defect

3

pre1.x

normal

#17324 
> ip expands predicates in conclusion

PierreYves Strub

defect

3

pre1.x

normal

#17326 
`+` intropattern may reorder assumptions

PierreYves Strub

defect

3

pre1.x

normal

#17327 
Variants of `<*>` with preference

PierreYves Strub

enhancement

3

pre1.x

normal

#17329 
EasyCrypt output (goals order e.g.) is not stable

PierreYves Strub

defect

4

pre1.x

normal

#17330 
anomaly on `apply/contra`

PierreYves Strub

defect

3

pre1.x

normal

#17331 
Tactic arguments for the `exists` tactic should not be commaseparated

PierreYves Strub

enhancement

3

pre1.x

normal

#17332 
Better localisation when a pattern cannot be infered

PierreYves Strub

enhancement

3

pre1.x

normal

#17333 
We need a `pragma` to stop EasyCrypt from reducing `b => false` into `!b`.

PierreYves Strub

enhancement

3

pre1.x

normal

#17336 
`inline` procedure selection by code position

PierreYves Strub

enhancement

3

pre1.x

normal

#17338 
misspelled pragmas are not reported

PierreYves Strub

enhancement

3

pre1.x

normal

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

PierreYves Strub

defect

4

pre1.x

major

#17354 
In cloning, `rename` should not be allowed to create unreachable/unparsable symbols

PierreYves Strub

defect

3

pre1.x

normal

#17355 
Prettyprinter sometimes forget to use the abbreviation

PierreYves Strub

defect

3

pre1.x

normal

#17361 
scoping problem with theory renaming

PierreYves Strub

defect

3

pre1.x

normal

#17365 
Proof of false using Ring and Reals.

PierreYves Strub

defect

5

pre1.x

critical

#17371 
new option for smt

PierreYves Strub

enhancement

3

pre1.x

normal

#17372 
"" and "!" semantic for smt

PierreYves Strub

enhancement

3

pre1.x

normal

#17375 
`include` command for modules / module types

PierreYves Strub

enhancement

3

pre1.x

normal

#17377 
characterization lemmas for <=> and \proper

PierreYves Strub

enhancement

3

pre1.x

normal

#17385 
problem sending goal to SMT (involving inductive datatype and higher order function)

PierreYves Strub

defect

3

pre1.x

normal

#17387 
no error message for match

PierreYves Strub

defect

3

pre1.x

normal

#17391 
case works with tuple corresponding to glob M, but not with glob M

PierreYves Strub

defect

3

pre1.x

normal

#17394 
anomaly on some smt calls

PierreYves Strub

defect

3

pre1.x

normal

#17398 
problem with new eco facility

PierreYves Strub

defect

3

pre1.x

normal

#17400 
eco problem: .ec file that uses unchanged .ec file is rechecked even though nothing changed and eco files stable

PierreYves Strub

defect

3

pre1.x

normal

#17403 
Support for `move/(_ _ x): H=> H`

PierreYves Strub

enhancement

3

pre1.x

normal

#15918 
Tactic for proving an equiv/hoare/bd_hoare goal when the precondition is contradictory

Santiago ZanellaBéguelin

enhancement

3

pre1.x


#15920 
[conseq (_ : pre => _)] tactic for bd_hoare doesn't work

Santiago ZanellaBéguelin

defect

3

pre1.x


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

Santiago ZanellaBéguelin

defect

3

pre1.x

normal

#15106 
Consider probability quantities as realvalued expressions


enhancement

2

pre1.x

normal

#15786 
Swap with call to the adversary


defect

3

pre1.x


#16058 
Syntax f.x in equiv precondition for fonction argument


enhancement

3

pre1.x

blocker

#16104 
naming issues


enhancement

3

pre1.x

blocker

#16229 
Substitution issue when quantified module variables have the same name as an existing module


defect

3

pre1.x

blocker

#16253 
Nonlocal modules and abstract restrictions.


defect

3

pre1.x


(more results for this group on next page)
