Custom query (541 matches)

Filters
 
or
 
  
 
Columns

Show under each result:

Results (1 - 100 of 541)

1 2 3 4 5 6 →

Status: accepted (12 matches)

Ticket Summary Owner Type Priority Component Version
#17378 Proof of false using smt and Eprover. Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17141 Wrong module type annotations accepted Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17024 Pattern matching should try to infer memory and module parameters Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17034 Generalizing loop fusion Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17040 Syntactic sugar for nested if-then-else statements. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17042 Pattern matching in non-normal form. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17070 better error message when difference between goal and lemma is tiny Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17195 Swap with 2 args move as far down as possible Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17250 off-by-one error in swap Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17309 `rewrite /F` when F is a fixpoint should simplify selected occurence for head-iota reduction. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17392 problems with glob and delta and matching Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16113 <top> in printer Pierre-Yves Strub defect 2 EasyCrypt pre-1.x

Status: assigned (28 matches)
Ticket Summary Owner Type Priority Component Version
#17181 slow rewriting for large expressions Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17194 anomaly: EcHiGoal.LowApply.NoInstance (in byequiv) Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17207 Applicative view Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17222 local clones do not disappear from the environment on section end Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17240 Syntactic sugar for proc. that reduces to a call to an external proc. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17255 Missing unification in `clone...with...` Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17256 apply/rewrite should work modulo zeta-reduction. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17261 `rewrite -/(f _)` should not match its own unfoldings. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17262 Add the possibility to add rewrite hints to rewrite hint databases. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17263 Multiple incompleteness in `apply` Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17265 `goal` vernacular command Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17268 Add a tactical that fails when no progress is done. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17269 Add notations for >/>= Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17270 `done` should close a goal when `false` is a local hyp. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17271 Pattern matching should solve problems of the form `?f tj...tn ~ f t1 ... tn` Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17308 `rewrite !(A,B)` loops when `B` is not known about Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17319 Anomaly triggered by `smt` defect 3 EasyCrypt pre-1.x
#17334 this message need more information: cannot infer all placeholders Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17335 the formula contains free type variables Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17117 Warning when restrictions over an adversary are empty Benjamin Grégoire enhancement 2 EasyCrypt pre-1.x
#17160 Call SMT in parallels. Pierre-Yves Strub enhancement 2 Internals pre-1.x
#17253 EasyCrypt should fail gracefully when applying a tactic on a solved goal. Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17264 Add the possibility to clear lemmas when closing a theory. Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17310 Top-level command to print various databases (exact, rewrite, ...) Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17347 Search with notations is broken. Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17343 (Optional) warning for old syntax Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17345 Bad printing Pierre-Yves Strub defect 1 EasyCrypt pre-1.x
#17364 Internals: use Batteries maps instead of Why3 ones. Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x

Status: closed (60 matches)
Ticket Summary Owner Type Priority Component Version
#15872 fun stopped working ckunz defect 5 EasyCrypt pre-1.x
#16306 Bug in cloning ? Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#16787 new conseq issues Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17013 EasyCrypt toolchain does not compile anymore on OSX Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17027 [Unsoundness] The HL and pHL tactics for abstract function calls do not quantify over variables that may be modified in the postcondition Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17068 Possible bug in the union-find algorithm Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17079 Make the test-suite pass. Pierre-Yves Strub defect 5 Libraries pre-1.x
#17109 Hoare adversary rule introducess references to non-existent memories in postconditions Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17112 `unknown symbol Top.o` when importing a theory including objects referring to `Top.o` Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17114 Unsoundness of module system Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17132 Unsoundness in definition of "glob M" Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17365 Proof of false using Ring and Reals. Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17379 Proving unreasonable/false lemmas through Alt-Ergo defect 5 EasyCrypt pre-1.x
#17380 Internal "seq" of pHL tactics is unsound Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#15702 Error with multiple require if they contain the same game Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#15891 Instantiating axioms and sub-theories when cloning theories Pierre-Yves Strub enhancement 4 EasyCrypt pre-1.x
#15893 Call in adversary call is not working properly Benjamin Grégoire defect 4 EasyCrypt pre-1.x
#15950 tactics for fundamental lemma Benjamin Grégoire enhancement 4 EasyCrypt pre-1.x
#16692 bug in apply. Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17012 pr_false is badly implemented (unsoundness) Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17035 Alt-Ergo succeeds on false obligations in weird circumstances Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17080 `t_generalize_hyps` does not work when given a non-singleton list. Pierre-Yves Strub defect 4 Internals pre-1.x
#17087 [conseq*] should be the default behaviour of [conseq] Pierre-Yves Strub enhancement 4 EasyCrypt pre-1.x
#17089 anomaly in [sim] Benjamin Grégoire defect 4 EasyCrypt pre-1.x
#17098 Add a search facility Pierre-Yves Strub enhancement 4 Documentation pre-1.x
#17120 [rnd] allows to prove false Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17127 Bug in typing of instruction x.[y] = e; Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17148 Operators should be subject to section restrictions Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17155 Fix stdlib w.r.t. why3 import Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17162 Bad interaction between abstract theories and local modules Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17329 EasyCrypt output (goals order e.g.) is not stable Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17339 `anomaly: EcLowGoal.InvalidProofTerm.` on `/>` Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#15502 "Ident <top>_[...] is not yet declared" when cloning a theory with operators Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15506 Issues when cloning theories Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15520 request for more loop manipulation tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15647 Can't extract easily function from tuple Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15651 lambda in operator doesn't work Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15676 Zeta tactics takes too much time to end(infinite loop ?) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15715 Can't access a variable from a functor in probability formula Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15716 Problem with introduction of Module in Proof Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15737 Type-soundness issue when implementing module signatures Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15738 Typing functor applications inside modules Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15742 Strange error raised during a call to trivial Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15744 require import causes name collisions in sub theories Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15762 Tactic to transform a tuple equality into a conjonction Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15764 Result not introduce after call in hoare logic Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15768 Inlining with functor and cloning doesn't work Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15769 ProofGeneral issue with new EasyCrypt: undo step at EOF give Emacs type error Pierre-Yves Strub defect 3 ProofGeneral pre-1.x
#15779 Inference during apply Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15781 Bug into env insertion of a specific axiom Pr[] Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15786 Swap with call to the adversary defect 3 EasyCrypt pre-1.x
#15791 import doesn't import function from module Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15794 Operator not found Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15808 Declaring/defining mixfix operators, using them when not in scope Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15809 Parsing/Printing scope for operator overloading "(x op y)%Scope" Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15813 call tactic signals an "unknown symbol" error Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15814 call tactic accepts variable defined in left game ({1}) defined for right game Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15827 memory restriction for adversary does not take inner modules into account Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15841 No explicit binding in equiv creates problems Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15842 Bug in lambda translation Benjamin Grégoire defect 3 EasyCrypt pre-1.x
(more results for this group on next page)
1 2 3 4 5 6 →
Note: See TracQuery for help on using queries.