Home.md

@@ -229,3 +229,88 @@ x = TERM.readInt();
 
 [![](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/raw/master/code/website/nested-loops-main-no-merge.svg)](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/blob/master/code/website/nested-loops-main-no-merge-highres.svg)
 [![](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/raw/master/code/website/nested-loops-main.svg)](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/blob/master/code/website/nested-loops-main-highres.svg)
+
+
+## A function with many evaluation paths
+
+```c
+int max = 3;
+
+
+int main()
+{
+
+  y = 1;
+  z = TERM.readInt();
+  x = z;
+  while( 0 <= x && x <= max )
+  {
+    if( y <= 0 )
+    {
+      LED1.switchOn();
+      LED2.switchOff();
+    }
+    else
+    {
+      LED2.switchOn();
+      LED1.switchOff();
+    }
+
+    y = y * -1;
+    x = x + 1;
+  }
+
+
+
+
+  z = TERM.readInt();
+  x = z;
+  while( 0 <= x && x <= max )
+  {
+    if( y <= 0 )
+    {
+      LED1.switchOn();
+      LED2.switchOff();
+    }
+    else
+    {
+      LED2.switchOn();
+      LED1.switchOff();
+    }
+
+    y = y * -1;
+    x = x + 1;
+  }
+
+
+
+
+
+  z = TERM.readInt();
+  x = z;
+  while( 0 <= x && x <= max )
+  {
+    if( y <= 0 )
+    {
+      LED1.switchOn();
+      LED2.switchOff();
+    }
+    else
+    {
+      LED2.switchOn();
+      LED1.switchOff();
+    }
+
+    y = y * -1;
+    x = x + 1;
+  }
+
+
+
+  return 0;
+
+}
+```
+
+[![](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/raw/master/code/website/many-fragments-main-no-merge.svg)](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/blob/master/code/website/many-fragments-main-no-merge-highres.svg)
+[![](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/raw/master/code/website/many-fragments-main.svg)](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/blob/master/code/website/many-fragments-main-highres.svg)