From 1636f42c0fa2b26d878d470e760517334eee3763 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@cs.ox.ac.uk>
Date: Sat, 17 Sep 2016 20:25:42 +0100
Subject: [PATCH 1/3] line terminators

---
 regression/cbmc-concurrency/deadlock1/main.c  |  44 +--
 regression/cbmc-concurrency/deadlock2/main.c  |  46 +--
 .../cbmc-concurrency/norace_array1/main.c     |  52 +--
 .../cbmc-concurrency/norace_scalar1/main.c    |  52 +--
 .../cbmc-concurrency/norace_struct1/main.c    |  52 +--
 .../cbmc-concurrency/struct_and_array1/main.c |  80 ++---
 .../cbmc-from-CVS/Struct_Pointer2/main.c      |  54 +--
 .../cbmc-from-CVS/Unbounded_Array5/main.c     |  40 +--
 .../cbmc-from-CVS/return2/tcas_v23_523.c      | 336 +++++++++---------
 regression/cbmc-with-incr/Float-div1/main.c   | 100 +++---
 .../cbmc-with-incr/Float-to-double2/main.c    |  24 +-
 regression/cbmc-with-incr/Float19/main.c      |  48 +--
 regression/cbmc-with-incr/Float20/main.c      | 112 +++---
 regression/cbmc-with-incr/Float21/main.c      | 132 +++----
 regression/cbmc-with-incr/Recursion4/main.c   |  34 +-
 regression/cpp-from-CVS/Array1/main.cpp       |  22 +-
 regression/cpp-from-CVS/Array2/main.cpp       |  22 +-
 regression/cpp/Decltype2/main.cpp             |  28 +-
 regression/cpp/Decltype3/main.cpp             |  36 +-
 19 files changed, 657 insertions(+), 657 deletions(-)

