Negative tests for array length encoding

This commit is contained in:
Aymeric Fromherz 2022-03-16 11:23:36 +01:00
parent 123541dc34
commit bb57abf750
4 changed files with 43 additions and 0 deletions

View File

@ -0,0 +1,11 @@
## Test
```catala
declaration scope A:
context x content collection integer
context y content boolean
scope A:
definition x equals [0; 5]
definition y under condition (number of x) > 0 consequence equals true
```

View File

@ -0,0 +1,12 @@
## Test
```catala
declaration scope A:
context x content collection integer
context y content boolean
scope A:
definition x equals [0; 5]
definition y under condition (number of x) >= 0 consequence equals true
definition y under condition (number of x) = 1 consequence equals false
```

View File

@ -0,0 +1,10 @@
[ERROR] [A.y] This variable might return an empty error:
--> tests/test_proof/bad/array_length-empty.catala_en
|
6 | context y content boolean
| ^
+ Test
Counterexample generation is disabled so none was generated.
[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

View File

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