Z3encoding: Add bad tests related to dates [skip ci]

This commit is contained in:
Aymeric Fromherz 2022-01-13 20:28:28 +01:00
parent 52f33aa1ae
commit c8be75ca75
4 changed files with 39 additions and 0 deletions

View File

@ -0,0 +1,13 @@
## Test
```catala
declaration scope A:
context x content date
context y content boolean
scope A:
definition x equals |2022-01-16|
definition y under condition x >=@ |2010-01-01| and x <@ |2015-01-01| consequence equals false
definition y under condition x >=@ |2015-01-01| and x <@ |2020-01-01| consequence equals true
definition y under condition x >=@ |2020-01-01| consequence equals false
```

View File

@ -0,0 +1,14 @@
## Test
```catala
declaration scope A:
context x content date
context y content boolean
scope A:
definition x equals |2022-01-16|
definition y under condition x <=@ |2010-01-01| consequence equals true
definition y under condition x >=@ |2010-01-01| and x <@ |2015-01-01| consequence equals false
definition y under condition x >=@ |2015-01-01| and x <@ |2020-01-01| consequence equals true
definition y under condition x >=@ |2020-01-01| consequence equals false
```

View File

@ -0,0 +1,6 @@
[ERROR] The translation to Z3 failed:
TODO
[ERROR] The translation to Z3 failed:
TODO
[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,6 @@
[ERROR] The translation to Z3 failed:
TODO
[ERROR] The translation to Z3 failed:
TODO
[RESULT] [A.x] This variable never returns an empty error
[RESULT] [A.x] No two exceptions to ever overlap for this variable