Allow specify cbmc args in goto-synthesizer regression tests

Author: qinheping

regression/goto-synthesizer/chain.sh

@@ -12,13 +12,20 @@ name=${*:$#}
 name=${name%.c}
 
 args=${*:6:$#-6}
-if [[ "$args" != *" _ "* ]]
-then
+if [[ "$args" != *" _ "* ]]; then
   args_inst=$args
   args_synthesizer=""
+  args_cbmc=""
 else
   args_inst="${args%%" _ "*}"
-  args_synthesizer="${args#*" _ "}"
+  args=${args#*" _ "}
+  if [[ "$args" != *" _ "* ]]; then
+    args_synthesizer=$args
+    args_cbmc=""
+  else
+    args_synthesizer="${args%%" _ "*}"
+    args_cbmc="${args#*" _ "}"
+  fi
 fi
 
 if [[ "${is_windows}" == "true" ]]; then
@@ -50,5 +57,5 @@ if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then
 else
   $goto_synthesizer ${args_synthesizer} "${name}-mod.gb" "${name}-mod-2.gb"
   echo "Running CBMC: "
-  $cbmc "${name}-mod-2.gb"
+  $cbmc ${args_cbmc} "${name}-mod-2.gb"
 fi