From 6a3d5522a4dd0a02ce465fed77eafe780964ede7 Mon Sep 17 00:00:00 2001
From: esteffin <enrylongo@gmail.com>
Date: Tue, 19 Dec 2023 17:14:08 +0000
Subject: [PATCH] Fixed contracts regressions

---
 .../contracts/assigns-replace-ignored-return-value/test.desc    | 2 +-
 regression/contracts/assigns_enforce_21/test.desc               | 2 +-
 regression/contracts/assigns_enforce_arrays_02/test.desc        | 2 +-
 regression/contracts/assigns_enforce_havoc_object/test.desc     | 2 +-
 regression/contracts/assigns_enforce_multi_file_02/test.desc    | 2 +-
 regression/contracts/assigns_enforce_scoping_02/test.desc       | 2 +-
 regression/contracts/assigns_enforce_statics/test.desc          | 2 +-
 regression/contracts/assigns_enforce_structs_06/test.desc       | 2 +-
 .../assigns_replace_havoc_dependent_targets_pass/enforce.desc   | 2 +-
 .../contracts/assigns_type_checking_valid_cases/test.desc       | 2 +-
 regression/contracts/detect_loop_locals/test.desc               | 2 +-
 .../contracts/github_6168_infinite_unwinding_bug/test.desc      | 2 +-
 regression/contracts/history-index/test.desc                    | 2 +-
 regression/contracts/history-pointer-enforce-10/test.desc       | 2 +-
 regression/contracts/history-pointer-replace-04/test.desc       | 2 +-
 regression/contracts/invar_check_multiple_loops/test.desc       | 2 +-
 regression/contracts/invar_check_nested_loops/test.desc         | 2 +-
 regression/contracts/invar_check_pointer_modifies-01/test.desc  | 2 +-
 regression/contracts/invar_check_pointer_modifies-02/test.desc  | 2 +-
 regression/contracts/invar_havoc_dynamic_array/test.desc        | 2 +-
 .../contracts/invar_havoc_dynamic_array_const_idx/test.desc     | 2 +-
 .../invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc | 2 +-
 regression/contracts/invar_loop-entry_check/test.desc           | 2 +-
 regression/contracts/invariant_side_effects/test.desc           | 2 +-
 regression/contracts/is_unique_01_replace/test.desc             | 2 +-
 regression/contracts/loop_assigns-01/test.desc                  | 2 +-
 regression/contracts/loop_assigns-03/test.desc                  | 2 +-
 regression/contracts/loop_assigns-05/test.desc                  | 2 +-
 .../contracts/loop_assigns-slice-assignable-ptr/test.desc       | 2 +-
 .../contracts/loop_assigns-slice-assignable-scalar/test.desc    | 2 +-
 regression/contracts/loop_assigns-slice-from/test.desc          | 2 +-
 regression/contracts/loop_assigns-slice-upto-fail/test.desc     | 2 +-
 regression/contracts/loop_assigns-slice-upto-pass/test.desc     | 2 +-
 regression/contracts/loop_assigns_inference-01/test.desc        | 2 +-
 regression/contracts/loop_assigns_inference-02/test.desc        | 2 +-
 .../contracts/loop_assigns_scoped_local_statics/test.desc       | 2 +-
 .../loop_assigns_scoped_local_statics_propagate/test.desc       | 2 +-
 regression/contracts/no_redudant_checks/test.desc               | 2 +-
 regression/contracts/nonvacuous_loop_contracts/test.desc        | 2 +-
 .../contracts/quantifiers-forall-ensures-enforce/test.desc      | 2 +-
 regression/contracts/quantifiers-loop-02/test.desc              | 2 +-
 regression/contracts/quantifiers-loop-03/test.desc              | 2 +-
 regression/contracts/test_aliasing_ensure/test.desc             | 2 +-
 regression/contracts/test_array_memory_replace/test.desc        | 2 +-
 .../contracts/test_array_memory_too_small_replace/test.desc     | 2 +-
 regression/contracts/test_scalar_memory_replace/test.desc       | 2 +-
 46 files changed, 46 insertions(+), 46 deletions(-)

