diff --git a/doc/man/goto-synthesizer.1 b/doc/man/goto-synthesizer.1
index 0c304850a0c..346be77c35a 100644
--- a/doc/man/goto-synthesizer.1
+++ b/doc/man/goto-synthesizer.1
@@ -18,13 +18,17 @@ resulting program as GOTO binary on disk.
 .SH OPTIONS
 .TP
 \fB\-loop\-contracts\-no\-unwind\fR
-Do not unwind transformed loops after applying the synthesized loop contracts.
+do not unwind transformed loops after applying the synthesized loop contracts
 .TP
 \fB\-\-dump\-loop\-contracts
-Dump the synthesized loop contracts as JSON.
+dump the synthesized loop contracts as JSON
 .TP
 \fB\-\-json-\output\fR \fIfile\fR
-Specify the output destination of the loop-contracts JSON.
+specify the output destination of the loop-contracts JSON
+.SS "Backend options:"
+.TP
+\fB\-\-object\-bits\fR n
+number of bits used for object addresses
 .SS "User-interface options:"
 .TP
 \fB\-\-xml\-ui\fR
diff --git a/regression/goto-synthesizer/address_space_size_limit/main.c b/regression/goto-synthesizer/address_space_size_limit/main.c
new file mode 100644
index 00000000000..4b0e6276dbb
--- /dev/null
+++ b/regression/goto-synthesizer/address_space_size_limit/main.c
@@ -0,0 +1,20 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int i;
+  char *a;
+  char *b;
+  char *c;
+  a = (char *)malloc(1);
+  b = (char *)malloc(1);
+  c = (char *)malloc(1);
+  for(i = 0; i < 5; ++i)
+  {
+    *a = 0;
+    *b = 0;
+    *c = 0;
+  }
+  assert(*c + *b + *c == 1);
+}
diff --git a/regression/goto-synthesizer/address_space_size_limit/test.desc b/regression/goto-synthesizer/address_space_size_limit/test.desc
new file mode 100644
index 00000000000..7bfcdf8d662
--- /dev/null
+++ b/regression/goto-synthesizer/address_space_size_limit/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check _ --object-bits 1
+too many addressed objects
+^EXIT=6$
+^SIGNAL=0$
+--
+Check if the synthesizer can correctly set object bits when calling CBMC.
diff --git a/regression/goto-synthesizer/chain.sh b/regression/goto-synthesizer/chain.sh
index fdf9e6288eb..b96966a5b95 100755
--- a/regression/goto-synthesizer/chain.sh
+++ b/regression/goto-synthesizer/chain.sh
@@ -48,7 +48,7 @@ echo "Running goto-synthesizer: "
 if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then
   $goto_synthesizer ${args_synthesizer} "${name}-mod.gb"
 else
-  $goto_synthesizer "${name}-mod.gb" "${name}-mod-2.gb"
+  $goto_synthesizer ${args_synthesizer} "${name}-mod.gb" "${name}-mod-2.gb"
   echo "Running CBMC: "
   $cbmc "${name}-mod-2.gb"
 fi
diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp
index 436dacc4066..a4c19ae77b3 100644
--- a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp
+++ b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp
@@ -8,7 +8,6 @@ Author: Qinheping Hu
 
 #include "goto_synthesizer_parse_options.h"
 
-#include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/version.h>
 
@@ -196,6 +195,9 @@ void goto_synthesizer_parse_optionst::help()
     HELP_DUMP_LOOP_CONTRACTS
     HELP_LOOP_CONTRACTS_NO_UNWIND
     "\n"
+    "Backend options:\n"
+    HELP_CONFIG_BACKEND
+    "\n"
     "Other options:\n"
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.h b/src/goto-synthesizer/goto_synthesizer_parse_options.h
index 214b99263a2..c9dc3817b0c 100644
--- a/src/goto-synthesizer/goto_synthesizer_parse_options.h
+++ b/src/goto-synthesizer/goto_synthesizer_parse_options.h
@@ -9,6 +9,7 @@ Author: Qinheping Hu
 #ifndef CPROVER_GOTO_SYNTHESIZER_GOTO_SYNTHESIZER_PARSE_OPTIONS_H
 #define CPROVER_GOTO_SYNTHESIZER_GOTO_SYNTHESIZER_PARSE_OPTIONS_H
 
+#include <util/config.h>
 #include <util/parse_options.h>
 
 #include <goto-programs/goto_model.h>
@@ -21,6 +22,7 @@ Author: Qinheping Hu
 #define GOTO_SYNTHESIZER_OPTIONS \
   OPT_DUMP_LOOP_CONTRACTS \
   "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \
+  OPT_CONFIG_BACKEND \
   "(verbosity):(version)(xml-ui)(json-ui)" \
   // empty last line