[Z3 encoding]: Add negative tests for rationals

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

@@ -0,0 +1,10 @@
+[ERROR] [A.y] This variable might return an empty error:
+ --> tests/test_proof/bad/rationals-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

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

@@ -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/rationals-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

tests/test_proof/bad/rationals-empty.catala_en

@@ -0,0 +1,11 @@
+## Test
+
+```catala
+declaration scope A:
+  context x content decimal
+  context y content boolean
+
+scope A:
+  definition x equals 1.
+  definition y under condition x >. 1./.3. consequence equals true
+```

tests/test_proof/bad/rationals-overlap.catala_en

@@ -0,0 +1,12 @@
+## Test
+
+```catala
+declaration scope A:
+  context x content decimal
+  context y content boolean
+
+scope A:
+  definition x equals 1.
+  definition y under condition x >=. 1./.3. consequence equals true
+  definition y under condition x <=. 1./.3. consequence equals false
+```