diff --git a/regression/contracts/assigns-replace-ignored-return-value/test.desc b/regression/contracts/assigns-replace-ignored-return-value/test.desc
index be3c595b24e..67757391cd5 100644
--- a/regression/contracts/assigns-replace-ignored-return-value/test.desc
+++ b/regression/contracts/assigns-replace-ignored-return-value/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
+--replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo _ --no-standard-checks
 ^\[bar.precondition.\d+\] line \d+ Check requires clause of bar in foo: SUCCESS$
 ^\[baz.precondition.\d+\] line \d+ Check requires clause of baz in foo: SUCCESS$
 ^EXIT=0$
diff --git a/regression/contracts/assigns_enforce_21/test.desc b/regression/contracts/assigns_enforce_21/test.desc
index f27b7f42c59..bd133cff21d 100644
--- a/regression/contracts/assigns_enforce_21/test.desc
+++ b/regression/contracts/assigns_enforce_21/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo --replace-call-with-contract quz
+--enforce-contract foo --replace-call-with-contract quz _ --no-standard-checks
 ^\[foo.assigns.\d+\] line \d+ Check that \*y is valid: SUCCESS$
 ^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^\[bar.assigns.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE$
diff --git a/regression/contracts/assigns_enforce_arrays_02/test.desc b/regression/contracts/assigns_enforce_arrays_02/test.desc
index e8150f13152..dd6bb3f6b0b 100644
--- a/regression/contracts/assigns_enforce_arrays_02/test.desc
+++ b/regression/contracts/assigns_enforce_arrays_02/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract f2
+--enforce-contract f1 --enforce-contract f2 _ --no-standard-checks
 ^\[f1.assigns.\d+\] line 6 Check that \*a is valid: SUCCESS$
 ^\[f1.assigns.\d+\] line 8 Check that a\[.*0\] is assignable: SUCCESS$
 ^\[f1.assigns.\d+\] line 9 Check that a\[.*5\] is assignable: FAILURE$
diff --git a/regression/contracts/assigns_enforce_havoc_object/test.desc b/regression/contracts/assigns_enforce_havoc_object/test.desc
index 2563aafae1a..d641ddacda6 100644
--- a/regression/contracts/assigns_enforce_havoc_object/test.desc
+++ b/regression/contracts/assigns_enforce_havoc_object/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo
+--enforce-contract foo _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_object_whole\(\(.*\)a1->u.b->c\) is valid: SUCCESS$
diff --git a/regression/contracts/assigns_enforce_multi_file_02/test.desc b/regression/contracts/assigns_enforce_multi_file_02/test.desc
index c9f45d47c58..95d882970cd 100644
--- a/regression/contracts/assigns_enforce_multi_file_02/test.desc
+++ b/regression/contracts/assigns_enforce_multi_file_02/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f1 _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[f1.assigns.\d+\] line \d+ Check that \*a is valid: SUCCESS$
diff --git a/regression/contracts/assigns_enforce_scoping_02/test.desc b/regression/contracts/assigns_enforce_scoping_02/test.desc
index a5d07aa04d5..e785c988870 100644
--- a/regression/contracts/assigns_enforce_scoping_02/test.desc
+++ b/regression/contracts/assigns_enforce_scoping_02/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f1 _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[f1.assigns.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$
diff --git a/regression/contracts/assigns_enforce_statics/test.desc b/regression/contracts/assigns_enforce_statics/test.desc
index 87f417d025f..6b17951f85e 100644
--- a/regression/contracts/assigns_enforce_statics/test.desc
+++ b/regression/contracts/assigns_enforce_statics/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo _ --pointer-primitive-check
+--enforce-contract foo _ --pointer-primitive-check --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[foo.assigns.\d+\] line \d+ Check that x is valid: SUCCESS$
diff --git a/regression/contracts/assigns_enforce_structs_06/test.desc b/regression/contracts/assigns_enforce_structs_06/test.desc
index 838bcce9c4e..18be8445731 100644
--- a/regression/contracts/assigns_enforce_structs_06/test.desc
+++ b/regression/contracts/assigns_enforce_structs_06/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract f2 --enforce-contract f3
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3 _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: SUCCESS$
diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_pass/enforce.desc b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/enforce.desc
index efca0a7366c..018166e7c24 100644
--- a/regression/contracts/assigns_replace_havoc_dependent_targets_pass/enforce.desc
+++ b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/enforce.desc
@@ -1,6 +1,6 @@
 CORE
 main_enforce.c
---enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+--enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --no-standard-checks
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns_type_checking_valid_cases/test.desc b/regression/contracts/assigns_type_checking_valid_cases/test.desc
index 6f67aaef718..4b9643d1418 100644
--- a/regression/contracts/assigns_type_checking_valid_cases/test.desc
+++ b/regression/contracts/assigns_type_checking_valid_cases/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo1 --enforce-contract foo2 --enforce-contract foo3 --enforce-contract foo4 --enforce-contract foo5 --enforce-contract foo6 --enforce-contract foo7 --enforce-contract foo8 --enforce-contract foo9 --enforce-contract foo10 _ --pointer-primitive-check
+--enforce-contract foo1 --enforce-contract foo2 --enforce-contract foo3 --enforce-contract foo4 --enforce-contract foo5 --enforce-contract foo6 --enforce-contract foo7 --enforce-contract foo8 --enforce-contract foo9 --enforce-contract foo10 _ --pointer-primitive-check --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[foo10.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$
diff --git a/regression/contracts/detect_loop_locals/test.desc b/regression/contracts/detect_loop_locals/test.desc
index c116642ea92..00284496aea 100644
--- a/regression/contracts/detect_loop_locals/test.desc
+++ b/regression/contracts/detect_loop_locals/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^\[main.assigns.\d+\].*line 10 Check that i is assignable: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/contracts/github_6168_infinite_unwinding_bug/test.desc b/regression/contracts/github_6168_infinite_unwinding_bug/test.desc
index 4714105d895..da9bf98b0d9 100644
--- a/regression/contracts/github_6168_infinite_unwinding_bug/test.desc
+++ b/regression/contracts/github_6168_infinite_unwinding_bug/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/history-index/test.desc b/regression/contracts/history-index/test.desc
index 7e0f7f23a3b..8f2e43d1a84 100644
--- a/regression/contracts/history-index/test.desc
+++ b/regression/contracts/history-index/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/history-pointer-enforce-10/test.desc b/regression/contracts/history-pointer-enforce-10/test.desc
index 6ab7a0823ef..785de8d3894 100644
--- a/regression/contracts/history-pointer-enforce-10/test.desc
+++ b/regression/contracts/history-pointer-enforce-10/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo --enforce-contract bar --enforce-contract baz
+--enforce-contract foo --enforce-contract bar --enforce-contract baz _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[bar.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
diff --git a/regression/contracts/history-pointer-replace-04/test.desc b/regression/contracts/history-pointer-replace-04/test.desc
index c4458b4a9bf..3e79c294713 100644
--- a/regression/contracts/history-pointer-replace-04/test.desc
+++ b/regression/contracts/history-pointer-replace-04/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract foo
+--replace-call-with-contract foo _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$
diff --git a/regression/contracts/invar_check_multiple_loops/test.desc b/regression/contracts/invar_check_multiple_loops/test.desc
index 86b4399b890..282796e8b78 100644
--- a/regression/contracts/invar_check_multiple_loops/test.desc
+++ b/regression/contracts/invar_check_multiple_loops/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_nested_loops/test.desc b/regression/contracts/invar_check_nested_loops/test.desc
index d7360332c84..fa5b348e90d 100644
--- a/regression/contracts/invar_check_nested_loops/test.desc
+++ b/regression/contracts/invar_check_nested_loops/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_pointer_modifies-01/test.desc b/regression/contracts/invar_check_pointer_modifies-01/test.desc
index deb947163f4..8729522855b 100644
--- a/regression/contracts/invar_check_pointer_modifies-01/test.desc
+++ b/regression/contracts/invar_check_pointer_modifies-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts --pointer-check
+--apply-loop-contracts --pointer-check _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_pointer_modifies-02/test.desc b/regression/contracts/invar_check_pointer_modifies-02/test.desc
index 95a9eb36ea7..8b60e96baed 100644
--- a/regression/contracts/invar_check_pointer_modifies-02/test.desc
+++ b/regression/contracts/invar_check_pointer_modifies-02/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts --pointer-check
+--apply-loop-contracts --pointer-check _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_dynamic_array/test.desc b/regression/contracts/invar_havoc_dynamic_array/test.desc
index 582a93ff682..5ed2833d3b1 100644
--- a/regression/contracts/invar_havoc_dynamic_array/test.desc
+++ b/regression/contracts/invar_havoc_dynamic_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc
index c970e1f49b1..c51ec4d4460 100644
--- a/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc
+++ b/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc
index ff6b7e8e980..7b1ec015160 100644
--- a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc
+++ b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_loop-entry_check/test.desc b/regression/contracts/invar_loop-entry_check/test.desc
index 554a504ef23..27c61040a6a 100644
--- a/regression/contracts/invar_loop-entry_check/test.desc
+++ b/regression/contracts/invar_loop-entry_check/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts _ --pointer-primitive-check
+--apply-loop-contracts _ --pointer-primitive-check --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invariant_side_effects/test.desc b/regression/contracts/invariant_side_effects/test.desc
index 8268af383e0..86e0e537648 100644
--- a/regression/contracts/invariant_side_effects/test.desc
+++ b/regression/contracts/invariant_side_effects/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/is_unique_01_replace/test.desc b/regression/contracts/is_unique_01_replace/test.desc
index ff7c558fb1e..176908706d2 100644
--- a/regression/contracts/is_unique_01_replace/test.desc
+++ b/regression/contracts/is_unique_01_replace/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract foo
+--replace-call-with-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/loop_assigns-01/test.desc b/regression/contracts/loop_assigns-01/test.desc
index dfdb76bc45b..9eabff95537 100644
--- a/regression/contracts/loop_assigns-01/test.desc
+++ b/regression/contracts/loop_assigns-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/loop_assigns-03/test.desc b/regression/contracts/loop_assigns-03/test.desc
index 15963cb9c00..c1aa6a60e39 100644
--- a/regression/contracts/loop_assigns-03/test.desc
+++ b/regression/contracts/loop_assigns-03/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/loop_assigns-05/test.desc b/regression/contracts/loop_assigns-05/test.desc
index 0dc2ffedc89..af839f6d028 100644
--- a/regression/contracts/loop_assigns-05/test.desc
+++ b/regression/contracts/loop_assigns-05/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$
diff --git a/regression/contracts/loop_assigns-slice-assignable-ptr/test.desc b/regression/contracts/loop_assigns-slice-assignable-ptr/test.desc
index 9a49850f1c3..7c4b3005f73 100644
--- a/regression/contracts/loop_assigns-slice-assignable-ptr/test.desc
+++ b/regression/contracts/loop_assigns-slice-assignable-ptr/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/loop_assigns-slice-assignable-scalar/test.desc b/regression/contracts/loop_assigns-slice-assignable-scalar/test.desc
index 3ab6f3105b4..7122fbf77bb 100644
--- a/regression/contracts/loop_assigns-slice-assignable-scalar/test.desc
+++ b/regression/contracts/loop_assigns-slice-assignable-scalar/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/loop_assigns-slice-from/test.desc b/regression/contracts/loop_assigns-slice-from/test.desc
index dca584fe348..82fee0e8ae0 100644
--- a/regression/contracts/loop_assigns-slice-from/test.desc
+++ b/regression/contracts/loop_assigns-slice-from/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/loop_assigns-slice-upto-fail/test.desc b/regression/contracts/loop_assigns-slice-upto-fail/test.desc
index 4300f9931ef..f15999d52dd 100644
--- a/regression/contracts/loop_assigns-slice-upto-fail/test.desc
+++ b/regression/contracts/loop_assigns-slice-upto-fail/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
diff --git a/regression/contracts/loop_assigns-slice-upto-pass/test.desc b/regression/contracts/loop_assigns-slice-upto-pass/test.desc
index a9aea6e7386..990fbc3e932 100644
--- a/regression/contracts/loop_assigns-slice-upto-pass/test.desc
+++ b/regression/contracts/loop_assigns-slice-upto-pass/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
diff --git a/regression/contracts/loop_assigns_inference-01/test.desc b/regression/contracts/loop_assigns_inference-01/test.desc
index 11da15c0fcf..7e476a79296 100644
--- a/regression/contracts/loop_assigns_inference-01/test.desc
+++ b/regression/contracts/loop_assigns_inference-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$
diff --git a/regression/contracts/loop_assigns_inference-02/test.desc b/regression/contracts/loop_assigns_inference-02/test.desc
index c153a24b794..cb6479b0037 100644
--- a/regression/contracts/loop_assigns_inference-02/test.desc
+++ b/regression/contracts/loop_assigns_inference-02/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/loop_assigns_scoped_local_statics/test.desc b/regression/contracts/loop_assigns_scoped_local_statics/test.desc
index 761d2f6fe27..5a7118440e8 100644
--- a/regression/contracts/loop_assigns_scoped_local_statics/test.desc
+++ b/regression/contracts/loop_assigns_scoped_local_statics/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$
diff --git a/regression/contracts/loop_assigns_scoped_local_statics_propagate/test.desc b/regression/contracts/loop_assigns_scoped_local_statics_propagate/test.desc
index 69d673846c6..4dc004cc32e 100644
--- a/regression/contracts/loop_assigns_scoped_local_statics_propagate/test.desc
+++ b/regression/contracts/loop_assigns_scoped_local_statics_propagate/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract bar --apply-loop-contracts
+--replace-call-with-contract bar --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assigns.\d+\] line \d+ Check that j \(assigned by the contract of bar\) is assignable: SUCCESS$
diff --git a/regression/contracts/no_redudant_checks/test.desc b/regression/contracts/no_redudant_checks/test.desc
index ed318ccbec3..74fcab6c862 100644
--- a/regression/contracts/no_redudant_checks/test.desc
+++ b/regression/contracts/no_redudant_checks/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-overflow-check _ --pointer-overflow-check --unsigned-overflow-check
+--pointer-overflow-check _ --pointer-overflow-check --unsigned-overflow-check --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[malloc.assertion.1\].*: SUCCESS
diff --git a/regression/contracts/nonvacuous_loop_contracts/test.desc b/regression/contracts/nonvacuous_loop_contracts/test.desc
index e50b9896f18..f0307d5e494 100644
--- a/regression/contracts/nonvacuous_loop_contracts/test.desc
+++ b/regression/contracts/nonvacuous_loop_contracts/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts _ --signed-overflow-check --unsigned-overflow-check
+--apply-loop-contracts _ --signed-overflow-check --unsigned-overflow-check --no-standard-checks
 \[main.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
 \[main.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
 \[main.assigns.\d+\] line \d+ Check that end is valid: SUCCESS$
diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc
index 77d7c1e018a..49e9233eb54 100644
--- a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc
+++ b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f1 _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
diff --git a/regression/contracts/quantifiers-loop-02/test.desc b/regression/contracts/quantifiers-loop-02/test.desc
index 3ae97f80f22..d097cbf4314 100644
--- a/regression/contracts/quantifiers-loop-02/test.desc
+++ b/regression/contracts/quantifiers-loop-02/test.desc
@@ -1,6 +1,6 @@
 CORE smt-backend broken-cprover-smt-backend thorough-smt-backend
 main.c
---apply-loop-contracts _ --z3
+--apply-loop-contracts _ --z3 --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.\d+\] line .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/quantifiers-loop-03/test.desc b/regression/contracts/quantifiers-loop-03/test.desc
index 86140e129eb..3bc5c386593 100644
--- a/regression/contracts/quantifiers-loop-03/test.desc
+++ b/regression/contracts/quantifiers-loop-03/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/test_aliasing_ensure/test.desc b/regression/contracts/test_aliasing_ensure/test.desc
index 70ae1bdd9ff..89a3721c710 100644
--- a/regression/contracts/test_aliasing_ensure/test.desc
+++ b/regression/contracts/test_aliasing_ensure/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo
+--enforce-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 \[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
diff --git a/regression/contracts/test_array_memory_replace/test.desc b/regression/contracts/test_array_memory_replace/test.desc
index b6c5d13435b..20f6445ca0a 100644
--- a/regression/contracts/test_array_memory_replace/test.desc
+++ b/regression/contracts/test_array_memory_replace/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract foo
+--replace-call-with-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 \[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS
diff --git a/regression/contracts/test_array_memory_too_small_replace/test.desc b/regression/contracts/test_array_memory_too_small_replace/test.desc
index fb30f3ebf7c..693a85b80e5 100644
--- a/regression/contracts/test_array_memory_too_small_replace/test.desc
+++ b/regression/contracts/test_array_memory_too_small_replace/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract foo
+--replace-call-with-contract foo _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 \[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: FAILURE
diff --git a/regression/contracts/test_scalar_memory_replace/test.desc b/regression/contracts/test_scalar_memory_replace/test.desc
index 941d4f8c249..e9c20b3fe62 100644
--- a/regression/contracts/test_scalar_memory_replace/test.desc
+++ b/regression/contracts/test_scalar_memory_replace/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract foo
+--replace-call-with-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 \[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS