assumptions are not retro-active

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4140 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

regression/cbmc/Assumption1/main.c

@@ -0,0 +1,13 @@
+int main()
+{
+  int x;
+  
+  __CPROVER_assume(x>=0);
+  assert(x!=-1);
+
+  // assumptions are not retro-active
+  assert(x==1); // fails
+  __CPROVER_assume(x==1);
+  assert(x==1); // passes
+}
+

regression/cbmc/Assumption1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--