Add parse option --show-array-constraints to track array constraints added during post processing

Array theory constraints added during post processing might be useful to reason
about proof runtimes. This commit adds a new parse option --show-array-constraints
that tracks constraints pertaining to arrays added during post processing.

fix command line argument to display error message of xml or plain format is used

Author: Natasha Yogananda Jeppu

src/cbmc/cbmc_parse_options.cpp

@@ -566,6 +566,17 @@ int cbmc_parse_optionst::doit()
     return CPROVER_EXIT_USAGE_ERROR;
   }
 
+  if(cmdline.isset("show-array-constraints"))
+  {
+    if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
+    {
+      log.error() << "--show-array-constraints supports only"
+                     " json output. Use --json-ui."
+                  << messaget::eom;
+      return CPROVER_EXIT_USAGE_ERROR;
+    }
+  }
+
   register_languages();
 
   // configure gcc, if required
@@ -1145,6 +1156,8 @@ void cbmc_parse_optionst::help()
     " --write-solver-stats-to json-file\n"
     "                              collect the solver query complexity\n"
     " --show-array-constraints     show array theory constraints added\n"
+    "                              during post processing.\n"
+    "                              Requires --json-ui.\n"
     "\n";
   // clang-format on
 }