diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml
index 341a8d15a18..2e3cd2289f2 100644
--- a/.github/workflows/pull-request-checks.yaml
+++ b/.github/workflows/pull-request-checks.yaml
@@ -69,10 +69,24 @@ jobs:
           make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss
       - name: Run regression tests
         run: |
-          make -C regression test-parallel JOBS=2
+          make -C regression test-parallel JOBS=2 LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
           make -C regression/cbmc test-paths-lifo
           env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
           make -C jbmc/regression test-parallel JOBS=2
+      - name: Check cleanup
+        run: |
+          make -C src clean IPASIR=$PWD/riss.git/riss
+          make -C jbmc/src clean IPASIR=$PWD/riss.git/riss
+          rm -r riss.git
+          rm src/goto-cc/goto-ld
+          make -C unit clean
+          make -C regression clean
+          make -C jbmc/unit clean
+          make -C jbmc/regression clean
+          if [[ $(git status --ignored --porcelain | grep -v .ccache/) ]] ; then
+            git status --ignored
+            exit 1
+          fi
 
   # This job takes approximately 25 to 34 minutes
   check-ubuntu-20_04-make-clang:
@@ -241,6 +255,17 @@ jobs:
           ls *.deb
       - name: Run tests
         run: cd build; ctest . -V -L CORE -j2
+      - name: Check cleanup
+        run: |
+          rm -r build
+          rm scripts/bash-autocomplete/cbmc.sh
+          make -C unit clean
+          make -C regression clean
+          make -C jbmc/regression clean
+          if [[ $(git status --ignored --porcelain | grep -v .ccache/) ]] ; then
+            git status --ignored
+            exit 1
+          fi
 
   # This job takes approximately 34 to 38 minutes
   check-ubuntu-22_04-make-clang:
diff --git a/regression/Makefile b/regression/Makefile
index 8a3c7350de4..daee836f505 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -30,6 +30,9 @@ DIRS = cbmc-shadow-memory \
        goto-diff \
        test-script \
        goto-analyzer-taint \
+       goto-bmc/goto-bmc-symex-ready-goto \
+       goto-bmc/goto-bmc-non-symex-ready-goto \
+       goto-bmc \
        goto-gcc \
        goto-cl \
        goto-cc-cbmc \
@@ -59,6 +62,7 @@ DIRS = cbmc-shadow-memory \
        cbmc-sequentialization \
        cpp-linter \
        catch-framework \
+       libcprover-cpp \
        # Empty last line
 
 ifeq ($(OS),Windows_NT)
@@ -110,9 +114,7 @@ test-parallel:
 
 .PHONY: clean
 clean:
-	@for dir in *; do \
-		if [ -d "$$dir" ]; then \
-			$(MAKE) -C "$$dir" clean; \
-		fi; \
+	@for dir in $(DIRS); do \
+		$(MAKE) -C "$$dir" clean; \
 	done;
 	$(RM) tests.log
diff --git a/regression/ansi-c/Makefile b/regression/ansi-c/Makefile
index c33acea9afb..ba16308dca6 100644
--- a/regression/ansi-c/Makefile
+++ b/regression/ansi-c/Makefile
@@ -64,4 +64,4 @@ build_goto_binaries:
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
 	find . -name '*.gb' -execdir $(RM) '{}' \;
-	$(RM) tests.log tests-c++-front-end.log
+	$(RM) tests*.log
diff --git a/regression/catch-framework/Makefile b/regression/catch-framework/Makefile
index 8b4ad5cfda4..01c98b1bf97 100644
--- a/regression/catch-framework/Makefile
+++ b/regression/catch-framework/Makefile
@@ -6,4 +6,5 @@ test:
 tests.log: ../test.pl test
 
 clean:
+	find . -name '*.out' -execdir $(RM) '{}' \;
 	$(RM) tests*.log