diff --git a/regression/cbmc-concurrency/deadlock1/main.c b/regression/cbmc-concurrency/deadlock1/main.c
index 2e134bc5f9d..891fb419e7e 100644
--- a/regression/cbmc-concurrency/deadlock1/main.c
+++ b/regression/cbmc-concurrency/deadlock1/main.c
@@ -1,22 +1,22 @@
-#include <pthread.h>
-#include <stdlib.h>
-#include <assert.h>
-
-pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
-
-void* lock_never_unlock_002_tsk_001(void* pram) { 
-  pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);  
-  return NULL; 
-} 
-
-void main() { 
-  pthread_t tid1; 
-  pthread_t tid2; 
-  pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL); 
-  pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL); 
-  pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL); 
-  pthread_join(tid1, NULL); 
-  pthread_join(tid2, NULL); 
-  // deadlock in the threads; assertion should not be reachable
-  assert(0);
-} 
+#include <pthread.h>
+#include <stdlib.h>
+#include <assert.h>
+
+pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void* lock_never_unlock_002_tsk_001(void* pram) { 
+  pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);  
+  return NULL; 
+} 
+
+void main() { 
+  pthread_t tid1; 
+  pthread_t tid2; 
+  pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL); 
+  pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL); 
+  pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL); 
+  pthread_join(tid1, NULL); 
+  pthread_join(tid2, NULL); 
+  // deadlock in the threads; assertion should not be reachable
+  assert(0);
+} 
diff --git a/regression/cbmc-concurrency/deadlock2/main.c b/regression/cbmc-concurrency/deadlock2/main.c
index c2ebc9b9a01..d8000f2027d 100644
--- a/regression/cbmc-concurrency/deadlock2/main.c
+++ b/regression/cbmc-concurrency/deadlock2/main.c
@@ -1,23 +1,23 @@
-#include <pthread.h>
-#include <stdlib.h>
-#include <assert.h>
-
-pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
-
-void* lock_never_unlock_002_tsk_001(void* pram) { 
-  pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);  
-  pthread_mutex_unlock(&lock_never_unlock_002_glb_mutex);  
-  return NULL; 
-} 
-
-void main() { 
-  pthread_t tid1; 
-  pthread_t tid2; 
-  pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL); 
-  pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL); 
-  pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL); 
-  pthread_join(tid1, NULL); 
-  pthread_join(tid2, NULL); 
-  // no deadlock in the threads; assertion should be reached
-  assert(0);
-} 
+#include <pthread.h>
+#include <stdlib.h>
+#include <assert.h>
+
+pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void* lock_never_unlock_002_tsk_001(void* pram) { 
+  pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);  
+  pthread_mutex_unlock(&lock_never_unlock_002_glb_mutex);  
+  return NULL; 
+} 
+
+void main() { 
+  pthread_t tid1; 
+  pthread_t tid2; 
+  pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL); 
+  pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL); 
+  pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL); 
+  pthread_join(tid1, NULL); 
+  pthread_join(tid2, NULL); 
+  // no deadlock in the threads; assertion should be reached
+  assert(0);
+} 
diff --git a/regression/cbmc-concurrency/norace_array1/main.c b/regression/cbmc-concurrency/norace_array1/main.c
index debc6871438..721065d6182 100644
--- a/regression/cbmc-concurrency/norace_array1/main.c
+++ b/regression/cbmc-concurrency/norace_array1/main.c
@@ -1,26 +1,26 @@
-#include <pthread.h>
-#include <assert.h>
-
-int s[2];
-
-void* thread_0(void* arg)
-{
-  s[0] = 2;
-  assert(s[0] == 2);
-  return NULL;
-}
-
-void* thread_1(void* arg)
-{
-  s[1] = 1;
-  assert(s[1] == 1);
-  return NULL;
-}
-
-int main(void)
-{
-  pthread_t thread0, thread1;
-  pthread_create(&thread0, NULL, thread_0, 0);
-  pthread_create(&thread1, NULL, thread_1, 0);
-  return 0;
-}
+#include <pthread.h>
+#include <assert.h>
+
+int s[2];
+
+void* thread_0(void* arg)
+{
+  s[0] = 2;
+  assert(s[0] == 2);
+  return NULL;
+}
+
+void* thread_1(void* arg)
+{
+  s[1] = 1;
+  assert(s[1] == 1);
+  return NULL;
+}
+
+int main(void)
+{
+  pthread_t thread0, thread1;
+  pthread_create(&thread0, NULL, thread_0, 0);
+  pthread_create(&thread1, NULL, thread_1, 0);
+  return 0;
+}
diff --git a/regression/cbmc-concurrency/norace_scalar1/main.c b/regression/cbmc-concurrency/norace_scalar1/main.c
index 8c39510fd73..eb5baf7fd6a 100644
--- a/regression/cbmc-concurrency/norace_scalar1/main.c
+++ b/regression/cbmc-concurrency/norace_scalar1/main.c
@@ -1,26 +1,26 @@
-#include <pthread.h>
-#include <assert.h>
-
-int f0, f1;
-
-void* thread_0(void* arg)
-{
-  f0 = 2;
-  assert(f0 == 2);
-  return NULL;
-}
-
-void* thread_1(void* arg)
-{
-  f1 = 1;
-  assert(f1 == 1);
-  return NULL;
-}
-
-int main(void)
-{
-  pthread_t thread0, thread1;
-  pthread_create(&thread0, NULL, thread_0, 0);
-  pthread_create(&thread1, NULL, thread_1, 0);
-  return 0;
-}
+#include <pthread.h>
+#include <assert.h>
+
+int f0, f1;
+
+void* thread_0(void* arg)
+{
+  f0 = 2;
+  assert(f0 == 2);
+  return NULL;
+}
+
+void* thread_1(void* arg)
+{
+  f1 = 1;
+  assert(f1 == 1);
+  return NULL;
+}
+
+int main(void)
+{
+  pthread_t thread0, thread1;
+  pthread_create(&thread0, NULL, thread_0, 0);
+  pthread_create(&thread1, NULL, thread_1, 0);
+  return 0;
+}
diff --git a/regression/cbmc-concurrency/norace_struct1/main.c b/regression/cbmc-concurrency/norace_struct1/main.c
index 1fca06df093..31dd7e324e3 100644
--- a/regression/cbmc-concurrency/norace_struct1/main.c
+++ b/regression/cbmc-concurrency/norace_struct1/main.c
@@ -1,26 +1,26 @@
-#include <pthread.h>
-#include <assert.h>
-
-struct { int f0; int f1; } s;
-
-void* thread_0(void* arg)
-{
-  s.f0 = 2;
-  assert(s.f0 == 2);
-  return NULL;
-}
-
-void* thread_1(void* arg)
-{
-  s.f1 = 1;
-  assert(s.f1 == 1);
-  return NULL;
-}
-
-int main(void)
-{
-  pthread_t thread0, thread1;
-  pthread_create(&thread0, NULL, thread_0, 0);
-  pthread_create(&thread1, NULL, thread_1, 0);
-  return 0;
-}
+#include <pthread.h>
+#include <assert.h>
+
+struct { int f0; int f1; } s;
+
+void* thread_0(void* arg)
+{
+  s.f0 = 2;
+  assert(s.f0 == 2);
+  return NULL;
+}
+
+void* thread_1(void* arg)
+{
+  s.f1 = 1;
+  assert(s.f1 == 1);
+  return NULL;
+}
+
+int main(void)
+{
+  pthread_t thread0, thread1;
+  pthread_create(&thread0, NULL, thread_0, 0);
+  pthread_create(&thread1, NULL, thread_1, 0);
+  return 0;
+}
diff --git a/regression/cbmc-concurrency/struct_and_array1/main.c b/regression/cbmc-concurrency/struct_and_array1/main.c
index cc3dd606089..42164904232 100644
--- a/regression/cbmc-concurrency/struct_and_array1/main.c
+++ b/regression/cbmc-concurrency/struct_and_array1/main.c
@@ -1,40 +1,40 @@
-#include <pthread.h>
-
-typedef struct st_t
-{
-  unsigned char x;
-  unsigned char y;
-} ST;
-
-ST st;
-
-char my_array[10];
-
-_Bool done1, done2;
-
-void *foo1(void *arg1)
-{
-  st.x = 1;
-  my_array[1]=1;
-  done1 = 1;
-}
-
-void *foo2(void *arg2)
-{
-  st.y = 1;
-  my_array[2]=2;
-  done2 = 1;
-}
-
-int main()
-{
-  pthread_t t;
-  pthread_create(&t,NULL,foo1,NULL);
-  pthread_create(&t,NULL,foo2,NULL);
-  
-  if(done1 && done2)
-  {
-    assert(st.x==st.y);
-    assert(my_array[1]==my_array[2]);
-  }
-}
+#include <pthread.h>
+
+typedef struct st_t
+{
+  unsigned char x;
+  unsigned char y;
+} ST;
+
+ST st;
+
+char my_array[10];
+
+_Bool done1, done2;
+
+void *foo1(void *arg1)
+{
+  st.x = 1;
+  my_array[1]=1;
+  done1 = 1;
+}
+
+void *foo2(void *arg2)
+{
+  st.y = 1;
+  my_array[2]=2;
+  done2 = 1;
+}
+
+int main()
+{
+  pthread_t t;
+  pthread_create(&t,NULL,foo1,NULL);
+  pthread_create(&t,NULL,foo2,NULL);
+  
+  if(done1 && done2)
+  {
+    assert(st.x==st.y);
+    assert(my_array[1]==my_array[2]);
+  }
+}
diff --git a/regression/cbmc-from-CVS/Struct_Pointer2/main.c b/regression/cbmc-from-CVS/Struct_Pointer2/main.c
index b50cfcd0f97..bf8ab0817c2 100644
--- a/regression/cbmc-from-CVS/Struct_Pointer2/main.c
+++ b/regression/cbmc-from-CVS/Struct_Pointer2/main.c
@@ -1,27 +1,27 @@
-#include <stdlib.h>
-#include <assert.h>
-
-struct mylist
-{
-  int  data;
-  struct mylist *next;
-};
-
-int main()
-{
-  struct mylist *p;
-
-  // Allocations:
-  p=malloc( sizeof(struct mylist ) );  
-  p->data=1;
-  p->next=malloc( sizeof(struct mylist ) );  
-  p->next->data=2;
-  p->next->next=malloc( sizeof(struct mylist ) );    
-  p->next->next->data=3;
-  p->next->next->next=malloc( sizeof(struct mylist ) );    
-  p->next->next->next->data=4;
-  
-  assert(p->next->next->data==3);
-
-  return 0;
-}
+#include <stdlib.h>
+#include <assert.h>
+
+struct mylist
+{
+  int  data;
+  struct mylist *next;
+};
+
+int main()
+{
+  struct mylist *p;
+
+  // Allocations:
+  p=malloc( sizeof(struct mylist ) );  
+  p->data=1;
+  p->next=malloc( sizeof(struct mylist ) );  
+  p->next->data=2;
+  p->next->next=malloc( sizeof(struct mylist ) );    
+  p->next->next->data=3;
+  p->next->next->next=malloc( sizeof(struct mylist ) );    
+  p->next->next->next->data=4;
+  
+  assert(p->next->next->data==3);
+
+  return 0;
+}
diff --git a/regression/cbmc-from-CVS/Unbounded_Array5/main.c b/regression/cbmc-from-CVS/Unbounded_Array5/main.c
index d797c3c2923..aebfa1e3a94 100644
--- a/regression/cbmc-from-CVS/Unbounded_Array5/main.c
+++ b/regression/cbmc-from-CVS/Unbounded_Array5/main.c
@@ -1,20 +1,20 @@
-int mem[__CPROVER_constant_infinity_uint];
-
-int  main()
-{
-  int i, j, mem_j;
-  
-  mem[0] = 0;
-  mem[1] = 1;
-
-  mem[j] = 1;
-  mem_j = mem[j];
-  assert(mem_j == 1);
-
-  mem[i] = mem[mem_j];
-   
-  unsigned xxxi=mem[i];
-  unsigned xxx1=mem[1];
-
-  __CPROVER_assert(xxxi == xxx1, "Check infinite mem");
-}
+int mem[__CPROVER_constant_infinity_uint];
+
+int  main()
+{
+  int i, j, mem_j;
+  
+  mem[0] = 0;
+  mem[1] = 1;
+
+  mem[j] = 1;
+  mem_j = mem[j];
+  assert(mem_j == 1);
+
+  mem[i] = mem[mem_j];
+   
+  unsigned xxxi=mem[i];
+  unsigned xxx1=mem[1];
+
+  __CPROVER_assert(xxxi == xxx1, "Check infinite mem");
+}
diff --git a/regression/cbmc-from-CVS/return2/tcas_v23_523.c b/regression/cbmc-from-CVS/return2/tcas_v23_523.c
index 6670715a6d2..4504d9c4dd4 100644
--- a/regression/cbmc-from-CVS/return2/tcas_v23_523.c
+++ b/regression/cbmc-from-CVS/return2/tcas_v23_523.c
@@ -1,171 +1,171 @@
-
-/*  -*- Last-Edit:  Fri Jan 29 11:13:27 1993 by Tarak S. Goradia; -*- */
+
+/*  -*- Last-Edit:  Fri Jan 29 11:13:27 1993 by Tarak S. Goradia; -*- */
 /* $Log: tcas_v23_523.c,v $
 /* Revision 1.1  2006-04-04 08:38:22  kroening
 /* more
-/*
- * Revision 1.2  1993/03/12  19:29:50  foster
- * Correct logic bug which didn't allow output of 2 - hf
- * */
-
-#include <stdio.h>
-
-#define OLEV       600		/* in feets/minute */
-#define MAXALTDIFF 600		/* max altitude difference in feet */
-#define MINSEP     300          /* min separation in feet */
-#define NOZCROSS   100		/* in feet */
-				/* variables */
-
-typedef int bool;
-
-int Cur_Vertical_Sep;
-bool High_Confidence;
-bool Two_of_Three_Reports_Valid;
-
-int Own_Tracked_Alt;
-int Own_Tracked_Alt_Rate;
-int Other_Tracked_Alt;
-
-int Alt_Layer_Value;		/* 0, 1, 2, 3 */
-int Positive_RA_Alt_Thresh[4];
-
-int Up_Separation;
-int Down_Separation;
-
-				/* state variables */
-int Other_RAC;			/* NO_INTENT, DO_NOT_CLIMB, DO_NOT_DESCEND */
-#define NO_INTENT 0
-#define DO_NOT_CLIMB 1
-#define DO_NOT_DESCEND 2
-
-int Other_Capability;		/* TCAS_TA, OTHER */
-#define TCAS_TA 1
-#define OTHER 2
-
-int Climb_Inhibit;		/* true/false */
-
-#define UNRESOLVED 0
-#define UPWARD_RA 1
-#define DOWNWARD_RA 2
-
-int  ALIM();
-int  Inhibit_Biased_Climb();
-bool   Non_Crossing_Biased_Climb();
-bool   Non_Crossing_Biased_Descend();
-bool   Own_Below_Threat();
-bool   Own_Above_Threat();
-int  alt_sep_test();
-void initialize()
-{
-    Positive_RA_Alt_Thresh[0] = 400;
-    Positive_RA_Alt_Thresh[1] = 500;
-    Positive_RA_Alt_Thresh[2] = 640;
-    Positive_RA_Alt_Thresh[3] = 740;
-}
-
-int ALIM ()
-{
- return Positive_RA_Alt_Thresh[Alt_Layer_Value];
-}
-
-int Inhibit_Biased_Climb ()
-{
-    return (Climb_Inhibit ? Up_Separation + NOZCROSS : Up_Separation);
-}
-
-bool Non_Crossing_Biased_Climb()
-{
-    int upward_preferred;
-    int upward_crossing_situation;
-    bool result;
-
-    upward_preferred = Inhibit_Biased_Climb() > Down_Separation;
-    if (upward_preferred)
-    {
-	result = !(Own_Below_Threat()) || ((Own_Below_Threat()) && (!(Down_Separation >= ALIM())));
-    }
-    else
-    {	
-	result = Own_Above_Threat() && (Cur_Vertical_Sep >= MINSEP) && (Up_Separation >= ALIM());
-    }
-    return result;
-}
-
-bool Non_Crossing_Biased_Descend()
-{
-    int upward_preferred;
-    int upward_crossing_situation;
-    bool result;
-
-    upward_preferred = (Up_Separation + NOZCROSS) > Down_Separation;
-    if (upward_preferred)
-    {
-	result = Own_Below_Threat() && (Cur_Vertical_Sep >= MINSEP) && (Down_Separation >= ALIM());
-    }
-    else
-    {
-	result = !(Own_Above_Threat()) || ((Own_Above_Threat()) && (Up_Separation >= ALIM()));
-    }
-    return result;
-}
-
-bool Own_Below_Threat()
-{
-    return (Own_Tracked_Alt < Other_Tracked_Alt);
-}
-
-bool Own_Above_Threat()
-{
-    return (Other_Tracked_Alt < Own_Tracked_Alt);
-}
-
-int alt_sep_test()
-{
-    bool enabled, tcas_equipped, intent_not_known;
-    bool need_upward_RA, need_downward_RA;
-    int alt_sep;
-
-    enabled = High_Confidence && (Own_Tracked_Alt_Rate <= OLEV) && (Cur_Vertical_Sep > MAXALTDIFF);
-    tcas_equipped = Other_Capability == TCAS_TA;
-    intent_not_known = Two_of_Three_Reports_Valid && Other_RAC == NO_INTENT;
-    
-    alt_sep = UNRESOLVED;
-    
-    if (enabled && ((tcas_equipped && intent_not_known) || !tcas_equipped))
-    {
-	need_upward_RA = Non_Crossing_Biased_Climb() && Own_Below_Threat();
-	need_downward_RA = Non_Crossing_Biased_Descend() && Own_Above_Threat();
-	if (need_upward_RA && need_downward_RA)
-        /* unreachable: requires Own_Below_Threat and Own_Above_Threat
-           to both be true - that requires Own_Tracked_Alt < Other_Tracked_Alt
-           and Other_Tracked_Alt < Own_Tracked_Alt, which isn't possible */
-	    alt_sep = UNRESOLVED;
-	else if (need_upward_RA)
-	    alt_sep = UPWARD_RA;
-	else if (need_downward_RA)
-	    alt_sep = DOWNWARD_RA;
-	else
-	    alt_sep = UNRESOLVED;
-    }
-    
-    return alt_sep;
-}
-
-main(int argc, char*argv[])
-{
-
-  initialize();
-  Cur_Vertical_Sep =  860; 
-  High_Confidence = 1; 
-  Two_of_Three_Reports_Valid = 1; 
-  Own_Tracked_Alt =  618; 
-  Own_Tracked_Alt_Rate =  329; 
-  Other_Tracked_Alt =  574; 
-  Alt_Layer_Value =  4; 
-  Up_Separation =  893; 
-  Down_Separation =  914; 
-  Other_RAC =  0; 
-  Other_Capability =  2; 
-  Climb_Inhibit =  0; 
-  assert(alt_sep_test()==0);
-}
+/*
+ * Revision 1.2  1993/03/12  19:29:50  foster
+ * Correct logic bug which didn't allow output of 2 - hf
+ * */
+
+#include <stdio.h>
+
+#define OLEV       600		/* in feets/minute */
+#define MAXALTDIFF 600		/* max altitude difference in feet */
+#define MINSEP     300          /* min separation in feet */
+#define NOZCROSS   100		/* in feet */
+				/* variables */
+
+typedef int bool;
+
+int Cur_Vertical_Sep;
+bool High_Confidence;
+bool Two_of_Three_Reports_Valid;
+
+int Own_Tracked_Alt;
+int Own_Tracked_Alt_Rate;
+int Other_Tracked_Alt;
+
+int Alt_Layer_Value;		/* 0, 1, 2, 3 */
+int Positive_RA_Alt_Thresh[4];
+
+int Up_Separation;
+int Down_Separation;
+
+				/* state variables */
+int Other_RAC;			/* NO_INTENT, DO_NOT_CLIMB, DO_NOT_DESCEND */
+#define NO_INTENT 0
+#define DO_NOT_CLIMB 1
+#define DO_NOT_DESCEND 2
+
+int Other_Capability;		/* TCAS_TA, OTHER */
+#define TCAS_TA 1
+#define OTHER 2
+
+int Climb_Inhibit;		/* true/false */
+
+#define UNRESOLVED 0
+#define UPWARD_RA 1
+#define DOWNWARD_RA 2
+
+int  ALIM();
+int  Inhibit_Biased_Climb();
+bool   Non_Crossing_Biased_Climb();
+bool   Non_Crossing_Biased_Descend();
+bool   Own_Below_Threat();
+bool   Own_Above_Threat();
+int  alt_sep_test();
+void initialize()
+{
+    Positive_RA_Alt_Thresh[0] = 400;
+    Positive_RA_Alt_Thresh[1] = 500;
+    Positive_RA_Alt_Thresh[2] = 640;
+    Positive_RA_Alt_Thresh[3] = 740;
+}
+
+int ALIM ()
+{
+ return Positive_RA_Alt_Thresh[Alt_Layer_Value];
+}
+
+int Inhibit_Biased_Climb ()
+{
+    return (Climb_Inhibit ? Up_Separation + NOZCROSS : Up_Separation);
+}
+
+bool Non_Crossing_Biased_Climb()
+{
+    int upward_preferred;
+    int upward_crossing_situation;
+    bool result;
+
+    upward_preferred = Inhibit_Biased_Climb() > Down_Separation;
+    if (upward_preferred)
+    {
+	result = !(Own_Below_Threat()) || ((Own_Below_Threat()) && (!(Down_Separation >= ALIM())));
+    }
+    else
+    {	
+	result = Own_Above_Threat() && (Cur_Vertical_Sep >= MINSEP) && (Up_Separation >= ALIM());
+    }
+    return result;
+}
+
+bool Non_Crossing_Biased_Descend()
+{
+    int upward_preferred;
+    int upward_crossing_situation;
+    bool result;
+
+    upward_preferred = (Up_Separation + NOZCROSS) > Down_Separation;
+    if (upward_preferred)
+    {
+	result = Own_Below_Threat() && (Cur_Vertical_Sep >= MINSEP) && (Down_Separation >= ALIM());
+    }
+    else
+    {
+	result = !(Own_Above_Threat()) || ((Own_Above_Threat()) && (Up_Separation >= ALIM()));
+    }
+    return result;
+}
+
+bool Own_Below_Threat()
+{
+    return (Own_Tracked_Alt < Other_Tracked_Alt);
+}
+
+bool Own_Above_Threat()
+{
+    return (Other_Tracked_Alt < Own_Tracked_Alt);
+}
+
+int alt_sep_test()
+{
+    bool enabled, tcas_equipped, intent_not_known;
+    bool need_upward_RA, need_downward_RA;
+    int alt_sep;
+
+    enabled = High_Confidence && (Own_Tracked_Alt_Rate <= OLEV) && (Cur_Vertical_Sep > MAXALTDIFF);
+    tcas_equipped = Other_Capability == TCAS_TA;
+    intent_not_known = Two_of_Three_Reports_Valid && Other_RAC == NO_INTENT;
+    
+    alt_sep = UNRESOLVED;
+    
+    if (enabled && ((tcas_equipped && intent_not_known) || !tcas_equipped))
+    {
+	need_upward_RA = Non_Crossing_Biased_Climb() && Own_Below_Threat();
+	need_downward_RA = Non_Crossing_Biased_Descend() && Own_Above_Threat();
+	if (need_upward_RA && need_downward_RA)
+        /* unreachable: requires Own_Below_Threat and Own_Above_Threat
+           to both be true - that requires Own_Tracked_Alt < Other_Tracked_Alt
+           and Other_Tracked_Alt < Own_Tracked_Alt, which isn't possible */
+	    alt_sep = UNRESOLVED;
+	else if (need_upward_RA)
+	    alt_sep = UPWARD_RA;
+	else if (need_downward_RA)
+	    alt_sep = DOWNWARD_RA;
+	else
+	    alt_sep = UNRESOLVED;
+    }
+    
+    return alt_sep;
+}
+
+main(int argc, char*argv[])
+{
+
+  initialize();
+  Cur_Vertical_Sep =  860; 
+  High_Confidence = 1; 
+  Two_of_Three_Reports_Valid = 1; 
+  Own_Tracked_Alt =  618; 
+  Own_Tracked_Alt_Rate =  329; 
+  Other_Tracked_Alt =  574; 
+  Alt_Layer_Value =  4; 
+  Up_Separation =  893; 
+  Down_Separation =  914; 
+  Other_RAC =  0; 
+  Other_Capability =  2; 
+  Climb_Inhibit =  0; 
+  assert(alt_sep_test()==0);
+}
diff --git a/regression/cbmc-with-incr/Float-div1/main.c b/regression/cbmc-with-incr/Float-div1/main.c
index dee31965dac..63f8512a7c2 100644
--- a/regression/cbmc-with-incr/Float-div1/main.c
+++ b/regression/cbmc-with-incr/Float-div1/main.c
@@ -1,50 +1,50 @@
-#include <assert.h>
-#include <math.h>
-
-#ifdef __GNUC__
-void inductiveStepHunt (float startState)
-{
-  float target = 0x1.fffffep-3f;
-
-  __CPROVER_assume((0 < startState) && (fpclassify(startState) == FP_NORMAL) && (0x1p-126f <= startState));
-
-  float secondPoint = (target / startState);
-
-  float nextState = (startState + secondPoint) / 2;
-
-  float oneAfter = (target / nextState);
-
-  assert(oneAfter > 0);
-}
-
-void simplifiedInductiveStepHunt (float nextState)
-{
-  float target = 0x1.fffffep-3f;
-
-  // Implies nextState == 0x1p+124f;
-  __CPROVER_assume((0x1.fffffep+123f < nextState) && (nextState < 0x1.000002p+124f));
-  
-  float oneAfter = (target / nextState);
-
-  // Is true and correctly proven by constant evaluation
-  // Note that this is the smallest normal number
-  assert(0x1.fffffep-3f / 0x1p+124f == 0x1p-126f);
-
-  assert(oneAfter > 0);
-}
-#endif
-
-int main (void)
-{
-  #ifdef __GNUC__
-  //  inductiveStepHunt(0x1p+125f);
-  //  simplifiedInductiveStepHunt(0x1p+124f);
-
-  float f, g;
-
-  inductiveStepHunt(f);
-  simplifiedInductiveStepHunt(g);
-  #endif
-
-  return 0;
-}
+#include <assert.h>
+#include <math.h>
+
+#ifdef __GNUC__
+void inductiveStepHunt (float startState)
+{
+  float target = 0x1.fffffep-3f;
+
+  __CPROVER_assume((0 < startState) && (fpclassify(startState) == FP_NORMAL) && (0x1p-126f <= startState));
+
+  float secondPoint = (target / startState);
+
+  float nextState = (startState + secondPoint) / 2;
+
+  float oneAfter = (target / nextState);
+
+  assert(oneAfter > 0);
+}
+
+void simplifiedInductiveStepHunt (float nextState)
+{
+  float target = 0x1.fffffep-3f;
+
+  // Implies nextState == 0x1p+124f;
+  __CPROVER_assume((0x1.fffffep+123f < nextState) && (nextState < 0x1.000002p+124f));
+  
+  float oneAfter = (target / nextState);
+
+  // Is true and correctly proven by constant evaluation
+  // Note that this is the smallest normal number
+  assert(0x1.fffffep-3f / 0x1p+124f == 0x1p-126f);
+
+  assert(oneAfter > 0);
+}
+#endif
+
+int main (void)
+{
+  #ifdef __GNUC__
+  //  inductiveStepHunt(0x1p+125f);
+  //  simplifiedInductiveStepHunt(0x1p+124f);
+
+  float f, g;
+
+  inductiveStepHunt(f);
+  simplifiedInductiveStepHunt(g);
+  #endif
+
+  return 0;
+}
diff --git a/regression/cbmc-with-incr/Float-to-double2/main.c b/regression/cbmc-with-incr/Float-to-double2/main.c
index 43ab0927eab..2db129fd08f 100644
--- a/regression/cbmc-with-incr/Float-to-double2/main.c
+++ b/regression/cbmc-with-incr/Float-to-double2/main.c
@@ -1,12 +1,12 @@
-#include <assert.h>
-
-int main(void)
-{
-  float f   = -0x1.0p-127f;
-  double d  = -0x1.0p-127;
-  double fp = (double)f;
-
-  assert(d == fp);
-
-  return 0;
-}
+#include <assert.h>
+
+int main(void)
+{
+  float f   = -0x1.0p-127f;
+  double d  = -0x1.0p-127;
+  double fp = (double)f;
+
+  assert(d == fp);
+
+  return 0;
+}
diff --git a/regression/cbmc-with-incr/Float19/main.c b/regression/cbmc-with-incr/Float19/main.c
index bc09c89924d..56b5548c602 100644
--- a/regression/cbmc-with-incr/Float19/main.c
+++ b/regression/cbmc-with-incr/Float19/main.c
@@ -1,24 +1,24 @@
-#include <assert.h>
-#include <math.h>
-
-#ifdef __GNUC__
-
-void f00 (float f)
-{
-  if (f > 0x1.FFFFFEp+127) {
-    assert(isinf(f));
-  }
-}
-
-#endif
-
-int main (void)
-{
-  #ifdef __GNUC__
-  float f;
-
-  f00(f);
-  #endif
-
-  return 0;
-}
+#include <assert.h>
+#include <math.h>
+
+#ifdef __GNUC__
+
+void f00 (float f)
+{
+  if (f > 0x1.FFFFFEp+127) {
+    assert(isinf(f));
+  }
+}
+
+#endif
+
+int main (void)
+{
+  #ifdef __GNUC__
+  float f;
+
+  f00(f);
+  #endif
+
+  return 0;
+}
diff --git a/regression/cbmc-with-incr/Float20/main.c b/regression/cbmc-with-incr/Float20/main.c
index dfacc8bac6d..b730f0d4f18 100644
--- a/regression/cbmc-with-incr/Float20/main.c
+++ b/regression/cbmc-with-incr/Float20/main.c
@@ -1,56 +1,56 @@
-/*
-** float-rounder-bug.c
-**
-** Martin Brain
-** martin.brain@cs.ox.ac.uk
-** 20/05/13
-**
-** Another manifestation of the casting bug.
-** If the number is in (0,0x1p-126) it is rounded to zero rather than a subnormal number.
-*/
-#define FULP 1
-
-void bug (float min) {
-  __CPROVER_assume(min == 0x1.fffffep-105f);
-  float modifier = (0x1.0p-23 * (1<<FULP));
-  float ulpdiff = min * modifier;
-
-  assert(ulpdiff == 0x1p-126f);    // Should be true
-
-  return;
-}
-
-void bugBrokenOut (float min) {
-  __CPROVER_assume(min == 0x1.fffffep-105f);
-  float modifier = (0x1.0p-23 * (1<<FULP));
-  double dulpdiff = (double)min * (double)modifier;  // Fine up to here
-  float ulpdiff = (float)dulpdiff;  // Error
-
-  assert(ulpdiff == 0x1p-126f); // Should be true
-
-  return;
-}
-
-void bugCasting (double d) {
-  __CPROVER_assume(d == 0x1.fffffep-127);
-
-  float f = (float) d;
-
-  assert(f == 0x1p-126f); // Should be true
-
-  return;
-}
-
-int main (void) {
-  float f;
-  bug(f);
-
-  float g;
-  bugBrokenOut(g);
-
-  double d;
-  bugCasting(d);
-
-  return 1;
-}
-
+/*
+** float-rounder-bug.c
+**
+** Martin Brain
+** martin.brain@cs.ox.ac.uk
+** 20/05/13
+**
+** Another manifestation of the casting bug.
+** If the number is in (0,0x1p-126) it is rounded to zero rather than a subnormal number.
+*/
+#define FULP 1
+
+void bug (float min) {
+  __CPROVER_assume(min == 0x1.fffffep-105f);
+  float modifier = (0x1.0p-23 * (1<<FULP));
+  float ulpdiff = min * modifier;
+
+  assert(ulpdiff == 0x1p-126f);    // Should be true
+
+  return;
+}
+
+void bugBrokenOut (float min) {
+  __CPROVER_assume(min == 0x1.fffffep-105f);
+  float modifier = (0x1.0p-23 * (1<<FULP));
+  double dulpdiff = (double)min * (double)modifier;  // Fine up to here
+  float ulpdiff = (float)dulpdiff;  // Error
+
+  assert(ulpdiff == 0x1p-126f); // Should be true
+
+  return;
+}
+
+void bugCasting (double d) {
+  __CPROVER_assume(d == 0x1.fffffep-127);
+
+  float f = (float) d;
+
+  assert(f == 0x1p-126f); // Should be true
+
+  return;
+}
+
+int main (void) {
+  float f;
+  bug(f);
+
+  float g;
+  bugBrokenOut(g);
+
+  double d;
+  bugCasting(d);
+
+  return 1;
+}
+
diff --git a/regression/cbmc-with-incr/Float21/main.c b/regression/cbmc-with-incr/Float21/main.c
index e01c31684a7..883e066cdfc 100644
--- a/regression/cbmc-with-incr/Float21/main.c
+++ b/regression/cbmc-with-incr/Float21/main.c
@@ -1,66 +1,66 @@
-/*
-** subnormal-boundary.c
-**
-** Martin Brain
-** martin.brain@cs.ox.ac.uk
-** 25/07/12
-**
-** Regression tests for casting and classification around the subnormal boundary.
-**
-*/
-
-#include <assert.h>
-#include <math.h>
-
-float nondet_float(void);
-
-int main (void)
-{
-  #ifdef __GNUC__
-
-  float smallestNormalFloat = 0x1.0p-126f;
-  float largestSubnormalFloat = 0x1.fffffcp-127f;
-  
-  double v = 0x1.FFFFFFp-127;
-
-  float f;
-
-
-  // Check the encodings are correct
-  assert(fpclassify(largestSubnormalFloat) == FP_SUBNORMAL);
-
-  f = nondet_float();
-  __CPROVER_assume(fpclassify(f) == FP_SUBNORMAL);
-  assert(f <= largestSubnormalFloat);
-
-
-  assert(fpclassify(smallestNormalFloat) == FP_NORMAL);
-
-  f = nondet_float();
-  __CPROVER_assume(fpclassify(f) == FP_NORMAL);
-  assert(smallestNormalFloat <= fabs(f));
-
-  assert(largestSubnormalFloat < smallestNormalFloat);
-
-
-  // Check the ordering as doubles
-  assert(((double)largestSubnormalFloat) < ((double)smallestNormalFloat));
-  assert(((double)largestSubnormalFloat) < v);
-  assert(v < ((double)smallestNormalFloat));
-
-
-  // Check coercion to float
-  assert((float)((double)largestSubnormalFloat) == largestSubnormalFloat);
-  assert((float)((double)smallestNormalFloat) == smallestNormalFloat);
-
-  assert(((double)smallestNormalFloat) - v <= v - ((double)largestSubnormalFloat));
-  assert(((float)v) == smallestNormalFloat);
-
-  f = nondet_float();
-  __CPROVER_assume(fpclassify(f) == FP_SUBNORMAL);
-  assert( ((float)((double)f)) == f );
-  
-  #endif
-
-  return 0;
-}
+/*
+** subnormal-boundary.c
+**
+** Martin Brain
+** martin.brain@cs.ox.ac.uk
+** 25/07/12
+**
+** Regression tests for casting and classification around the subnormal boundary.
+**
+*/
+
+#include <assert.h>
+#include <math.h>
+
+float nondet_float(void);
+
+int main (void)
+{
+  #ifdef __GNUC__
+
+  float smallestNormalFloat = 0x1.0p-126f;
+  float largestSubnormalFloat = 0x1.fffffcp-127f;
+  
+  double v = 0x1.FFFFFFp-127;
+
+  float f;
+
+
+  // Check the encodings are correct
+  assert(fpclassify(largestSubnormalFloat) == FP_SUBNORMAL);
+
+  f = nondet_float();
+  __CPROVER_assume(fpclassify(f) == FP_SUBNORMAL);
+  assert(f <= largestSubnormalFloat);
+
+
+  assert(fpclassify(smallestNormalFloat) == FP_NORMAL);
+
+  f = nondet_float();
+  __CPROVER_assume(fpclassify(f) == FP_NORMAL);
+  assert(smallestNormalFloat <= fabs(f));
+
+  assert(largestSubnormalFloat < smallestNormalFloat);
+
+
+  // Check the ordering as doubles
+  assert(((double)largestSubnormalFloat) < ((double)smallestNormalFloat));
+  assert(((double)largestSubnormalFloat) < v);
+  assert(v < ((double)smallestNormalFloat));
+
+
+  // Check coercion to float
+  assert((float)((double)largestSubnormalFloat) == largestSubnormalFloat);
+  assert((float)((double)smallestNormalFloat) == smallestNormalFloat);
+
+  assert(((double)smallestNormalFloat) - v <= v - ((double)largestSubnormalFloat));
+  assert(((float)v) == smallestNormalFloat);
+
+  f = nondet_float();
+  __CPROVER_assume(fpclassify(f) == FP_SUBNORMAL);
+  assert( ((float)((double)f)) == f );
+  
+  #endif
+
+  return 0;
+}
diff --git a/regression/cbmc-with-incr/Recursion4/main.c b/regression/cbmc-with-incr/Recursion4/main.c
index 00198d60574..c2cc4c13ae1 100644
--- a/regression/cbmc-with-incr/Recursion4/main.c
+++ b/regression/cbmc-with-incr/Recursion4/main.c
@@ -1,17 +1,17 @@
-int factorial2(int i)
-{
-  if(i==0) return 1;
-
-  // tmp_result gets renamed during recursion!
-  int tmp_result;
-  tmp_result=factorial2(0);
-  return tmp_result;
-}
-
-int main()
-{
-  int result_factorial;
-  result_factorial=factorial2(1);
-  assert(result_factorial==1);
-  return 0;
-}
+int factorial2(int i)
+{
+  if(i==0) return 1;
+
+  // tmp_result gets renamed during recursion!
+  int tmp_result;
+  tmp_result=factorial2(0);
+  return tmp_result;
+}
+
+int main()
+{
+  int result_factorial;
+  result_factorial=factorial2(1);
+  assert(result_factorial==1);
+  return 0;
+}
diff --git a/regression/cpp-from-CVS/Array1/main.cpp b/regression/cpp-from-CVS/Array1/main.cpp
index 8c77e5c8f89..ba02b972c16 100644
--- a/regression/cpp-from-CVS/Array1/main.cpp
+++ b/regression/cpp-from-CVS/Array1/main.cpp
@@ -1,11 +1,11 @@
-int y[5][4][3][2];
-
-int main()
-{
-  for(int i=0; i<5; i++)
-    for(int j=0; j<4; j++)
-      for(int k=0; k<3; k++)
-        for(int l=0; l<2; l++)
-          y[i][j][k][l]=2;
-}
-
+int y[5][4][3][2];
+
+int main()
+{
+  for(int i=0; i<5; i++)
+    for(int j=0; j<4; j++)
+      for(int k=0; k<3; k++)
+        for(int l=0; l<2; l++)
+          y[i][j][k][l]=2;
+}
+
diff --git a/regression/cpp-from-CVS/Array2/main.cpp b/regression/cpp-from-CVS/Array2/main.cpp
index 5359e4e8149..0e3e35b8ad3 100644
--- a/regression/cpp-from-CVS/Array2/main.cpp
+++ b/regression/cpp-from-CVS/Array2/main.cpp
@@ -1,11 +1,11 @@
-int y[2][3][4][5];
-
-int main()
-{
-  for(int i=0; i<5; i++)
-    for(int j=0; j<4; j++)
-      for(int k=0; k<3; k++)
-        for(int l=0; l<2; l++)
-          y[i][j][k][l]=2; // out-of-bounds
-}
-
+int y[2][3][4][5];
+
+int main()
+{
+  for(int i=0; i<5; i++)
+    for(int j=0; j<4; j++)
+      for(int k=0; k<3; k++)
+        for(int l=0; l<2; l++)
+          y[i][j][k][l]=2; // out-of-bounds
+}
+
diff --git a/regression/cpp/Decltype2/main.cpp b/regression/cpp/Decltype2/main.cpp
index f315130f21a..ba26a736059 100644
--- a/regression/cpp/Decltype2/main.cpp
+++ b/regression/cpp/Decltype2/main.cpp
@@ -1,14 +1,14 @@
-// C++11
-// decltype is a C++11 feature to get the "declared type" of an expression.
-// It is similar to 'typeof' but handles reference types "properly".
-
-class base {};
-class derived : public base {};
-
-derived d;
-
-decltype(static_cast<derived *>(&d)) z;
-
-int main()
-{
-}
+// C++11
+// decltype is a C++11 feature to get the "declared type" of an expression.
+// It is similar to 'typeof' but handles reference types "properly".
+
+class base {};
+class derived : public base {};
+
+derived d;
+
+decltype(static_cast<derived *>(&d)) z;
+
+int main()
+{
+}
diff --git a/regression/cpp/Decltype3/main.cpp b/regression/cpp/Decltype3/main.cpp
index 0ded9d5c44f..e0a95f38b00 100644
--- a/regression/cpp/Decltype3/main.cpp
+++ b/regression/cpp/Decltype3/main.cpp
@@ -1,18 +1,18 @@
-// C++11
-// decltype is a C++11 feature to get the "declared type" of an expression.
-// It is similar to 'typeof' but handles reference types "properly".
-
-template <class A, class B>
-struct whatever {
-	int f00 (const B b) {
-		typedef	decltype(static_cast<A>(b)) T;
-		T z;
-		return 1;
-	}
-};
-
-whatever<int,float> thing;
-
-int main()
-{
-}
+// C++11
+// decltype is a C++11 feature to get the "declared type" of an expression.
+// It is similar to 'typeof' but handles reference types "properly".
+
+template <class A, class B>
+struct whatever {
+	int f00 (const B b) {
+		typedef	decltype(static_cast<A>(b)) T;
+		T z;
+		return 1;
+	}
+};
+
+whatever<int,float> thing;
+
+int main()
+{
+}

