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/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 3b0d7b5bc6a..6b46b941b02 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"))
@@ -595,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;