From c0a8362fd9fe5fb9d22d78d182869e7079dedff2 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Wed, 12 Jan 2022 19:19:42 +0100 Subject: [PATCH] [skip ci] Z3 encoding: update last missing examples with TODOs --- .../good/output/enums.catala_en.Proof | 106 +---------------- .../good/output/structs.catala_en.Proof | 110 +----------------- 2 files changed, 8 insertions(+), 208 deletions(-) diff --git a/tests/test_proof/good/output/enums.catala_en.Proof b/tests/test_proof/good/output/enums.catala_en.Proof index 26b62047..5e25281b 100644 --- a/tests/test_proof/good/output/enums.catala_en.Proof +++ b/tests/test_proof/good/output/enums.catala_en.Proof @@ -1,104 +1,6 @@ -[RESULT] For this variable: - --> test_proof/good/enums.catala_en - | -13 | context x content integer - | ^ - + Test -This verification condition was generated for no two exceptions to ever overlap: -true && true && - true && true && true && true && true && ~ false && - true && true && true && ~ false && true && true && ~ false && - true && true && true && true && true && ~ false && - true && true && true && ~ false && true && true && ~ false && - true && true && true && ~ false && true && true && true && ~ false && - true && true && - ~ - if true then - if false then false else false && true && true || - if - match y_12 with - A: λ (a_44: integer) → true - | B: λ (b_45: T) → false then true else false && - true && true && true && true else false && true && true && - if true then - if false then false else false && true && true || - if - match y_12 with - A: λ (a_46: integer) → false - | B: λ (b_47: T) → true then true else false && - true && true && true && true else false && true && true - && true && ~ false && true -[RESULT] The translation to Z3 is the following: +[ERROR] The translation to Z3 failed: TODO -[RESULT] For this variable: - --> test_proof/good/enums.catala_en - | -13 | context x content integer - | ^ - + Test -This verification condition was generated for the variable definition never to return an empty error: -if true then - if true then - if false then false else false && true && true || - if false then false else false && true && true else false && - true && true || - if true then - if false then false else false && true && true || - if - match y_12 with - A: λ (a_48: integer) → true - | B: λ (b_49: T) → false then true else false && - true && true && true && true else false && true && true || - if true then - if false then false else false && true && true || - if - match y_12 with - A: λ (a_50: integer) → false - | B: λ (b_51: T) → true then true else false && - true && true && true && true else false && true && true else - false && true || false && true -[RESULT] The translation to Z3 is the following: +[ERROR] The translation to Z3 failed: TODO -[RESULT] For this variable: - --> test_proof/good/enums.catala_en - | -14 | context y content S - | ^ - + Test -This verification condition was generated for no two exceptions to ever overlap: -true && true && - true && true && true && ~ false && true && true && true && ~ false && - true && true && ~ false && - true && true && true && ~ false && true && true && true && ~ false && - true && true && ~ false && true && ~ false && true -[RESULT] The translation to Z3 is the following: -(let ((a!1 (and (and true (and (and true true) (not false))) - (and true (and (and true true) (not false))) - (and (and true true) (not false))))) - (and (and true true) a!1 a!1 true (not false) true)) -[RESULT] For this variable: - --> test_proof/good/enums.catala_en - | -14 | context y content S - | ^ - + Test -This verification condition was generated for the variable definition never to return an empty error: -if true then - if true then - if false then false else false && true && true || - if false then false else false && true && true else false && - true && true || - if true then - if false then false else false && true && true || - if true then true else false && true && true else false && - true && true else false && true || false && true -[RESULT] The translation to Z3 is the following: -(let ((a!1 (and (=> false false) (=> (not false) false) (and true true)))) -(let ((a!2 (or a!1 (and (=> true true) (=> (not true) false) (and true true))))) -(let ((a!3 (or (and (=> true (or a!1 a!1)) - (=> (not true) false) - (and true true)) - (and (=> true a!2) (=> (not true) false) (and true true))))) -(let ((a!4 (or (and (=> true a!3) (=> (not true) false) true) false))) - (and a!4 true))))) -[RESULT] Success: Empty unreachable +[RESULT] A.y: no two exceptions to ever overlap for this variable +[RESULT] A.y: this variable never returns an empty error diff --git a/tests/test_proof/good/output/structs.catala_en.Proof b/tests/test_proof/good/output/structs.catala_en.Proof index 6bd56ff0..5e25281b 100644 --- a/tests/test_proof/good/output/structs.catala_en.Proof +++ b/tests/test_proof/good/output/structs.catala_en.Proof @@ -1,108 +1,6 @@ -[RESULT] For this variable: - --> test_proof/good/structs.catala_en - | -13 | context x content integer - | ^ - + Test -This verification condition was generated for no two exceptions to ever overlap: -true && true && - true && true && true && true && true && true && true && ~ false && - true && true && true && ~ false && true && true && ~ false && - true && - true && true && true && true && true && true && true && true && ~ false - && true && true && true && ~ false && true && true && ~ false && - true && true && true && ~ false && true && true && true && ~ false && - true && true && - ~ - if true then - if false then false else false && true && true || - if y_4."a" = 0 && y_4."b"."c" then true else false && - true && true && true && true && true && true else false && - true && true && - if true then - if false then false else false && true && true || - if ~ y_4."a" = 0 || ~ y_4."b"."c" then true else false && - true && true && true && true && true && true && true && - true else false && true && true && true && ~ false && - true -[RESULT] The translation to Z3 is the following: +[ERROR] The translation to Z3 failed: TODO -[RESULT] For this variable: - --> test_proof/good/structs.catala_en - | -13 | context x content integer - | ^ - + Test -This verification condition was generated for the variable definition never to return an empty error: -if true then - if true then - if false then false else false && true && true || - if false then false else false && true && true else false && - true && true || - if true then - if false then false else false && true && true || - if y_4."a" = 0 && y_4."b"."c" then true else false && - true && true && true && true && true && true else false && - true && true || - if true then - if false then false else false && true && true || - if ~ y_4."a" = 0 || ~ y_4."b"."c" then true else false && - true && true && true && true && true && true && true && true else - false && true && true else false && true || false && true -[RESULT] The translation to Z3 is the following: +[ERROR] The translation to Z3 failed: TODO -[RESULT] For this variable: - --> test_proof/good/structs.catala_en - | -14 | context y content S - | ^ - + Test -This verification condition was generated for no two exceptions to ever overlap: -true && true && - true && true && true && true && true && ~ false && - true && true && true && ~ false && true && true && ~ false && - true && true && true && ~ false && true && true && true && ~ false && - true && true && ~ false && true && ~ false && true -[RESULT] The translation to Z3 is the following: -(and (and true true) - (and true true) - true - (and (and true true) (not false)) - (and true (and (and true true) (not false))) - (and (and true true) (not false)) - (and true (and (and true true) (not false))) - (and true (and (and true true) (not false))) - (and (and true true) (not false)) - true - (not false) - true) -[RESULT] For this variable: - --> test_proof/good/structs.catala_en - | -14 | context y content S - | ^ - + Test -This verification condition was generated for the variable definition never to return an empty error: -if true then - if true then - if false then false else false && true && true || - if false then false else false && true && true else false && - true && true || - if true then - if false then false else false && true && true || - if true then true && true && true else false && true && true else - false && true && true else false && true || false && true -[RESULT] The translation to Z3 is the following: -(let ((a!1 (and (=> false false) (=> (not false) false) (and true true))) - (a!2 (and (=> true (and (and true true) true)) - (=> (not true) false) - (and true true)))) -(let ((a!3 (or (and (=> true (or a!1 a!1)) - (=> (not true) false) - (and true true)) - (and (=> true (or a!1 a!2)) - (=> (not true) false) - (and true true))))) -(let ((a!4 (or (and (=> true a!3) (=> (not true) false) true) false))) - (and a!4 true)))) -[RESULT] Success: Empty unreachable +[RESULT] A.y: no two exceptions to ever overlap for this variable +[RESULT] A.y: this variable never returns an empty error