check all properties if multiple --property p options present on command line

Author: peterschrammel

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;
+}

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

src/cbmc/cbmc_parse_options.cpp

@@ -181,16 +181,14 @@ 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);
   else
     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"))