diff --git a/regression/cbmc-primitives/Makefile b/regression/cbmc-primitives/Makefile
index 64e9659281e..1c5578af570 100644
--- a/regression/cbmc-primitives/Makefile
+++ b/regression/cbmc-primitives/Makefile
@@ -11,4 +11,4 @@ tests.log: ../test.pl
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
-	$(RM) tests.log
+	$(RM) tests*.log
diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
index 13108fb57b8..a633d3cbaa9 100644
--- a/regression/cbmc/Makefile
+++ b/regression/cbmc/Makefile
@@ -39,4 +39,5 @@ tests.log: ../test.pl test
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
 	find . -name '*.smt2' -execdir $(RM) '{}' \;
+	$(RM) export-symex-ready-goto/exported.symex.ready.goto
 	$(RM) tests*.log
diff --git a/regression/contracts-dfcc/Makefile b/regression/contracts-dfcc/Makefile
index d31f978d48b..9dac0ee2d79 100644
--- a/regression/contracts-dfcc/Makefile
+++ b/regression/contracts-dfcc/Makefile
@@ -34,10 +34,10 @@ tests.log: ../test.pl test
 
 clean:
 	@for dir in *; do \
-		$(RM) tests.log; \
 		if [ -d "$$dir" ]; then \
 			cd "$$dir"; \
 			$(RM) *.out *.gb *.smt2; \
 			cd ..; \
 		fi \
 	done
+	$(RM) tests*.log
diff --git a/regression/cprover/Makefile b/regression/cprover/Makefile
index 7ba46755339..0e7c3786a40 100644
--- a/regression/cprover/Makefile
+++ b/regression/cprover/Makefile
@@ -10,4 +10,5 @@ test-no-p:
 	@../test.pl -e -c '../../../src/cprover/cprover'
 
 clean:
+	find . -name '*.out' -execdir $(RM) '{}' \;
 	$(RM) tests.log
