diff --git a/regression/goto-synthesizer/array_uf/test.desc b/regression/goto-synthesizer/array_uf/test.desc
index 81f0cc90d5de..bf33d9d629e8 100644
--- a/regression/goto-synthesizer/array_uf/test.desc
+++ b/regression/goto-synthesizer/array_uf/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check _ --arrays-uf-always _ --arrays-uf-always
+--pointer-check _ --no-malloc-may-fail --arrays-uf-always _ --arrays-uf-always
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_01/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_01/test.desc
index 405303402c77..443ffa43fddf 100644
--- a/regression/goto-synthesizer/loop_contracts_synthesis_01/test.desc
+++ b/regression/goto-synthesizer/loop_contracts_synthesis_01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+--pointer-check _ --no-malloc-may-fail _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] line 10 Check loop invariant before entry: SUCCESS$
diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_01/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_01/test_dump.desc
index 363f91f24e65..8d9ef3ada569 100644
--- a/regression/goto-synthesizer/loop_contracts_synthesis_01/test_dump.desc
+++ b/regression/goto-synthesizer/loop_contracts_synthesis_01/test_dump.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check _ --dump-loop-contracts --json-output main.c
+--pointer-check _ --no-malloc-may-fail --dump-loop-contracts --json-output main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \"sources"\: \[ \"main\.c\" \]
diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_02/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_02/test.desc
index 71ecf7106695..a7a3276e65e5 100644
--- a/regression/goto-synthesizer/loop_contracts_synthesis_02/test.desc
+++ b/regression/goto-synthesizer/loop_contracts_synthesis_02/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+--pointer-check _ --no-malloc-may-fail
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.pointer\_dereference.\d+\] .* SUCCESS$
diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc
index dd6f4658ccad..8200b32e88e3 100644
--- a/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc
+++ b/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check _ --dump-loop-contracts
+--pointer-check _ --dump-loop-contracts --no-malloc-may-fail
 ^EXIT=0$
 ^SIGNAL=0$
 \"sources"\: \[ \"main\.c\" \]
diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_03/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_03/test.desc
index 70c75536ac23..195581932abb 100644
--- a/regression/goto-synthesizer/loop_contracts_synthesis_03/test.desc
+++ b/regression/goto-synthesizer/loop_contracts_synthesis_03/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+--pointer-check _ --no-malloc-may-fail _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.pointer\_dereference.\d+\] .* SUCCESS$
diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_03/test_cadical.desc b/regression/goto-synthesizer/loop_contracts_synthesis_03/test_cadical.desc
index 9b1ab0946342..c7efad193a57 100644
--- a/regression/goto-synthesizer/loop_contracts_synthesis_03/test_cadical.desc
+++ b/regression/goto-synthesizer/loop_contracts_synthesis_03/test_cadical.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check _ --sat-solver cadical --verbosity 10
+--pointer-check _ --no-malloc-may-fail --sat-solver cadical --verbosity 10 _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 Solving with CaDiCaL|The specified solver, 'cadical', is not available. The default solver will be used instead.
diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_03/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_03/test_dump.desc
index 08d4cad81ff7..bfec5782fe80 100644
--- a/regression/goto-synthesizer/loop_contracts_synthesis_03/test_dump.desc
+++ b/regression/goto-synthesizer/loop_contracts_synthesis_03/test_dump.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check _ --dump-loop-contracts
+--pointer-check _ --no-malloc-may-fail --dump-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 \"sources"\: \[ \"main\.c\" \]
diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_04/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_04/test.desc
index e7ee10ae51a4..9ebb1913e743 100644
--- a/regression/goto-synthesizer/loop_contracts_synthesis_04/test.desc
+++ b/regression/goto-synthesizer/loop_contracts_synthesis_04/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check _ --verbosity 9
+--pointer-check _ --no-malloc-may-fail --verbosity 9
 ^EXIT=0$
 ^SIGNAL=0$
 Quick filter\: 6.* out of 67 candidates were filtered out\.
diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_04/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_04/test_dump.desc
index 41399773eff7..a8274ceb1bde 100644
--- a/regression/goto-synthesizer/loop_contracts_synthesis_04/test_dump.desc
+++ b/regression/goto-synthesizer/loop_contracts_synthesis_04/test_dump.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check _ --dump-loop-contracts
+--pointer-check _ --no-malloc-may-fail --dump-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 \"sources"\: \[ \"main\.c\" \]
diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_08/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_08/test.desc
index 2b98c115ec74..ecedb4797aab 100644
--- a/regression/goto-synthesizer/loop_contracts_synthesis_08/test.desc
+++ b/regression/goto-synthesizer/loop_contracts_synthesis_08/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+--pointer-check _ --no-malloc-may-fail _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.pointer\_dereference.\d+\] .* SUCCESS$