Allocation familiales proof diff

gistfile1.txt

[RESULT] [InterfaceAllocationsFamiliales.i_montant_versé] This variable never returns an empty error
[RESULT] [InterfaceAllocationsFamiliales.i_montant_versé] No two exceptions to ever overlap for this variable
[RESULT] [InterfaceAllocationsFamiliales.allocations_familiales.avait_enfant_à_charge_avant_1er_janvier_2012] No two exceptions to ever overlap for this variable
[RESULT] [InterfaceAllocationsFamiliales.allocations_familiales.enfants_à_charge] No two exceptions to ever overlap for this variable
[RESULT] [InterfaceAllocationsFamiliales.allocations_familiales.date_courante] No two exceptions to ever overlap for this variable
[RESULT] [InterfaceAllocationsFamiliales.allocations_familiales.résidence] No two exceptions to ever overlap for this variable
[RESULT] [InterfaceAllocationsFamiliales.allocations_familiales.ressources_ménage] No two exceptions to ever overlap for this variable
[RESULT] [InterfaceAllocationsFamiliales.allocations_familiales.personne_charge_effective_permanente_remplit_titre_I] No two exceptions to ever overlap for this variable
[RESULT] [InterfaceAllocationsFamiliales.allocations_familiales.personne_charge_effective_permanente_est_parent] No two exceptions to ever overlap for this variable
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[RESULT] [AllocationsFamiliales.montant_versé] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.montant_versé] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.montant_versé_complément_pour_base_et_majoration] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.montant_versé_complément_pour_base_et_majoration] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.montant_base_complément_pour_base_et_majoration] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.montant_base_complément_pour_base_et_majoration] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.montant_versé_majoration] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.montant_versé_majoration] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.montant_versé_base] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.montant_versé_base] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.montant_avec_garde_alternée_majoration] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.montant_avec_garde_alternée_majoration] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.montant_avec_garde_alternée_base] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.montant_avec_garde_alternée_base] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.montant_versé_complément_pour_forfaitaire] This variable never returns an empty error
[ERROR] The translation to Z3 failed:
[Z3 encoding] LRat literals not supported
[RESULT] [AllocationsFamiliales.montant_initial_majoration] This variable never returns an empty error
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[RESULT] [AllocationsFamiliales.montant_initial_base] This variable never returns an empty error
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TRat type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TRat type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[RESULT] [AllocationsFamiliales.montant_versé_forfaitaire_par_enfant] This variable never returns an empty error
[ERROR] [AllocationsFamiliales.montant_versé_forfaitaire_par_enfant] At least two exceptions overlap for this variable:
   --> examples/allocations_familiales/prologue.catala_fr
    | 
128 |   interne montant_versé_forfaitaire_par_enfant contenu argent
    |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    + Prologue
The solver generated the following counterexample to explain the faulty behavior:
--> plafond_II_d521_3 : -0.01 $
--> plafond_I_d521_3 : 0.00 $
--> ressources_ménage : 0.00 $
[RESULT] [AllocationsFamiliales.complément_dégressif] This variable never returns an empty error
[ERROR] The translation to Z3 failed:
[Z3 encoding] LRat literals not supported
[RESULT] [AllocationsFamiliales.droit_ouvert_majoration] This variable never returns an empty error
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[RESULT] [AllocationsFamiliales.droit_ouvert_base] This variable never returns an empty error
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[RESULT] [AllocationsFamiliales.montant_initial_base_premier_enfant] This variable never returns an empty error
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[RESULT] [AllocationsFamiliales.nombre_moyen_enfants] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.nombre_moyen_enfants] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.nombre_total_enfants] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.nombre_total_enfants] No two exceptions to ever overlap for this variable
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[RESULT] [AllocationsFamiliales.droit_ouvert_forfaitaire] This variable never returns an empty error
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[RESULT] [AllocationsFamiliales.droit_ouvert_complément] This variable never returns an empty error
[ERROR] The translation to Z3 failed:
[Z3 encoding] TArray type not supported
[RESULT] [AllocationsFamiliales.plafond_I_d521_3] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.plafond_I_d521_3] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.plafond_II_d521_3] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.plafond_II_d521_3] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.est_enfant_le_plus_âgé] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.est_enfant_le_plus_âgé] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.enfants_à_charge_droit_ouvert_prestation_familiale] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.enfants_à_charge_droit_ouvert_prestation_familiale] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.âge_minimum_alinéa_1_l521_3] This variable never returns an empty error
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[RESULT] [AllocationsFamiliales.enfant_le_plus_âgé.enfants] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.prestations_familiales.résidence] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.prestations_familiales.prestation_courante] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.prestations_familiales.date_courante] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.nombre_enfants_alinéa_2_l521_3] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.nombre_enfants_alinéa_2_l521_3] No two exceptions to ever overlap for this variable
[RESULT] [AllocationsFamiliales.nombre_enfants_l521_1] This variable never returns an empty error
[RESULT] [AllocationsFamiliales.nombre_enfants_l521_1] No two exceptions to ever overlap for this variable
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[RESULT] [PrestationsFamiliales.droit_ouvert] This variable never returns an empty error
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[RESULT] [PrestationsFamiliales.conditions_hors_âge] This variable never returns an empty error
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[RESULT] [PrestationsFamiliales.plafond_l512_3_2] This variable never returns an empty error
[RESULT] [PrestationsFamiliales.plafond_l512_3_2] No two exceptions to ever overlap for this variable
[RESULT] [PrestationsFamiliales.régime_outre_mer_l751_1] This variable never returns an empty error
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[RESULT] [PrestationsFamiliales.smic.résidence] No two exceptions to ever overlap for this variable
[RESULT] [PrestationsFamiliales.smic.date_courante] No two exceptions to ever overlap for this variable
[ERROR] [PrestationsFamiliales.base_mensuelle] This variable might return an empty error:
  --> examples/allocations_familiales/prologue.catala_fr
   | 
74 |   sortie base_mensuelle contenu argent
   |          ^^^^^^^^^^^^^^
   + Prologue
The solver generated the following counterexample to explain the faulty behavior:
--> date_courante : 1900-01-01
[RESULT] [PrestationsFamiliales.base_mensuelle] No two exceptions to ever overlap for this variable
[RESULT] [PrestationsFamiliales.âge_l512_3_2] This variable never returns an empty error
[RESULT] [PrestationsFamiliales.âge_l512_3_2] No two exceptions to ever overlap for this variable
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[RESULT] [AllocationFamilialesAvril2008.âge_minimum_alinéa_1_l521_3] This variable never returns an empty error
[RESULT] [AllocationFamilialesAvril2008.âge_minimum_alinéa_1_l521_3] No two exceptions to ever overlap for this variable
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported
[ERROR] The translation to Z3 failed:
[Z3 encoding] TUnit type not supported