Custom query (532 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (401 - 500 of 532)

1 2 3 4 5 6

Status: closed (48 matches)

Ticket Summary Owner Type Priority Version Severity
#17372 "" and "!" semantic for smt Pierre-Yves Strub enhancement 3 pre-1.x normal
#17373 introduction pattern bug somehow related to SmtMap defect 3 pre-1.x normal
#17375 `include` command for modules / module types Pierre-Yves Strub enhancement 3 pre-1.x normal
#17376 behaviour of module type include in functor types Benjamin Grégoire enhancement 3 pre-1.x normal
#17377 characterization lemmas for <=> and \proper Pierre-Yves Strub enhancement 3 pre-1.x normal
#17385 problem sending goal to SMT (involving inductive datatype and higher order function) Pierre-Yves Strub defect 3 pre-1.x normal
#17386 crush reduces goal whose conclusion is `y1 = y2 <=> x1 = x2` to false goal defect 3 pre-1.x normal
#17387 no error message for match Pierre-Yves Strub defect 3 pre-1.x normal
#17389 inline does not inline under match statement defect 3 pre-1.x normal
#17391 case works with tuple corresponding to glob M, but not with glob M Pierre-Yves Strub defect 3 pre-1.x normal
#17393 Cloning polymorphic datatypes does not allow case analysis defect 3 pre-1.x normal
#17394 anomaly on some smt calls Pierre-Yves Strub defect 3 pre-1.x normal
#17397 odd scoping when overwriting operator in theory cloning enhancement 3 pre-1.x normal
#17398 problem with new eco facility Pierre-Yves Strub defect 3 pre-1.x normal
#17400 eco problem: .ec file that uses unchanged .ec file is rechecked even though nothing changed and eco files stable Pierre-Yves Strub defect 3 pre-1.x normal
#17401 Generalizations may perform freeness checks in the wrong context defect 3 pre-1.x normal
#17403 Support for `move/(_ _ x): H=> H` Pierre-Yves Strub enhancement 3 pre-1.x normal
#15702 Error with multiple require if they contain the same game Pierre-Yves Strub defect 4 pre-1.x critical
#15891 Instantiating axioms and sub-theories when cloning theories Pierre-Yves Strub enhancement 4 pre-1.x
#15893 Call in adversary call is not working properly Benjamin Grégoire defect 4 pre-1.x
#15950 tactics for fundamental lemma Benjamin Grégoire enhancement 4 pre-1.x major
#16692 bug in apply. Pierre-Yves Strub defect 4 pre-1.x normal
#17012 pr_false is badly implemented (unsoundness) Pierre-Yves Strub defect 4 pre-1.x critical
#17035 Alt-Ergo succeeds on false obligations in weird circumstances Pierre-Yves Strub defect 4 pre-1.x critical
#17082 SMT tactic should be interruptable. Pierre-Yves Strub enhancement 4 pre-1.x normal
#17087 [conseq*] should be the default behaviour of [conseq] Pierre-Yves Strub enhancement 4 pre-1.x normal
#17089 anomaly in [sim] Benjamin Grégoire defect 4 pre-1.x normal
#17120 [rnd] allows to prove false Pierre-Yves Strub defect 4 pre-1.x normal
#17127 Bug in typing of instruction x.[y] = e; Pierre-Yves Strub defect 4 pre-1.x major
#17148 Operators should be subject to section restrictions Pierre-Yves Strub defect 4 pre-1.x major
#17155 Fix stdlib w.r.t. why3 import Pierre-Yves Strub defect 4 pre-1.x major
#17162 Bad interaction between abstract theories and local modules Pierre-Yves Strub defect 4 pre-1.x normal
#17329 EasyCrypt output (goals order e.g.) is not stable Pierre-Yves Strub defect 4 pre-1.x normal
#17339 `anomaly: EcLowGoal.InvalidProofTerm.` on `/>` Pierre-Yves Strub defect 4 pre-1.x major
#15872 fun stopped working ckunz defect 5 pre-1.x critical
#16306 Bug in cloning ? Benjamin Grégoire defect 5 pre-1.x major
#16787 new conseq issues Benjamin Grégoire defect 5 pre-1.x blocker
#17013 EasyCrypt toolchain does not compile anymore on OSX Pierre-Yves Strub defect 5 pre-1.x major
#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 pre-1.x critical
#17068 Possible bug in the union-find algorithm Pierre-Yves Strub defect 5 pre-1.x critical
#17109 Hoare adversary rule introducess references to non-existent memories in postconditions Benjamin Grégoire defect 5 pre-1.x normal
#17112 `unknown symbol Top.o` when importing a theory including objects referring to `Top.o` Pierre-Yves Strub defect 5 pre-1.x major
#17114 Unsoundness of module system Benjamin Grégoire defect 5 pre-1.x blocker
#17132 Unsoundness in definition of "glob M" Pierre-Yves Strub defect 5 pre-1.x blocker
#17270 `done` should close a goal when `false` is a local hyp. Pierre-Yves Strub enhancement 5 pre-1.x normal
#17365 Proof of false using Ring and Reals. Pierre-Yves Strub defect 5 pre-1.x critical
#17379 Proving unreasonable/false lemmas through Alt-Ergo defect 5 pre-1.x critical
#17380 Internal "seq" of pHL tactics is unsound Benjamin Grégoire defect 5 pre-1.x critical

Status: new (52 matches)

Ticket Summary Owner Type Priority Version Severity
#16912 Lifting the "collection update" statements to tuples enhancement 1 pre-1.x normal
#17036 Instantiating abstract modules: warnings and interactive justification enhancement 1 pre-1.x normal
#17045 Rewriting procedures in probability expressions directly from an equivalence enhancement 1 pre-1.x normal
#17183 Variant of `sim` that works modulo inlining. enhancement 1 pre-1.x normal
#17297 Allow the optional use of undeclared variables in procedures enhancement 1 pre-1.x normal
#17307 Coq style Locate enhancement 1 pre-1.x minor
#17353 `&&` could disappear from internal code, and be replaced by distinct splitting lemmas for `/\` enhancement 1 pre-1.x normal
#17356 Two-sided `rcondx` enhancement 1 pre-1.x normal
#17037 Poor error message for module restriction example Pierre-Yves Strub enhancement 2 pre-1.x minor
#17088 `case !a` should reduce to proving `a` Pierre-Yves Strub enhancement 2 pre-1.x normal
#17090 Selecting procedure(s) to [inline] by position enhancement 2 pre-1.x normal
#16103 scoping issue with theories enhancement 3 pre-1.x
#16987 Move facts from precondition to context enhancement 3 pre-1.x normal
#17002 Better section && cloning support Pierre-Yves Strub task 3 pre-1.x major
#17022 Pattern-matching on variables in judgments and probability expressions enhancement 3 pre-1.x normal
#17085 Generic Notations Pierre-Yves Strub enhancement 3 pre-1.x normal
#17086 Generalize [rewrite Pr] enhancement 3 pre-1.x normal
#17105 [transitivity] for phoare and hoare enhancement 3 pre-1.x normal
#17113 Decide what to do on rewrite with defined head symbols enhancement 3 pre-1.x normal
#17140 Pattern matching should make use of simplification rules. enhancement 3 pre-1.x normal
#17149 Expand glob A for concrete module enhancement 3 pre-1.x normal
#17156 New vernacular command: `print axiom` enhancement 3 pre-1.x normal
#17164 behavior of -check-all enhancement 3 pre-1.x normal
#17169 Anonymous functor arguments: passing procedures to functors directly enhancement 3 pre-1.x normal
#17175 Direct intro on negative goals enhancement 3 pre-1.x normal
#17192 Problem with `glob` and type inference defect 3 pre-1.x normal
#17197 Asserts in equivalence proofs enhancement 3 pre-1.x normal
#17202 Add seq* tactic enhancement 3 pre-1.x major
#17210 Pattern-matching for pairs in operator arguments enhancement 3 pre-1.x normal
#17215 Issues with module typing when functor parameters are themselves functors defect 3 pre-1.x normal
#17217 need better error message when attempting to apply lemma to goal that isn't a judgment enhancement 3 pre-1.x normal
#17218 proposal for expressing goal of two-sided PRHL rnd tactic using isomorphism of bijections predicate enhancement 3 pre-1.x normal
#17225 Explore reproducible smt calls enhancement 3 pre-1.x normal
#17239 Mutual inductive types. enhancement 3 pre-1.x normal
#17245 Formula manipulation commands (for `conseq` and `seq`) enhancement 3 pre-1.x normal
#17246 `rewrite`, apply, ... in contracts defect 3 pre-1.x normal
#17251 print Self enhancement 3 pre-1.x normal
#17267 `auto` with `call` enhancement 3 pre-1.x normal
#17279 Improve `invalid goal shape` error messages for variants of `byequiv` enhancement 3 pre-1.x normal
#17281 Several problems with `apply` in program logics enhancement 3 pre-1.x normal
#17282 call should not work task 3 phl normal
#17283 pattern matching complexity problem defect 3 pre-1.x normal
#17285 Transitivity on procedures should support inferring contracts from `equiv` lemmas. enhancement 3 pre-1.x normal
#17286 pRHL `apply` should have a framing variant enhancement 3 pre-1.x normal
#17287 Program transformation tactics should not `anomaly` without a side in pRHL defect 3 pre-1.x normal
#17288 EasyCrypt crashes when printing required abstract theory IterProc defect 3 pre-1.x normal
#17295 local ops enhancement 3 pre-1.x normal
#17301 Applicative view for `if then else` enhancement 3 pre-1.x normal
#17305 proc* in eager case needlessly assigns result of procedures returning unit to variables enhancement 3 pre-1.x normal
#17311 `smt (@Self)` enhancement 3 pre-1.x normal
#17316 [smt (@Theory)] should force the use of axioms marked as `nosmt` defect 3 pre-1.x normal
#17317 `search` should work somewhat better with abbreviations enhancement 3 pre-1.x normal
(more results for this group on next page)
1 2 3 4 5 6
Note: See TracQuery for help on using queries.