#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

#17132 
Unsoundness in definition of "glob M"

PierreYves Strub

defect

5

pre1.x

blocker

#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

#17135 
anomaly when intro pattern has wrong form

PierreYves Strub

defect

3

pre1.x

minor

#17138 
"easycrypt checkall" does not load "Logic"

PierreYves Strub

defect

3

pre1.x

minor

#17142 
Anomaly (related to SMT and memories)

Benjamin Grégoire

defect

3

pre1.x

normal

#17143 
Anomaly (free type variables in conseq)

PierreYves Strub

defect

3

pre1.x

normal

#17144 
Module type checking: Unclear error message and probably bug

PierreYves Strub

defect

3

pre1.x

normal

#17145 
"choice" reorders its arguments

PierreYves Strub

defect

3

pre1.x

normal

#17146 
Bad error message in combination choice/modules/section

PierreYves Strub

defect

3

pre1.x

normal

#17147 
Parse error in (some) expressions involving memories

PierreYves Strub

defect

3

pre1.x

normal

#17148 
Operators should be subject to section restrictions

PierreYves Strub

defect

4

pre1.x

major

#17153 
seq does not check type of its arguments

PierreYves Strub

defect

3

pre1.x

normal

#17154 
anomaly: EcPV.MemoryClash


defect

3

pre1.x

normal

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

PierreYves Strub

defect

4

pre1.x

major

#17162 
Bad interaction between abstract theories and local modules

PierreYves Strub

defect

4

pre1.x

normal

#17168 
Unsoundness: combination of sections, modules, and choiceoperators

PierreYves Strub

defect

3

pre1.x

critical

#17172 
Looping on `rewrite !/op`

PierreYves Strub

defect

3

pre1.x

normal

#17174 
Return of the memory explosion


defect

3

pre1.x

normal

#17177 
View application fails non gracely when it cannot instanciate all type variables.

PierreYves Strub

defect

3

pre1.x

minor

#17178 
Generalizing over an empty list should generate a sane name

PierreYves Strub

defect

3

pre1.x

normal

#17180 
anomaly: File "src/ecCoreFol.ml", line 1207, characters 1925: Assertion failed

PierreYves Strub

defect

3

pre1.x

normal

#17184 
parse error involving parameterized module

PierreYves Strub

defect

3

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

#17188 
Error with smt : lazy


defect

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

#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

#17203 
Rewrite strangely failling

PierreYves Strub

defect

3

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

#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

#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

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

PierreYves Strub

defect

3

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

#17236 
error with rewriting occurrence of 1 when only one matching occurrence


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

#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

#17254 
print produces misleading results on partially applied functors


defect

3

pre1.x

normal

#17260 
pragma +option should fail gracefully.

PierreYves Strub

defect

3

pre1.x

normal

#17272 
Wrong name


defect

3

pre1.x

trivial

#17273 
`alias` failures look like uncaught exceptions


defect

3

pre1.x

minor

#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

#17278 
[eta] reduction is not full on multiary functions

github <noreply@…>

defect

3

pre1.x

normal

#17289 
Missing dependencies in OPAM package


defect

3

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

#17292 
anomaly on application of a `<=>` lemma to a `=` goal


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

#17296 
Some program tactics (`rnd`) generate invalid formulas when Distr is not loaded


defect

3

pre1.x

normal

#17300 
Module type checks have wrong variance when dealing with some functor configurations

Benjamin Grégoire

defect

3

pre1.x

normal

#17302 
fel can generate subgoal with undefined memory

Benjamin Grégoire

defect

3

pre1.x

normal

#17303 
more fel peculiarities

Benjamin Grégoire

defect

3

pre1.x

normal

#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

#17315 
[print] on notations is not very useful


defect

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

#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

#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

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

PierreYves Strub

defect

4

pre1.x

major

#17348 
Intropattern `>` might transform a provable goal to a nonprovable one


defect

3

pre1.x

normal

#17350 
witness not in apRHL


defect

3

pre1.x

normal

#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

#17366 
crush losing some context on intermediate substitutions


defect

3

pre1.x

normal

#17369 
imprecise pretty printing with functor application


defect

2

pre1.x

normal

#17373 
introduction pattern bug somehow related to SmtMap


defect

3

pre1.x

normal

#17379 
Proving unreasonable/false lemmas through AltErgo


defect

5

pre1.x

critical

#17380 
Internal "seq" of pHL tactics is unsound

Benjamin Grégoire

defect

5

pre1.x

critical

#17381 
Possible bug: no matching operator even when available


defect

2

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

#17386 
crush reduces goal whose conclusion is `y1 = y2 <=> x1 = x2` to false goal


defect

3

pre1.x

normal

(more results for this group on next page)
