[Z3backend] Bad unit tests for EInj node

tests/test_proof/bad/enums_inj-empty.catala_en

@@ -0,0 +1,15 @@
+## Article
+
+```catala
+declaration enumeration E:
+  -- C1
+  -- C2
+
+declaration scope A:
+  context x content E
+  context y content integer
+
+scope A:
+  definition x equals C1
+  definition y under condition x = C1 consequence equals 1
+```

tests/test_proof/bad/enums_inj-overlap.catala_en

@@ -0,0 +1,17 @@
+## Article
+
+```catala
+declaration enumeration E:
+  -- C1
+  -- C2
+
+declaration scope A:
+  context x content E
+  context y content integer
+
+scope A:
+  definition x equals C1
+  definition y under condition x = C1 consequence equals 1
+  definition y under condition x = C2 consequence equals 2
+  definition y under condition x = C2 consequence equals 3
+```

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

@@ -0,0 +1,10 @@
+[ERROR] [A.y] This variable might return an empty error:
+  --> tests/test_proof/bad/enums_inj-empty.catala_en
+   | 
+10 |   context y content integer
+   |           ^
+   + Article
+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/enums_inj-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/enums_inj-overlap.catala_en
+   | 
+10 |   context y content integer
+   |           ^
+   + Article
+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