From cb6c188c1bfa9bf812da590c571e0e36333cad99 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sat, 22 Oct 2016 18:07:28 +0100
Subject: [PATCH 2/3] check all properties if multiple --property p options
 present on command line

---
 regression/cbmc/Multiple_Properties1/main.c    | 14 ++++++++++++++
 regression/cbmc/Multiple_Properties1/test.desc | 10 ++++++++++
 src/cbmc/cbmc_parse_options.cpp                |  4 +---
 3 files changed, 25 insertions(+), 3 deletions(-)
 create mode 100644 regression/cbmc/Multiple_Properties1/main.c
 create mode 100644 regression/cbmc/Multiple_Properties1/test.desc

diff --git a/regression/cbmc/Multiple_Properties1/main.c b/regression/cbmc/Multiple_Properties1/main.c
new file mode 100644
index 00000000000..633ee3adb15
--- /dev/null
+++ b/regression/cbmc/Multiple_Properties1/main.c
@@ -0,0 +1,14 @@
+int main () {
+  int x, y;
+  __CPROVER_assume(x>=100 && y<=1000 & x>y+2);
+  x--;
+  assert(x>y);  
+  x--;
+  assert(x>y);  
+  x--;
+  assert(x>y);  
+  y=0;
+  assert(x>y);  
+
+  return 0;
+}
diff --git a/regression/cbmc/Multiple_Properties1/test.desc b/regression/cbmc/Multiple_Properties1/test.desc
new file mode 100644
index 00000000000..1c7d5d0087c
--- /dev/null
+++ b/regression/cbmc/Multiple_Properties1/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--property main.assertion.1 --property main.assertion.3
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED
+^.*main.assertion.1.*SUCCESS
+^.*main.assertion.3.*FAILURE
+--
+^warning: ignoring
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 3b0d7b5bc6a..f898c639779 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -181,7 +181,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("simplify", true);
 
   if(cmdline.isset("stop-on-fail") ||
-     cmdline.isset("property") ||
      cmdline.isset("dimacs") ||
      cmdline.isset("outfile"))
     options.set_option("stop-on-fail", true);
