diff --git a/src/plugins/e-acsl/tests/constructs/function_contract.i b/src/plugins/e-acsl/tests/constructs/function_contract.i
index 90eca5e7829d3e1e7911aca5d02d25ff4b61a872..512c41f6474f048d0bf26e64360764d289df8b21 100644
--- a/src/plugins/e-acsl/tests/constructs/function_contract.i
+++ b/src/plugins/e-acsl/tests/constructs/function_contract.i
@@ -45,9 +45,9 @@ void k(void) { X += Y; }
 
 // mix ensures + contract on return
 /*@ ensures X == 5; */
-int l() { 
+int l() {
   /*@ assert Y == 2; */
-  return X; 
+  return X;
 }
 
 // mix ensures and assumes
@@ -72,6 +72,40 @@ void m(void) { X += Y; }
   @   ensures X == 98; */
 void n(void) { X ++; }
 
+// several complete and disjoint clauses
+/*@
+    requires X > -1000;
+    ensures X == \old(Y);
+
+    behavior neg:
+        assumes Y < 0;
+        requires Y < 1;
+        ensures X == \old(Y);
+
+    behavior pos:
+        assumes Y >= 0;
+        requires Y > -1;
+        ensures X == \old(Y);
+
+    behavior odd:
+        assumes Y % 2 == 1;
+        requires (Y % 2) - 1 == 0;
+        ensures X == \old(Y);
+
+    behavior even:
+        assumes Y % 2 == 0;
+        requires (Y % 2) + 1 == 1;
+        ensures X == \old(Y);
+
+    complete behaviors neg, pos;
+    complete behaviors odd, even;
+    complete behaviors;
+
+    disjoint behaviors neg, pos;
+    disjoint behaviors odd, even;
+*/
+void o(void) { X = Y; }
+
 int main(void) {
   f();
   g();
@@ -82,5 +116,6 @@ int main(void) {
   l();
   m();
   n();
+  o();
   return 0;
 }
diff --git a/src/plugins/e-acsl/tests/constructs/stmt_contract.i b/src/plugins/e-acsl/tests/constructs/stmt_contract.i
index 3d105913dedf80485537533a730982636ee6ac4b..a8d4595526c599e502c9aa55f92111d6b38b2e31 100644
--- a/src/plugins/e-acsl/tests/constructs/stmt_contract.i
+++ b/src/plugins/e-acsl/tests/constructs/stmt_contract.i
@@ -3,7 +3,7 @@
 */
 
 int main(void) {
-  int x = 0, y = 2;
+  int x = 0, y = 2, z;
   // one ensures
   /*@ ensures x == 1; */
   x = 1;
@@ -21,9 +21,9 @@ int main(void) {
     @ requires y == 2; */
   x = x + y;
   // several behaviors
-  /*@ behavior b1: 
+  /*@ behavior b1:
     @   requires x == 5;
-    @   ensures x == 3; 
+    @   ensures x == 3;
     @ behavior b2:
     @   requires x == 3+y;
     @   requires y == 2;
@@ -32,7 +32,7 @@ int main(void) {
   // mix requires and assumes
   /*@ behavior b1:
     @   assumes x == 1;
-    @   requires x == 0; 
+    @   requires x == 0;
     @ behavior b2:
     @   assumes x == 3;
     @   assumes y == 2;
@@ -44,7 +44,30 @@ int main(void) {
   /*@ requires y == 2; */
   x = x + y;
 
-  /*@ requires x == 7; 
+  // complete and disjoint behaviors
+  /*@
+    requires x > -1000;
+    assigns x;
+    ensures z >= 0;
+
+    behavior pos:
+      assumes x >= 0;
+      ensures z == x;
+
+    behavior neg:
+      assumes x < 0;
+      ensures z == -x;
+
+    complete behaviors;
+    disjoint behaviors;
+  */
+  if (x < 0) {
+    z = -x;
+  } else {
+    z = x;
+  }
+
+  /*@ requires x == 7;
     @ ensures x == 7; */
   return 0;
 }