diff --git a/regression/goto-bmc/Makefile b/regression/goto-bmc/Makefile
new file mode 100644
index 00000000000..de14253cbeb
--- /dev/null
+++ b/regression/goto-bmc/Makefile
@@ -0,0 +1,12 @@
+default: tests.log
+
+test:
+	@../test.pl -e -p -c ../../../src/goto-bmc/goto-bmc
+
+tests.log: ../test.pl
+	@../test.pl -e -p -c ../../../src/goto-bmc/goto-bmc
+
+clean:
+	find . -name '*.out' -execdir $(RM) '{}' \;
+	find . -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
diff --git a/regression/goto-bmc/goto-bmc-non-symex-ready-goto/Makefile b/regression/goto-bmc/goto-bmc-non-symex-ready-goto/Makefile
new file mode 100644
index 00000000000..ce78e36252f
--- /dev/null
+++ b/regression/goto-bmc/goto-bmc-non-symex-ready-goto/Makefile
@@ -0,0 +1,25 @@
+default: tests.log
+
+include ../../../src/config.inc
+include ../../../src/common
+
+GOTO_BMC_EXE=../../../../src/goto-bmc/goto-bmc
+
+ifeq ($(BUILD_ENV_),MSVC)
+	GOTO_CC_EXE=../../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	GOTO_CC_EXE=../../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
+test:
+	@../../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_BMC_EXE) $(is_windows)"
+
+tests.log: ../test.pl
+	@../../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_BMC_EXE) $(is_windows)"
+
+clean:
+	find . -name '*.out' -execdir $(RM) '{}' \;
+	find . -name '*.gb' -execdir $(RM) {} \;
+	$(RM) tests.log
diff --git a/regression/goto-bmc/goto-bmc-symex-ready-goto/Makefile b/regression/goto-bmc/goto-bmc-symex-ready-goto/Makefile
new file mode 100644
index 00000000000..d52a881aad5
--- /dev/null
+++ b/regression/goto-bmc/goto-bmc-symex-ready-goto/Makefile
@@ -0,0 +1,15 @@
+default: tests.log
+
+CBMC_EXE=../../../../src/cbmc/cbmc
+GOTO_BMC_EXE=../../../../src/goto-bmc/goto-bmc
+
+test:
+	@../../test.pl -e -p -c "../chain.sh $(CBMC_EXE) $(GOTO_BMC_EXE)"
+
+tests.log: ../test.pl
+	@../../test.pl -e -p -c "../chain.sh $(CBMC_EXE) $(GOTO_BMC_EXE)"
+
+clean:
+	find . -name '*.out' -execdir $(RM) '{}' \;
+	find . -name '*.gb' -execdir $(RM) {} \;
+	$(RM) tests.log
diff --git a/regression/goto-bmc/goto-bmc-symex-ready-goto/chain.sh b/regression/goto-bmc/goto-bmc-symex-ready-goto/chain.sh
index 8fe1d4577c1..2bca8755b21 100755
--- a/regression/goto-bmc/goto-bmc-symex-ready-goto/chain.sh
+++ b/regression/goto-bmc/goto-bmc-symex-ready-goto/chain.sh
@@ -9,5 +9,5 @@ options=${*:3:$#-3}
 name=${*:$#}
 base_name=${name%.c}
 
-"${cbmc}" --export-symex-ready-goto "${base_name}.goto.symex_ready" "${name}"
-"${goto_bmc}" "${base_name}.goto.symex_ready" ${options}
+"${cbmc}" --export-symex-ready-goto "${base_name}.gb" "${name}"
+"${goto_bmc}" "${base_name}.gb" ${options}
diff --git a/regression/goto-harness/Makefile b/regression/goto-harness/Makefile
index 71166794d86..3a1d2fb5937 100644
--- a/regression/goto-harness/Makefile
+++ b/regression/goto-harness/Makefile
@@ -23,4 +23,5 @@ tests.log: ../test.pl
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
 	find . -name '*.gb' -execdir $(RM) {} \;
+	find . -name '*-harness.c' -execdir $(RM) {} \;
 	$(RM) tests.log
diff --git a/regression/goto-instrument/Makefile b/regression/goto-instrument/Makefile
index 26ca0a7c48b..ea28defcf7b 100644
--- a/regression/goto-instrument/Makefile
+++ b/regression/goto-instrument/Makefile
@@ -26,3 +26,4 @@ clean:
 			cd ..; \
 		fi \
 	done
+	$(RM) ../cbmc/Recursion6/*.gb
diff --git a/regression/libcprover-cpp/Makefile b/regression/libcprover-cpp/Makefile
new file mode 100644
index 00000000000..54c8323d226
--- /dev/null
+++ b/regression/libcprover-cpp/Makefile
@@ -0,0 +1,41 @@
+default: tests.log
+
+SRC = call_bmc.cpp $(wildcard ../../src/libcprover-cpp/*.cpp)
+
+OBJ += ../../src/libcprover-cpp/libcprover-cpp$(LIBEXT)
+
+INCLUDES = -I ../../src/ -I ../../src/goto-programs/
+
+CLEANFILES = api-binary-driver$(EXEEXT)
+
+include ../../src/config.inc
+include ../../src/common
+
+api-binary-driver$(EXEEXT): $(OBJ)
+	$(LINKBIN)
+
+DIRS = \
+  model_loading
+
+test:
+	@for dir in $(DIRS); do \
+		$(MAKE) -C "$$dir" test || exit 1; \
+	done;
+
+tests.log:
+	@for dir in $(DIRS); do \
+		$(MAKE) -C "$$dir" tests.log || exit 1; \
+	done;
+
+test tests.log: api-binary-driver$(EXEEXT)
+
+clean: regression_clean
+
+.PHONY: regression_clean
+regression_clean:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			$(MAKE) -C "$$dir" clean; \
+		fi; \
+	done;
+	$(RM) tests.log
diff --git a/regression/libcprover-cpp/model_loading/Makefile b/regression/libcprover-cpp/model_loading/Makefile
new file mode 100644
index 00000000000..06e3888f23a
--- /dev/null
+++ b/regression/libcprover-cpp/model_loading/Makefile
@@ -0,0 +1,12 @@
+default: tests.log
+
+test:
+	@../../test.pl -e -p -c ../../api-binary-driver
+
+tests.log:
+	@../../test.pl -e -p -c ../../api-binary-driver
+
+clean:
+	find . -name '*.out' -execdir $(RM) '{}' \;
+	find . -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
diff --git a/regression/solver-hardness/Makefile b/regression/solver-hardness/Makefile
index a290f5841bf..d7c7e123a7d 100644
--- a/regression/solver-hardness/Makefile
+++ b/regression/solver-hardness/Makefile
@@ -16,4 +16,5 @@ tests.log: ../test.pl test
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
+	find . -name '*.json' -execdir $(RM) '{}' \;
 	$(RM) tests.log
diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py
index 4405f5c3f92..1ee1c781abd 100644
--- a/regression/validate-trace-xml-schema/check.py
+++ b/regression/validate-trace-xml-schema/check.py
@@ -41,6 +41,7 @@
     # these test for invalid command line handling
     ['bad_option', 'test_multiple.desc'],
     ['bad_option', 'test.desc'],
+    ['export-symex-ready-goto', 'test-bad-usage.desc'],
     ['unknown-argument-suggestion', 'test.desc'],
     ['sat-solver-error', 'test.desc'],
     # this one produces XML intermingled with main XML output when used with --xml-ui
diff --git a/src/Makefile b/src/Makefile
index 48dd9944bde..dae2d361cf2 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -7,6 +7,7 @@ DIRS = analyses \
        cprover \
        crangler \
        goto-analyzer \
+       goto-bmc \
        goto-cc \
        goto-checker \
        goto-diff \
@@ -20,6 +21,7 @@ DIRS = analyses \
        json \
        json-symtab-language \
        langapi \
+       libcprover-cpp \
        linking \
        memory-analyzer \
        pointer-analysis \
@@ -34,6 +36,7 @@ all: cbmc.dir \
      cprover.dir \
      crangler.dir \
      goto-analyzer.dir \
+     goto-bmc.dir \
      goto-cc.dir \
      goto-diff.dir \
      goto-instrument.dir \
@@ -114,6 +117,10 @@ goto-synthesizer.dir: languages util.dir goto-programs.dir langapi.dir \
                     json.dir goto-checker.dir \
                     goto-instrument.dir
 
+goto-bmc.dir: libcprover-cpp.dir
+
+libcprover-cpp.dir: cbmc.dir
+
 # building for a particular directory
 
 $(patsubst %, %.dir, $(DIRS)):
diff --git a/src/goto-bmc/Makefile b/src/goto-bmc/Makefile
new file mode 100644
index 00000000000..e5e62c490c7
--- /dev/null
+++ b/src/goto-bmc/Makefile
@@ -0,0 +1,29 @@
+SRC = \
+  goto_bmc_main.cpp \
+  goto_bmc_parse_options.cpp \
+  # Empty last line
+
+OBJ += \
+  ../libcprover-cpp/libcprover-cpp$(LIBEXT) \
+  # Empty last line
+
+INCLUDES= -I .. -I ../libcprover-cpp
+
+LIBS =
+
+CLEANFILES = goto-bmc$(EXEEXT)
+
+include ../config.inc
+include ../common
+
+all: goto-bmc$(EXEEXT)
+
+###############################################################################
+
+goto-bmc$(EXEEXT): $(OBJ)
+	$(LINKBIN)
+
+.PHONY: goto-bmc-mac-signed
+
+goto-bmc-mac-signed: goto-bmc$(EXEEXT)
+	codesign -v -s $(OSX_IDENTITY) goto-bmc$(EXEEXT)
diff --git a/src/libcprover-cpp/Makefile b/src/libcprover-cpp/Makefile
new file mode 100644
index 00000000000..96a8ef29be5
--- /dev/null
+++ b/src/libcprover-cpp/Makefile
@@ -0,0 +1,61 @@
+SRC = \
+  api.cpp \
+  api_options.cpp \
+  verification_result.cpp \
+  # Empty last line
+
+OBJ += \
+  ../analyses/analyses$(LIBEXT) \
+  ../ansi-c/ansi-c$(LIBEXT) \
+  ../assembler/assembler$(LIBEXT) \
+  ../big-int/big-int$(LIBEXT) \
+  ../goto-checker/goto-checker$(LIBEXT) \
+  ../goto-instrument/cover$(OBJEXT) \
+  ../goto-instrument/cover_basic_blocks$(OBJEXT) \
+  ../goto-instrument/cover_filter$(OBJEXT) \
+  ../goto-instrument/cover_instrument_assume$(OBJEXT) \
+  ../goto-instrument/cover_instrument_branch$(OBJEXT) \
+  ../goto-instrument/cover_instrument_condition$(OBJEXT) \
+  ../goto-instrument/cover_instrument_decision$(OBJEXT) \
+  ../goto-instrument/cover_instrument_location$(OBJEXT) \
+  ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
+  ../goto-instrument/cover_instrument_other$(OBJEXT) \
+  ../goto-instrument/cover_util$(OBJEXT) \
+  ../goto-instrument/full_slicer$(OBJEXT) \
+  ../goto-instrument/nondet_static$(OBJEXT) \
+  ../goto-instrument/reachability_slicer$(OBJEXT) \
+  ../goto-instrument/source_lines$(OBJEXT) \
+  ../goto-instrument/unwindset$(OBJEXT) \
+  ../goto-programs/goto-programs$(LIBEXT) \
+  ../goto-symex/goto-symex$(LIBEXT) \
+  ../jsil/jsil$(LIBEXT) \
+  ../json-symtab-language/json-symtab-language$(LIBEXT) \
+  ../json/json$(LIBEXT) \
+  ../langapi/langapi$(LIBEXT) \
+  ../linking/linking$(LIBEXT) \
+  ../pointer-analysis/add_failed_symbols$(OBJEXT) \
+  ../pointer-analysis/goto_program_dereference$(OBJEXT) \
+  ../pointer-analysis/value_set$(OBJEXT) \
+  ../pointer-analysis/value_set_analysis_fi$(OBJEXT) \
+  ../pointer-analysis/value_set_dereference$(OBJEXT) \
+  ../pointer-analysis/value_set_domain_fi$(OBJEXT) \
+  ../pointer-analysis/value_set_fi$(OBJEXT) \
+  ../solvers/solvers$(LIBEXT) \
+  ../statement-list/statement-list$(LIBEXT) \
+  ../util/util$(LIBEXT) \
+  ../xmllang/xmllang$(LIBEXT) \
+  # Empty last line
+
+INCLUDES = -I ..
+
+include ../config.inc
+include ../common
+
+CLEANFILES = libcprover-cpp$(LIBEXT)
+
+all: libcprover-cpp$(LIBEXT)
+
+###############################################################################
+
+libcprover-cpp$(LIBEXT): $(OBJ)
+	$(LINKLIB)
diff --git a/unit/Makefile b/unit/Makefile
index d93c683ab7e..59b3c5455eb 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -303,7 +303,7 @@ memory-analyzer/test.inc: memory-analyzer/test.c
 memory-analyzer/gdb_api$(OBJEXT): memory-analyzer/input.inc memory-analyzer/test.inc
 
 CLEANFILES = $(CATCH_TEST) testing-utils/testing-utils$(LIBEXT) \
-             memory-analyzer/input.inc memory-analyzer/test.inc
+             memory-analyzer/input.inc memory-analyzer/test.inc gdb.txt
 
 # only add a dependency for libraries to avoid triggering implicit rules, which
 # would cause unnecessary rebuilds