@@ -189,8 +188,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("stop-on-fail", false);
 
   if(cmdline.isset("trace") ||
-     cmdline.isset("stop-on-fail") ||
-     cmdline.isset("property"))
+     cmdline.isset("stop-on-fail"))
     options.set_option("trace", true);
 
   if(cmdline.isset("localize-faults"))

From cdd7ac6e305e8c15db28b890107d9af1f896cb33 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sat, 22 Oct 2016 18:10:25 +0100
Subject: [PATCH 3/3] allow comma-separated list of properties with --property
 option

---
 regression/cbmc/Multiple_Properties2/main.c   | 14 ++++++++
 .../cbmc/Multiple_Properties2/test.desc       | 11 +++++++
 regression/cbmc/Multiple_Properties3/main.c   | 14 ++++++++
 .../cbmc/Multiple_Properties3/test.desc       |  9 ++++++
 src/cbmc/cbmc_parse_options.cpp               |  6 ++--
 src/util/cmdline.cpp                          | 32 +++++++++++++++++++
 src/util/cmdline.h                            |  2 ++
 7 files changed, 86 insertions(+), 2 deletions(-)
 create mode 100644 regression/cbmc/Multiple_Properties2/main.c
 create mode 100644 regression/cbmc/Multiple_Properties2/test.desc
 create mode 100644 regression/cbmc/Multiple_Properties3/main.c
 create mode 100644 regression/cbmc/Multiple_Properties3/test.desc

