Merge pull request #167 from lucasccordeiro/aisimplifier

Aisimplifier

Author: kroening

regression/goto-analyzer/intervals2/intervals2.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main(){
+  int x;
+  if (x > 0) {
+    if (x < 20) {
+      assert(x > -10 && x < 100);
+    }
+  }
+  return 0;
+}

regression/goto-analyzer/intervals2/test.desc

@@ -0,0 +1,8 @@
+CORE
+intervals2.c
+--intervals
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals2.c line 7 function main, assertion x > -10 && x < 100: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/intervals3/intervals3.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main(){
+  int x;
+  if (x > 0) {
+    if (x < 20) {
+      assert(x > -10 || x < 100);
+    }
+  }
+  return 0;
+}

regression/goto-analyzer/intervals3/test.desc

@@ -0,0 +1,8 @@
+CORE
+intervals3.c
+--intervals
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals3.c line 7 function main, assertion x > -10 || x < 100: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/intervals4/intervals4.c

@@ -0,0 +1,12 @@
+//#include <assert.h>
+
+int main()
+{
+  int i;
+  
+  if(i>0)
+    if(i<3)
+      assert(i>=1 && i<=2);
+ 
+  return 0;
+} 

regression/goto-analyzer/intervals4/test.desc

@@ -0,0 +1,8 @@
+CORE
+intervals4.c
+--intervals
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals4.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/intervals5/intervals5.c

@@ -0,0 +1,12 @@
+//#include <assert.h>
+
+int main()
+{
+  int i;
+  
+  if(i>0)
+    if(i<3)
+      assert(i>=1 || i<=2);
+ 
+  return 0;
+} 

regression/goto-analyzer/intervals5/test.desc

@@ -0,0 +1,8 @@
+CORE
+intervals5.c
+--intervals
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals5.c line 9 function main, assertion i >= 1 || i <= 2: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/intervals6/intervals6.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main(){
+  int x;
+  if (x > 0) {
+    if (x < 20) {
+      assert(x < -10 || x > 100);
+    }
+  }
+  return 0;
+}

regression/goto-analyzer/intervals6/test.desc

@@ -0,0 +1,8 @@
+CORE
+intervals6.c
+--intervals
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals6.c line 7 function main, assertion x < -10 || x > 100: UNKNOWN$
+--
+^warning: ignoring