]> matita.cs.unibo.it Git - helm.git/blob - benchmarks/bugs
forced associativity in if construct
[helm.git] / benchmarks / bugs
1 ==== CoFix
2 cic:/Lyon/COINDUCTIVES/STREAMS/Examples/mapS2.con \e[0;31mFAIL\e[0m
3 cic:/Marseille/CCS/Trans_Sys/refl_strong_eq.con \e[0;31mFAIL\e[0m
4 cic:/Marseille/CCS/Trans_Sys/sym_strong_eq.con \e[0;31mFAIL\e[0m
5 cic:/Marseille/CCS/Trans_Sys/trans_strong_eq.con \e[0;31mFAIL\e[0m
6 cic:/Marseille/CCS/Trans_Sys/refl_weak_eq.con \e[0;31mFAIL\e[0m
7 cic:/Marseille/CCS/Trans_Sys/strong_weak.con \e[0;31mFAIL\e[0m
8 cic:/Marseille/CCS/Trans_Sys/sym_weak_eq.con \e[0;31mFAIL\e[0m
9 cic:/Marseille/CCS/Trans_Sys/weak_eq1_weak_eq.con \e[0;31mFAIL\e[0m
10
11 ==== Non positive occurrence
12 cic:/Suresnes/MiniC/MiniC/State/n_type.ind \e[0;31mFAIL\e[0m
13 cic:/Suresnes/MiniC/MiniC/CAbstractSyntax/c_type.ind \e[0;31mFAIL\e[0m
14 cic:/Suresnes/MiniC/MiniC/BasicTypes/c_value.ind \e[0;31mFAIL\e[0m
15 cic:/Lyon/FIRING-SQUAD/bib/div2.ind \e[0;31mFAIL\e[0m
16 cic:/Lyon/GRAPHS-BASICS/Trees/Tree.ind \e[0;31mFAIL\e[0m
17 cic:/Lyon/GRAPHS-BASICS/Graphs/Graph.ind \e[0;31mFAIL\e[0m
18 cic:/Lyon/GRAPHS-BASICS/Digraphs/Digraph.ind \e[0;31mFAIL\e[0m
19 cic:/Lyon/GRAPHS-BASICS/Connected/Connected.ind \e[0;31mFAIL\e[0m
20 cic:/Lyon/GRAPHS-BASICS/Acyclic/Acyclic.ind \e[0;31mFAIL\e[0m
21 cic:/Rocq/TreeAutomata/pl_path/pl_path_recon.ind \e[0;31mFAIL\e[0m
22 cic:/Rocq/COMPILER/Mini_ML/compilation.ind \e[0;31mFAIL\e[0m
23 cic:/Rocq/COMPILER/Mini_ML/compilation_id.ind \e[0;31mFAIL\e[0m
24 cic:/Rocq/COC/Infer/expln.ind \e[0;31mFAIL\e[0m
25 cic:/Rocq/COC/Machine/transition.ind \e[0;31mFAIL\e[0m
26
27
28 ==== Convertibilita
29 cic:/Rocq/TreeAutomata/defs/term_list_term_ind.con \e[0;31mFAIL\e[0m
30 cic:/Rocq/TreeAutomata/defs/term_list_term_rec.con \e[0;31mFAIL\e[0m
31 cic:/Rocq/TreeAutomata/defs/term_term_list_ind.con \e[0;31mFAIL\e[0m
32 cic:/Rocq/TreeAutomata/defs/term_term_list_rec.con \e[0;31mFAIL\e[0m
33 cic:/Rocq/TreeAutomata/semantics/mlrec_ind.con \e[0;31mFAIL\e[0m
34 cic:/Rocq/TreeAutomata/semantics/mreconnaissance_ind.con \e[0;31mFAIL\e[0m
35 cic:/Rocq/TreeAutomata/semantics/mstrec_ind.con \e[0;31mFAIL\e[0m
36 cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/Fairness.con \e[0;31mFAIL\e[0m
37 cic:/Rocq/TreeAutomata/non_coacc_kill/mlrec_co_ind.con \e[0;31mFAIL\e[0m
38 cic:/Rocq/TreeAutomata/non_coacc_kill/mreconnaissance_co_ind.con \e[0;31mFAIL\e[0m
39 cic:/Rocq/TreeAutomata/non_coacc_kill/mstrec_co_ind.con \e[0;31mFAIL\e[0m
40 cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/Equity.con \e[0;31mFAIL\e[0m
41 cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/InTrace.con \e[0;31mFAIL\e[0m
42 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state1.con \e[0;31mFAIL\e[0m
43 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state2.con \e[0;31mFAIL\e[0m
44 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state3.con \e[0;31mFAIL\e[0m
45 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state5.con \e[0;31mFAIL\e[0m
46 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state4.con \e[0;31mFAIL\e[0m
47 cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique3.con \e[0;31mFAIL\e[0m
48 cic:/Suresnes/BDD/canonicite/Boolean_functions/Assign_k_finite.con \e[0;31mFAIL\e[0m
49 cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique2.con \e[0;31mFAIL\e[0m
50 cic:/Suresnes/BDD/canonicite/Vars/Var_k_finite.con \e[0;31mFAIL\e[0m
51 cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique1.con \e[0;31mFAIL\e[0m
52 cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique45.con \e[0;31mFAIL\e[0m
53 cic:/Rocq/HIGMAN/Higman/higman.con \e[0;31mFAIL\e[0m
54
55
56 === Unknown constant
57 cic:/Sophia-Antipolis/Huffman/Permutation/permutation_map_ex.con \e[0;31mFAIL\e[0m
58
59 === Caso non implementato
60 cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/ACK.con \e[0;31mFAIL\e[0m
61 cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/ACKING.con \e[0;31mFAIL\e[0m
62 cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/OUT.con \e[0;31mFAIL\e[0m
63 cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/REPEAT.con \e[0;31mFAIL\e[0m
64 cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/SEND.con \e[0;31mFAIL\e[0m
65 cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/SENDING.con \e[0;31mFAIL\e[0m
66 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/ACK.con \e[0;31mFAIL\e[0m
67 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/ACKING.con \e[0;31mFAIL\e[0m
68 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/OUT.con \e[0;31mFAIL\e[0m
69 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/REPEAT.con \e[0;31mFAIL\e[0m
70 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/SEND.con \e[0;31mFAIL\e[0m
71 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/SENDING.con \e[0;31mFAIL\e[0m
72 cic:/Rocq/MUTUAL-EXCLUSION/binary/version2/Correctness/correct.con \e[0;31mFAIL\e[0m
73 cic:/Rocq/MUTUAL-EXCLUSION/binary/version1/Correctness/correct.con \e[0;31mFAIL\e[0m
74
75 === Wrong branch type (Nel primo caso: esportato male (argomenti permutati
76     nel tipo di Disc!)
77 cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/IsClear.con \e[0;31mFAIL\e[0m
78 cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/OneDel.con \e[0;31mFAIL\e[0m
79 cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/Rtalks.con \e[0;31mFAIL\e[0m
80
81 === check_is_really_smaller su un const o mutind?
82 cic:/Nijmegen/QArith/positive_fraction_encoding/encoding_algorithm.con \e[0;31mFAIL\e[0m
83 cic:/Nijmegen/QArith/positive_fraction_encoding/encoding_algorithm_ind.con \e[0;31mFAIL\e[0m