diff --git a/regression/cbmc/Multiple_Properties2/main.c b/regression/cbmc/Multiple_Properties2/main.c
new file mode 100644
index 00000000000..633ee3adb15
--- /dev/null
+++ b/regression/cbmc/Multiple_Properties2/main.c
@@ -0,0 +1,14 @@
+int main () {
+  int x, y;
+  __CPROVER_assume(x>=100 && y<=1000 & x>y+2);
+  x--;
+  assert(x>y);  
+  x--;
+  assert(x>y);  
+  x--;
+  assert(x>y);  
+  y=0;
+  assert(x>y);  
+
+  return 0;
+}
diff --git a/regression/cbmc/Multiple_Properties2/test.desc b/regression/cbmc/Multiple_Properties2/test.desc
new file mode 100644
index 00000000000..79353b53632
--- /dev/null
+++ b/regression/cbmc/Multiple_Properties2/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--property main.assertion.1,main.assertion.3,main.assertion.4
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED
+^.*main.assertion.1.*SUCCESS
+^.*main.assertion.3.*FAILURE
+^.*main.assertion.4.*SUCCESS
+--
+^warning: ignoring
diff --git a/regression/cbmc/Multiple_Properties3/main.c b/regression/cbmc/Multiple_Properties3/main.c
new file mode 100644
index 00000000000..633ee3adb15
--- /dev/null
+++ b/regression/cbmc/Multiple_Properties3/main.c
@@ -0,0 +1,14 @@
+int main () {
+  int x, y;
+  __CPROVER_assume(x>=100 && y<=1000 & x>y+2);
+  x--;
+  assert(x>y);  
+  x--;
+  assert(x>y);  
+  x--;
+  assert(x>y);  
+  y=0;
+  assert(x>y);  
+
+  return 0;
+}
diff --git a/regression/cbmc/Multiple_Properties3/test.desc b/regression/cbmc/Multiple_Properties3/test.desc
new file mode 100644
index 00000000000..4f3b8d71e8f
--- /dev/null
+++ b/regression/cbmc/Multiple_Properties3/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--property main.assertion.3
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED
+^.*main.assertion.3.*FAILURE
+--
+^warning: ignoring
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index f898c639779..6b46b941b02 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -593,10 +593,12 @@ bool cbmc_parse_optionst::set_properties(goto_functionst &goto_functions)
   try
   {
     if(cmdline.isset("claim")) // will go away
-      ::set_properties(goto_functions, cmdline.get_values("claim"));
+      ::set_properties(goto_functions, 
+                       cmdline.get_comma_separated_values("claim"));
 
     if(cmdline.isset("property")) // use this one
-      ::set_properties(goto_functions, cmdline.get_values("property"));
+      ::set_properties(goto_functions, 
+                       cmdline.get_comma_separated_values("property"));
   }
 
   catch(const char *e)
