Add --no-standard-checks to regression/book-examples runner scripts

Author: NlightNFotis

regression/book-examples/CMakeLists.txt

@@ -13,27 +13,27 @@ else()
 endif()
 
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
+    "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
 )
 
 add_test_pl_profile(
     "book-examples-paths-lifo"
-    "$<TARGET_FILE:cbmc> --paths lifo"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --paths lifo"
     "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}"
     "CORE"
 )
 
 add_test_pl_profile(
     "book-examples-cprover-smt2"
-    "$<TARGET_FILE:cbmc> --cprover-smt2"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --cprover-smt2"
     "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}"
     "CORE"
 )
 
 # If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
 add_test_pl_profile(
   "book-examples-new-smt-backend"
-  "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
+  "$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'"
   "${gcc_only_string}-X;no-new-smt;-s;new-smt-backend"
   "CORE"
 )

regression/book-examples/Makefile

@@ -10,27 +10,27 @@ GCC_ONLY =
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
 
 test-cprover-smt2:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --cprover-smt2" \
 					  -X broken-smt-backend -X thorough-smt-backend \
 					  -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
 					  -s cprover-smt2 $(GCC_ONLY)
 
 test-z3:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --z3" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --z3" \
 					  -X broken-smt-backend -X thorough-smt-backend \
 					  -X broken-z3-smt-backend -X thorough-z3-smt-backend \
 					  -s z3 $(GCC_ONLY)
 
 test-paths-lifo:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --paths lifo" \
 					  -X thorough-paths -X smt-backend -X paths-lifo-expected-failure \
 					  -s paths-lifo $(GCC_ONLY)
 
 test-new-smt-backend:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'" \
 					  -X no-new-smt \
 					  -s new-smt-backend $(GCC_ONLY)