Sort VCs by alphabetical order

compiler/verification/conditions.ml

@@ -431,4 +431,15 @@ let rec generate_verification_conditions_scopes
 let generate_verification_conditions
     (p : program) (s : Dcalc.Ast.ScopeName.t option) :
     verification_condition list =
-  generate_verification_conditions_scopes p.decl_ctx p.scopes s
+  let vcs = generate_verification_conditions_scopes p.decl_ctx p.scopes s in
+  (* We sort this list by scope name and then variable name to ensure consistent
+     output for testing*)
+  List.sort
+    (fun vc1 vc2 ->
+      let to_str vc =
+        Format.asprintf "%s.%s"
+          (Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
+          (Bindlib.name_of (Pos.unmark vc.vc_variable))
+      in
+      String.compare (to_str vc1) (to_str vc2))
+    vcs

tests/test_proof/bad/output/enums-empty.catala_en.Proof

@@ -1,5 +1,3 @@
-[RESULT] [A.y] This variable never returns an empty error
-[RESULT] [A.y] No two exceptions to ever overlap for this variable
 [ERROR] [A.x] This variable might return an empty error:
   --> tests/test_proof/bad/enums-empty.catala_en
    | 
@@ -8,3 +6,5 @@
    + Test
 Counterexample generation is disabled so none was generated.
 [RESULT] [A.x] No two exceptions to ever overlap for this variable
+[RESULT] [A.y] This variable never returns an empty error
+[RESULT] [A.y] No two exceptions to ever overlap for this variable

tests/test_proof/bad/output/enums-overlap.catala_en.Proof

@@ -1,5 +1,3 @@
-[RESULT] [A.y] This variable never returns an empty error
-[RESULT] [A.y] No two exceptions to ever overlap for this variable
 [RESULT] [A.x] This variable never returns an empty error
 [ERROR] [A.x] At least two exceptions overlap for this variable:
   --> tests/test_proof/bad/enums-overlap.catala_en
@@ -8,3 +6,5 @@
    |           ^
    + Test
 Counterexample generation is disabled so none was generated.
+[RESULT] [A.y] This variable never returns an empty error
+[RESULT] [A.y] No two exceptions to ever overlap for this variable

tests/test_proof/bad/output/prolala_motivating_example.catala_en.Proof

@@ -1,13 +1,3 @@
-[RESULT] [Amount.is_student] This variable never returns an empty error
-[RESULT] [Amount.is_student] No two exceptions to ever overlap for this variable
-[RESULT] [Amount.is_professor] This variable never returns an empty error
-[RESULT] [Amount.is_professor] No two exceptions to ever overlap for this variable
-[RESULT] [Amount.number_of_advisors] This variable never returns an empty error
-[RESULT] [Amount.number_of_advisors] No two exceptions to ever overlap for this variable
-[RESULT] [Amount.eligibility.is_student] No two exceptions to ever overlap for this variable
-[RESULT] [Amount.eligibility.is_professor] No two exceptions to ever overlap for this variable
-[RESULT] [Amount.correct_amount] This variable never returns an empty error
-[RESULT] [Amount.correct_amount] No two exceptions to ever overlap for this variable
 [ERROR] [Amount.amount] This variable might return an empty error:
   --> tests/test_proof/bad/prolala_motivating_example.catala_en
    | 
@@ -17,12 +7,16 @@
    +-+ Amount
 Counterexample generation is disabled so none was generated.
 [RESULT] [Amount.amount] No two exceptions to ever overlap for this variable
-[RESULT] [Eligibility.is_student] This variable never returns an empty error
-[RESULT] [Eligibility.is_student] No two exceptions to ever overlap for this variable
-[RESULT] [Eligibility.is_professor] This variable never returns an empty error
-[RESULT] [Eligibility.is_professor] No two exceptions to ever overlap for this variable
-[RESULT] [Eligibility.is_eligible_correct] This variable never returns an empty error
-[RESULT] [Eligibility.is_eligible_correct] No two exceptions to ever overlap for this variable
+[RESULT] [Amount.correct_amount] This variable never returns an empty error
+[RESULT] [Amount.correct_amount] No two exceptions to ever overlap for this variable
+[RESULT] [Amount.eligibility.is_professor] No two exceptions to ever overlap for this variable
+[RESULT] [Amount.eligibility.is_student] No two exceptions to ever overlap for this variable
+[RESULT] [Amount.is_professor] This variable never returns an empty error
+[RESULT] [Amount.is_professor] No two exceptions to ever overlap for this variable
+[RESULT] [Amount.is_student] This variable never returns an empty error
+[RESULT] [Amount.is_student] No two exceptions to ever overlap for this variable
+[RESULT] [Amount.number_of_advisors] This variable never returns an empty error
+[RESULT] [Amount.number_of_advisors] No two exceptions to ever overlap for this variable
 [ERROR] [Eligibility.is_eligible] This variable might return an empty error:
   --> tests/test_proof/bad/prolala_motivating_example.catala_en
    | 
@@ -39,3 +33,9 @@ Counterexample generation is disabled so none was generated.
    + ProLaLa 2022 Super Cash Bonus
    +-+ Eligibility
 Counterexample generation is disabled so none was generated.
+[RESULT] [Eligibility.is_eligible_correct] This variable never returns an empty error
+[RESULT] [Eligibility.is_eligible_correct] No two exceptions to ever overlap for this variable
+[RESULT] [Eligibility.is_professor] This variable never returns an empty error
+[RESULT] [Eligibility.is_professor] No two exceptions to ever overlap for this variable
+[RESULT] [Eligibility.is_student] This variable never returns an empty error
+[RESULT] [Eligibility.is_student] No two exceptions to ever overlap for this variable

tests/test_proof/bad/output/sat_solving.catala_en.Proof

@@ -1,5 +1,13 @@
 [RESULT] [A.x1] This variable never returns an empty error
 [RESULT] [A.x1] No two exceptions to ever overlap for this variable
+[ERROR] [A.x10] This variable might return an empty error:
+  --> tests/test_proof/bad/sat_solving.catala_en
+   | 
+15 |   context x10 content boolean
+   |           ^^^
+   + Test
+Counterexample generation is disabled so none was generated.
+[RESULT] [A.x10] No two exceptions to ever overlap for this variable
 [RESULT] [A.x2] This variable never returns an empty error
 [RESULT] [A.x2] No two exceptions to ever overlap for this variable
 [RESULT] [A.x3] This variable never returns an empty error
@@ -16,11 +24,3 @@
 [RESULT] [A.x8] No two exceptions to ever overlap for this variable
 [RESULT] [A.x9] This variable never returns an empty error
 [RESULT] [A.x9] No two exceptions to ever overlap for this variable
-[ERROR] [A.x10] This variable might return an empty error:
-  --> tests/test_proof/bad/sat_solving.catala_en
-   | 
-15 |   context x10 content boolean
-   |           ^^^
-   + Test
-Counterexample generation is disabled so none was generated.
-[RESULT] [A.x10] No two exceptions to ever overlap for this variable

tests/test_proof/bad/output/structs-empty.catala_en.Proof

@@ -1,5 +1,3 @@
-[RESULT] [A.y] This variable never returns an empty error
-[RESULT] [A.y] No two exceptions to ever overlap for this variable
 [ERROR] [A.x] This variable might return an empty error:
   --> tests/test_proof/bad/structs-empty.catala_en
    | 
@@ -8,3 +6,5 @@
    + Test
 Counterexample generation is disabled so none was generated.
 [RESULT] [A.x] No two exceptions to ever overlap for this variable
+[RESULT] [A.y] This variable never returns an empty error
+[RESULT] [A.y] No two exceptions to ever overlap for this variable

tests/test_proof/bad/output/structs-overlap.catala_en.Proof

@@ -1,5 +1,3 @@
-[RESULT] [A.y] This variable never returns an empty error
-[RESULT] [A.y] No two exceptions to ever overlap for this variable
 [RESULT] [A.x] This variable never returns an empty error
 [ERROR] [A.x] At least two exceptions overlap for this variable:
   --> tests/test_proof/bad/structs-overlap.catala_en
@@ -8,3 +6,5 @@
    |           ^
    + Test
 Counterexample generation is disabled so none was generated.
+[RESULT] [A.y] This variable never returns an empty error
+[RESULT] [A.y] No two exceptions to ever overlap for this variable

tests/test_proof/good/output/enums-arith.catala_en.Proof

@@ -1,4 +1,4 @@
-[RESULT] [A.y] This variable never returns an empty error
-[RESULT] [A.y] No two exceptions to ever overlap for this variable
 [RESULT] [A.x] This variable never returns an empty error
 [RESULT] [A.x] No two exceptions to ever overlap for this variable
+[RESULT] [A.y] This variable never returns an empty error
+[RESULT] [A.y] No two exceptions to ever overlap for this variable

tests/test_proof/good/output/enums.catala_en.Proof

@@ -1,4 +1,4 @@
-[RESULT] [A.y] This variable never returns an empty error
-[RESULT] [A.y] No two exceptions to ever overlap for this variable
 [RESULT] [A.x] This variable never returns an empty error
 [RESULT] [A.x] No two exceptions to ever overlap for this variable
+[RESULT] [A.y] This variable never returns an empty error
+[RESULT] [A.y] No two exceptions to ever overlap for this variable

tests/test_proof/good/output/simple_vars.catala_en.Proof

@@ -1,6 +1,6 @@
-[RESULT] [A.y] This variable never returns an empty error
-[RESULT] [A.y] No two exceptions to ever overlap for this variable
 [RESULT] [A.x] This variable never returns an empty error
 [RESULT] [A.x] No two exceptions to ever overlap for this variable
+[RESULT] [A.y] This variable never returns an empty error
+[RESULT] [A.y] No two exceptions to ever overlap for this variable
 [RESULT] [A.z] This variable never returns an empty error
 [RESULT] [A.z] No two exceptions to ever overlap for this variable

tests/test_proof/good/output/structs.catala_en.Proof

@@ -1,4 +1,4 @@
-[RESULT] [A.y] This variable never returns an empty error
-[RESULT] [A.y] No two exceptions to ever overlap for this variable
 [RESULT] [A.x] This variable never returns an empty error
 [RESULT] [A.x] No two exceptions to ever overlap for this variable
+[RESULT] [A.y] This variable never returns an empty error
+[RESULT] [A.y] No two exceptions to ever overlap for this variable