diff --git a/src/util/cmdline.cpp b/src/util/cmdline.cpp
index e2ce9575795..bb315f4ecd3 100644
--- a/src/util/cmdline.cpp
+++ b/src/util/cmdline.cpp
@@ -220,6 +220,38 @@ const std::list<std::string>& cmdlinet::get_values(const std::string &option) co
 
 /*******************************************************************\
 
+Function: cmdlinet::get_comma_separated_values
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+const std::list<std::string> cmdlinet::get_comma_separated_values(
+  const std::string &option) const
+{
+  int i=getoptnr(option);
+  assert(i>=0);
+  std::list<std::string> values;
+  for(const auto &value : options[i].values)
+  {
+    std::string::size_type length=value.length();
+    for(std::string::size_type idx=0; idx<length; idx++)
+    {
+      std::string::size_type next=value.find(",", idx);
+      values.push_back(value.substr(idx, next-idx));
+      if(next==std::string::npos) break;
+      idx=next;
+    }
+  }
+  return values;
+}
+
+/*******************************************************************\
+
 Function: cmdlinet::getoptnr
 
   Inputs:
diff --git a/src/util/cmdline.h b/src/util/cmdline.h
index f249c79bc87..a6338db6ea6 100644
--- a/src/util/cmdline.h
+++ b/src/util/cmdline.h
@@ -23,6 +23,8 @@ class cmdlinet
 
   const std::list<std::string> &get_values(const std::string &option) const;
   const std::list<std::string> &get_values(char option) const;
+  const std::list<std::string> get_comma_separated_values(
+    const std::string &option) const;
 
   virtual bool isset(char option) const;
   virtual bool isset(const char *option) const;