From bdc353858366669321ff420583e84c7f8c93ea6b Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 13 Dec 2022 18:02:12 +0000 Subject: [PATCH] Add 645 regression tests from cbmc folder --- regression/cbmc/ACSL/quantifier-precedence.desc | 2 +- regression/cbmc/ASHR1/test.desc | 2 +- regression/cbmc/Address_of1/test.desc | 2 +- regression/cbmc/Address_of2/test.desc | 2 +- regression/cbmc/Array_Access1/test.desc | 2 +- regression/cbmc/Array_Access2/test.desc | 2 +- regression/cbmc/Array_Access3/test.desc | 2 +- regression/cbmc/Array_Initialization1/test.desc | 2 +- regression/cbmc/Array_Initialization2/test.desc | 2 +- regression/cbmc/Array_Initialization3/test.desc | 2 +- regression/cbmc/Array_Pointer1/test.desc | 2 +- regression/cbmc/Array_Pointer2/test.desc | 2 +- regression/cbmc/Array_Pointer3/test.desc | 2 +- regression/cbmc/Array_Pointer4/test.desc | 2 +- regression/cbmc/Array_Pointer5/test.desc | 2 +- regression/cbmc/Array_Pointer6/test.desc | 2 +- regression/cbmc/Array_Pointer7/test.desc | 2 +- regression/cbmc/Array_Propagation1/test.desc | 2 +- regression/cbmc/Array_UF1/test.desc | 2 +- regression/cbmc/Array_UF10/test.desc | 2 +- regression/cbmc/Array_UF11/test.desc | 2 +- regression/cbmc/Array_UF12/test.desc | 2 +- regression/cbmc/Array_UF13/test.desc | 2 +- regression/cbmc/Array_UF14/test.desc | 2 +- regression/cbmc/Array_UF15/test.desc | 2 +- regression/cbmc/Array_UF16/test.desc | 2 +- regression/cbmc/Array_UF17/test.desc | 2 +- regression/cbmc/Array_UF18/test.desc | 2 +- regression/cbmc/Array_UF19/test.desc | 2 +- regression/cbmc/Array_UF2/test.desc | 2 +- regression/cbmc/Array_UF20/test.desc | 2 +- regression/cbmc/Array_UF21/test.desc | 2 +- regression/cbmc/Array_UF3/test.desc | 2 +- regression/cbmc/Array_UF5/test.desc | 2 +- regression/cbmc/Array_UF6/test.desc | 2 +- regression/cbmc/Array_UF7/test.desc | 2 +- regression/cbmc/Array_UF9/test.desc | 2 +- regression/cbmc/BV_Arithmetic1/test.desc | 2 +- regression/cbmc/BV_Arithmetic2/test.desc | 2 +- regression/cbmc/BV_Arithmetic3/test.desc | 2 +- regression/cbmc/BV_Arithmetic4/test.desc | 2 +- regression/cbmc/BV_Arithmetic5/test.desc | 2 +- regression/cbmc/BV_Arithmetic6/test.desc | 2 +- regression/cbmc/Bitfields4/test.desc | 2 +- regression/cbmc/Bool/bool1.desc | 2 +- regression/cbmc/Bool/bool4.desc | 2 +- regression/cbmc/Bool/bool5-full-slice.desc | 2 +- regression/cbmc/Bool/bool5.desc | 2 +- regression/cbmc/Bool/bool6.desc | 2 +- regression/cbmc/Boolean_Guards1/test.desc | 2 +- regression/cbmc/Division1/test.desc | 2 +- regression/cbmc/Division2/test.desc | 2 +- regression/cbmc/Ellipsis1/test.desc | 2 +- regression/cbmc/Ellipsis2/test.desc | 2 +- regression/cbmc/End_thread1/test.desc | 2 +- regression/cbmc/Endianness1/test.desc | 2 +- regression/cbmc/Endianness2/test.desc | 2 +- regression/cbmc/Endianness3/test.desc | 2 +- regression/cbmc/Endianness4/test.desc | 2 +- regression/cbmc/Endianness5/test.desc | 2 +- regression/cbmc/Endianness6/test.desc | 2 +- regression/cbmc/Endianness8/test.desc | 2 +- regression/cbmc/Endianness9/test.desc | 2 +- regression/cbmc/Error_Label1/test.desc | 2 +- regression/cbmc/Error_Label2/test.desc | 2 +- regression/cbmc/Error_Label3/test.desc | 2 +- regression/cbmc/Eval_Order1/test.desc | 2 +- regression/cbmc/Exceptions1/test.desc | 2 +- regression/cbmc/Failed_Symbols1/test.desc | 2 +- regression/cbmc/Failing_Assert1/test.desc | 2 +- regression/cbmc/Free1/test.desc | 2 +- regression/cbmc/Free2/test.desc | 2 +- regression/cbmc/Free3/test.desc | 2 +- regression/cbmc/Free4/test.desc | 2 +- regression/cbmc/Function12/test.desc | 2 +- regression/cbmc/Function2/test.desc | 2 +- regression/cbmc/Function3/test.desc | 2 +- regression/cbmc/Function4/test.desc | 2 +- regression/cbmc/Function_Eval_Order2/test.desc | 2 +- regression/cbmc/Function_Pointer1/test.desc | 2 +- regression/cbmc/Function_Pointer10/test.desc | 2 +- regression/cbmc/Function_Pointer12/test.desc | 2 +- regression/cbmc/Function_Pointer13/test.desc | 2 +- regression/cbmc/Function_Pointer14/test.desc | 2 +- regression/cbmc/Function_Pointer16/test.desc | 2 +- regression/cbmc/Function_Pointer17/test.desc | 2 +- regression/cbmc/Function_Pointer18/test.desc | 2 +- regression/cbmc/Function_Pointer19/test.desc | 2 +- regression/cbmc/Function_Pointer4/test.desc | 2 +- regression/cbmc/Function_Pointer7/test.desc | 2 +- regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc | 2 +- regression/cbmc/Global_Initialization1/test.desc | 2 +- regression/cbmc/Global_Initialization2/test.desc | 2 +- regression/cbmc/Initialization1/test.desc | 2 +- regression/cbmc/Initialization2/test.desc | 2 +- regression/cbmc/Initialization3/test.desc | 2 +- regression/cbmc/KnR1/test.desc | 2 +- regression/cbmc/Linked_List1/test.desc | 2 +- regression/cbmc/Linking1/test.desc | 2 +- regression/cbmc/Linking2/test.desc | 2 +- regression/cbmc/Linking3/test.desc | 2 +- regression/cbmc/Linking4/test.desc | 2 +- regression/cbmc/Linking5/test.desc | 2 +- regression/cbmc/Linking6/test.desc | 2 +- regression/cbmc/Linking7/return_type.desc | 2 +- regression/cbmc/Linking8/test.desc | 2 +- regression/cbmc/Local_out_of_scope1/test.desc | 2 +- regression/cbmc/Local_out_of_scope2/test.desc | 2 +- regression/cbmc/Local_out_of_scope3/test.desc | 2 +- regression/cbmc/Local_out_of_scope4/test.desc | 2 +- regression/cbmc/Malloc1/test.desc | 2 +- regression/cbmc/Malloc11/slice-formula.desc | 2 +- regression/cbmc/Malloc11/test.desc | 2 +- regression/cbmc/Malloc14/test.desc | 2 +- regression/cbmc/Malloc15/test.desc | 2 +- regression/cbmc/Malloc16/test.desc | 2 +- regression/cbmc/Malloc17/test.desc | 2 +- regression/cbmc/Malloc18/test.desc | 2 +- regression/cbmc/Malloc2/test.desc | 2 +- regression/cbmc/Malloc21/test.desc | 2 +- regression/cbmc/Malloc22/test.desc | 2 +- regression/cbmc/Malloc24/test.desc | 2 +- regression/cbmc/Malloc25/test.desc | 2 +- regression/cbmc/Malloc3/test.desc | 2 +- regression/cbmc/Malloc4/test.desc | 2 +- regression/cbmc/Malloc5/test.desc | 2 +- regression/cbmc/Malloc6/test.desc | 2 +- regression/cbmc/Malloc7/test.desc | 2 +- regression/cbmc/Malloc9/test.desc | 2 +- regression/cbmc/Memory_leak_abort/test.desc | 2 +- regression/cbmc/Multi_Dimensional_Array1/test.desc | 2 +- regression/cbmc/Multi_Dimensional_Array2/test.desc | 2 +- regression/cbmc/Multi_Dimensional_Array3/test.desc | 2 +- regression/cbmc/Multi_Dimensional_Array4/test.desc | 2 +- regression/cbmc/Multi_Dimensional_Array5/test.desc | 2 +- regression/cbmc/Multi_Dimensional_Array6/test.desc | 2 +- regression/cbmc/Multiple_Properties1/test.desc | 2 +- regression/cbmc/Pointer20/test.desc | 2 +- regression/cbmc/Pointer21/test.desc | 2 +- regression/cbmc/Pointer23/test.desc | 2 +- regression/cbmc/Pointer3/test.desc | 2 +- regression/cbmc/Pointer31/test.desc | 2 +- regression/cbmc/Pointer4/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic1/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic11/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic16/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic8/test.desc | 2 +- regression/cbmc/Pointer_Object_Type1/test.desc | 2 +- regression/cbmc/Pointer_array1/test.desc | 2 +- regression/cbmc/Pointer_array2/test.desc | 2 +- regression/cbmc/Pointer_array3/test.desc | 2 +- regression/cbmc/Pointer_array4/test.desc | 2 +- regression/cbmc/Pointer_array6/test.desc | 2 +- regression/cbmc/Pointer_array7/big-endian.desc | 2 +- regression/cbmc/Pointer_array7/test.desc | 2 +- regression/cbmc/Pointer_byte_extract2/test.desc | 2 +- regression/cbmc/Pointer_byte_extract5/test.desc | 2 +- regression/cbmc/Pointer_byte_extract7/test.desc | 2 +- regression/cbmc/Pointer_byte_extract8/test.desc | 2 +- regression/cbmc/Pointer_comparison2/test.desc | 2 +- regression/cbmc/Pointer_difference1/no-simplify.desc | 2 +- regression/cbmc/Pointer_difference1/test.desc | 2 +- regression/cbmc/Promotion1/test.desc | 2 +- regression/cbmc/Promotion2/test.desc | 2 +- regression/cbmc/Promotion3/test.desc | 2 +- regression/cbmc/Promotion4/test.desc | 2 +- regression/cbmc/Quantifiers-simplify/rewrite_exists.desc | 2 +- regression/cbmc/Quantifiers-simplify/rewrite_forall.desc | 2 +- regression/cbmc/Quantifiers-simplify/simplify_not_forall.desc | 2 +- regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc | 2 +- regression/cbmc/Quantifiers1/test.desc | 2 +- regression/cbmc/Recursion1/test.desc | 2 +- regression/cbmc/Recursion2/test.desc | 2 +- regression/cbmc/Recursion3/test.desc | 2 +- regression/cbmc/Recursion4/test.desc | 2 +- regression/cbmc/Recursion5/test.desc | 2 +- regression/cbmc/Recursion6/test.desc | 2 +- regression/cbmc/Same_Basename1/test.desc | 2 +- regression/cbmc/Sideeffects1/test.desc | 2 +- regression/cbmc/Sideeffects2/test.desc | 2 +- regression/cbmc/Sideeffects3/test.desc | 2 +- regression/cbmc/Sideeffects4/test.desc | 2 +- regression/cbmc/Sideeffects5/test.desc | 2 +- regression/cbmc/Sideeffects6/test.desc | 2 +- regression/cbmc/Sideeffects8/test.desc | 2 +- regression/cbmc/Sizeof1/test.desc | 2 +- regression/cbmc/Static2/test.desc | 2 +- regression/cbmc/Static4/test.desc | 2 +- regression/cbmc/Static_Functions1/test.desc | 2 +- regression/cbmc/String1/test.desc | 2 +- regression/cbmc/String4/test.desc | 2 +- regression/cbmc/String5/test.desc | 2 +- regression/cbmc/String7/test.desc | 2 +- regression/cbmc/String_Abstraction1/test.desc | 2 +- regression/cbmc/String_Abstraction11/test.desc | 2 +- regression/cbmc/String_Abstraction12/test.desc | 2 +- regression/cbmc/String_Abstraction14/test.desc | 2 +- regression/cbmc/String_Abstraction15/test.desc | 2 +- regression/cbmc/String_Abstraction19/test.desc | 2 +- regression/cbmc/String_Abstraction2/test.desc | 2 +- regression/cbmc/String_Abstraction20/test.desc | 2 +- regression/cbmc/String_Abstraction22/test.desc | 2 +- regression/cbmc/String_Abstraction23/test.desc | 2 +- regression/cbmc/String_Abstraction3/test.desc | 2 +- regression/cbmc/String_Abstraction8/test.desc | 2 +- regression/cbmc/String_Abstraction9/test.desc | 2 +- regression/cbmc/Type_Error1/test.desc | 2 +- regression/cbmc/Typecast1/test.desc | 2 +- regression/cbmc/Typecast2/test.desc | 2 +- regression/cbmc/Typecast3/test.desc | 2 +- regression/cbmc/Unbounded_Array1/test.desc | 2 +- regression/cbmc/Unbounded_Array2/test.desc | 2 +- regression/cbmc/Unbounded_Array3/test.desc | 2 +- regression/cbmc/Unbounded_Array4/test.desc | 2 +- regression/cbmc/Unbounded_Array5/test.desc | 2 +- regression/cbmc/Undefined_Function1/test.desc | 2 +- regression/cbmc/Undefined_Function2/test.desc | 2 +- regression/cbmc/Undefined_Shift1/test.desc | 2 +- regression/cbmc/Unwinding_Locality1/test.desc | 2 +- regression/cbmc/Variadic1/test.desc | 2 +- regression/cbmc/Visual_Studio_Types1/test.desc | 2 +- regression/cbmc/Visual_Studio_Types2/test.desc | 2 +- regression/cbmc/Zero_Initialization1/test.desc | 2 +- regression/cbmc/__func__1/test.desc | 2 +- regression/cbmc/always_inline2/test.desc | 2 +- regression/cbmc/always_inline3/test.desc | 2 +- regression/cbmc/apply_condition1/test.desc | 2 +- regression/cbmc/argc-and-argv/argc1.desc | 2 +- regression/cbmc/argc-and-argv/argv1.desc | 2 +- regression/cbmc/argv2/test.desc | 2 +- regression/cbmc/array-cell-sensitivity1/test_execution.desc | 2 +- regression/cbmc/array-cell-sensitivity11/test.desc | 2 +- regression/cbmc/array-cell-sensitivity13/test.desc | 2 +- regression/cbmc/array-cell-sensitivity14/test.desc | 2 +- regression/cbmc/array-cell-sensitivity15/test.desc | 2 +- regression/cbmc/array-cell-sensitivity2/test.desc | 2 +- regression/cbmc/array-cell-sensitivity2/test_execution.desc | 2 +- regression/cbmc/array-cell-sensitivity3/test_execution.desc | 2 +- regression/cbmc/array-cell-sensitivity4/test_execution.desc | 2 +- regression/cbmc/array-cell-sensitivity5/test_execution.desc | 2 +- regression/cbmc/array-cell-sensitivity6/test_execution.desc | 2 +- regression/cbmc/array-constraint/test.desc | 2 +- regression/cbmc/array-constraint/test_xml.desc | 2 +- regression/cbmc/array-tests/test.desc | 2 +- regression/cbmc/array-tests/uf-always.desc | 2 +- regression/cbmc/array-tests/zero-sized.desc | 2 +- regression/cbmc/assert_rtn_four/test.desc | 2 +- .../assigning_nullpointers_should_not_crash_symex/test.desc | 2 +- regression/cbmc/atomic_X_fetch-1/pointer.desc | 2 +- regression/cbmc/atomic_X_fetch-1/test.desc | 2 +- regression/cbmc/atomic_X_fetch-1/two.desc | 2 +- regression/cbmc/atomic_fetch_X-1/pointer.desc | 2 +- regression/cbmc/atomic_fetch_X-1/two.desc | 2 +- regression/cbmc/atomic_load_store-1/test.desc | 2 +- regression/cbmc/bad_option/test.desc | 2 +- regression/cbmc/bad_option/test_multiple.desc | 2 +- regression/cbmc/big-endian-array1/test.desc | 2 +- regression/cbmc/bounds_check2/test.desc | 2 +- regression/cbmc/byte-op-metric/test.desc | 2 +- regression/cbmc/byte-op-metric/test_json.desc | 2 +- regression/cbmc/byte_update1/test.desc | 2 +- regression/cbmc/byte_update10/test.desc | 2 +- regression/cbmc/byte_update2/test.desc | 2 +- regression/cbmc/byte_update3/test.desc | 2 +- regression/cbmc/byte_update4/test.desc | 2 +- regression/cbmc/byte_update5/full-slice.desc | 2 +- regression/cbmc/byte_update5/test.desc | 2 +- regression/cbmc/byte_update6/test.desc | 2 +- regression/cbmc/byte_update7/test.desc | 2 +- regression/cbmc/byte_update8/test.desc | 2 +- regression/cbmc/byte_update9/test.desc | 2 +- regression/cbmc/character_handling1/test.desc | 2 +- regression/cbmc/clang_builtins/bitreverse-typeconflict.desc | 2 +- regression/cbmc/comma1/test.desc | 2 +- regression/cbmc/compound-assignment/compound_promotion.desc | 2 +- regression/cbmc/compound_literal1/test.desc | 2 +- regression/cbmc/condition-propagation-1/test.desc | 2 +- regression/cbmc/condition-propagation-2/test.desc | 2 +- regression/cbmc/condition-propagation-3/test.desc | 2 +- regression/cbmc/condition-propagation-4/test.desc | 2 +- regression/cbmc/const_ptr1/test.desc | 2 +- regression/cbmc/constant_folding1/test.desc | 2 +- regression/cbmc/constant_folding2/test.desc | 2 +- regression/cbmc/constructor1/test.desc | 2 +- .../cbmc/cover-failed-assertions/test-no-failed-assertions.desc | 2 +- regression/cbmc/cover-failed-assertions/test.desc | 2 +- regression/cbmc/coverage_report1/paths.desc | 2 +- regression/cbmc/coverage_report1/test.desc | 2 +- regression/cbmc/cprover_bool1/test.desc | 2 +- regression/cbmc/cprover_fence_one/test.desc | 2 +- regression/cbmc/cprover_havoc_object_one/test.desc | 2 +- regression/cbmc/cprover_id1/test.desc | 2 +- regression/cbmc/cprover_postcondition/test.desc | 2 +- regression/cbmc/cprover_precondition/test.desc | 2 +- regression/cbmc/dereference-cache-flag/test-no-cache.desc | 2 +- regression/cbmc/dereference-cache-flag/test-with-cache.desc | 2 +- regression/cbmc/destructor1/test.desc | 2 +- regression/cbmc/destructors/compound_literal.desc | 2 +- regression/cbmc/destructors/enter_lexical_block.desc | 2 +- regression/cbmc/double_deref/double_deref.desc | 2 +- regression/cbmc/double_deref/double_deref_single_alias.desc | 2 +- regression/cbmc/double_deref/double_deref_with_cast.desc | 2 +- .../cbmc/double_deref/double_deref_with_cast_single_alias.desc | 2 +- regression/cbmc/double_deref/double_deref_with_member.desc | 2 +- .../double_deref/double_deref_with_member_single_alias.desc | 2 +- .../cbmc/double_deref/double_deref_with_pointer_arithmetic.desc | 2 +- regression/cbmc/dynamic_size1/test.desc | 2 +- regression/cbmc/dynamic_sizeof1/test.desc | 2 +- regression/cbmc/enum1/test.desc | 2 +- regression/cbmc/enum2/test.desc | 2 +- regression/cbmc/enum4/test.desc | 2 +- regression/cbmc/enum6/test.desc | 2 +- regression/cbmc/enum7/test.desc | 2 +- regression/cbmc/enum8/test.desc | 2 +- regression/cbmc/enum_is_in_range/enum_test3-simplified.desc | 2 +- regression/cbmc/enum_is_in_range/enum_test3.desc | 2 +- regression/cbmc/enum_is_in_range/enum_test7.desc | 2 +- regression/cbmc/enum_is_in_range/format.desc | 2 +- regression/cbmc/enum_is_in_range/no_duplicate.desc | 2 +- regression/cbmc/enum_underlying_type_01/test.desc | 2 +- regression/cbmc/enum_underlying_type_02/test.desc | 2 +- regression/cbmc/enum_underlying_type_03/test.desc | 2 +- regression/cbmc/equality_through_array1/test.desc | 2 +- regression/cbmc/equality_through_array2/test.desc | 2 +- regression/cbmc/equality_through_array3/test.desc | 2 +- regression/cbmc/equality_through_array4/test.desc | 2 +- regression/cbmc/equality_through_array5/test.desc | 2 +- regression/cbmc/equality_through_array6/test.desc | 2 +- regression/cbmc/extern1/test.desc | 2 +- regression/cbmc/extern2/test.desc | 2 +- regression/cbmc/extern3/test.desc | 2 +- regression/cbmc/extern4/test.desc | 2 +- regression/cbmc/extern5/test.desc | 2 +- regression/cbmc/extern_initialization1/test.desc | 2 +- regression/cbmc/extern_initialization2/test.desc | 2 +- regression/cbmc/field-sensitivity10/test.desc | 2 +- regression/cbmc/field-sensitivity14/test.desc | 2 +- regression/cbmc/field-sensitivity6/test.desc | 2 +- regression/cbmc/field-sensitivity7/test.desc | 2 +- regression/cbmc/field-sensitivity8/test.desc | 2 +- regression/cbmc/for-break1/test.desc | 2 +- regression/cbmc/full_slice3/test.desc | 2 +- regression/cbmc/function-return-no-body1/test.desc | 2 +- regression/cbmc/function_option1/test.desc | 2 +- regression/cbmc/gcc_attribute_alias1/test.desc | 2 +- regression/cbmc/gcc_builtin_add_overflow/type-conflict-2.desc | 2 +- regression/cbmc/gcc_builtin_add_overflow/type-conflict.desc | 2 +- regression/cbmc/gcc_builtin_va_arg_one/test.desc | 2 +- regression/cbmc/gcc_c99-bool-1/test.desc | 2 +- regression/cbmc/gcc_conditional_expr1/test.desc | 2 +- regression/cbmc/gcc_local_label1/test.desc | 2 +- regression/cbmc/gcc_statement_expression1/test.desc | 2 +- regression/cbmc/gcc_statement_expression2/test.desc | 2 +- regression/cbmc/gcc_statement_expression3/test.desc | 2 +- regression/cbmc/gcc_statement_expression4/test.desc | 2 +- regression/cbmc/gcc_statement_expression5/test.desc | 2 +- regression/cbmc/gcc_switch_case_range1/test.desc | 2 +- regression/cbmc/gcc_switch_case_range2/test.desc | 2 +- regression/cbmc/gcc_vector2/test.desc | 2 +- regression/cbmc/gcc_vector3/test.desc | 2 +- regression/cbmc/goto2/test.desc | 2 +- regression/cbmc/goto3/test.desc | 2 +- regression/cbmc/goto5/test.desc | 2 +- regression/cbmc/havoc_slice/test_array_slice_1.desc | 2 +- regression/cbmc/havoc_slice/test_array_slice_2.desc | 2 +- regression/cbmc/havoc_slice/test_whole_array.desc | 2 +- regression/cbmc/havoc_slice/test_whole_array_with_offset.desc | 2 +- regression/cbmc/havoc_slice_checks/full-slice.desc | 2 +- regression/cbmc/havoc_undefined_functions/test.desc | 2 +- regression/cbmc/hex_string1/test.desc | 2 +- regression/cbmc/if2/test.desc | 2 +- regression/cbmc/incomplete-sizeof/array.desc | 2 +- regression/cbmc/incomplete-sizeof/enum.desc | 2 +- regression/cbmc/incomplete-sizeof/struct.desc | 2 +- regression/cbmc/incomplete-sizeof/union.desc | 2 +- regression/cbmc/incomplete-structs/test.desc | 2 +- .../cbmc/inequality-with-constant-normalisation/test.desc | 2 +- .../cbmc/inequality-with-constant-normalisation1/test.desc | 2 +- regression/cbmc/inline1/test.desc | 2 +- regression/cbmc/integer-assignments1/integer-typecheck.desc | 2 +- .../cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc | 2 +- regression/cbmc/json-interface1/test.desc | 2 +- regression/cbmc/json-interface1/test_wrong_flag.desc | 2 +- regression/cbmc/json-interface1/test_wrong_option.desc | 2 +- regression/cbmc/json-ui/no_entry.desc | 2 +- regression/cbmc/json-ui/syntax_error.desc | 2 +- regression/cbmc/json1/test.desc | 2 +- regression/cbmc/link_json_symtabs/test.desc | 2 +- regression/cbmc/little-endian-array1/test.desc | 2 +- regression/cbmc/locations1/test.desc | 2 +- regression/cbmc/loophead-trace/test-json.desc | 2 +- regression/cbmc/loophead-trace/test-xml.desc | 2 +- regression/cbmc/malloc-may-fail/test.desc | 2 +- regression/cbmc/malloc-may-fail/test_without_option.desc | 2 +- regression/cbmc/malloc-too-large/largest_representable.desc | 2 +- regression/cbmc/malloc-too-large/max_size.desc | 2 +- regression/cbmc/malloc-too-large/one_byte_too_large.desc | 2 +- regression/cbmc/member1/test.desc | 2 +- regression/cbmc/memory_allocation1/test.desc | 2 +- regression/cbmc/memory_allocation2/test.desc | 2 +- regression/cbmc/memset2/test.desc | 2 +- regression/cbmc/memset3/test.desc | 2 +- regression/cbmc/mm_io1/test.desc | 2 +- regression/cbmc/nested_label1/test.desc | 2 +- regression/cbmc/nondet-pointer/nondet-pointer1.desc | 2 +- regression/cbmc/nondet-pointer/nondet-pointer2.desc | 2 +- regression/cbmc/nondet-pointer/nondet-pointer3.desc | 2 +- regression/cbmc/nondet-pointer/nondet-pointer4.desc | 2 +- regression/cbmc/nondet-pointer/nondet-pointer5.desc | 2 +- regression/cbmc/noop2/test.desc | 2 +- regression/cbmc/null2/test.desc | 2 +- regression/cbmc/null3/test.desc | 2 +- regression/cbmc/null5/test.desc | 2 +- regression/cbmc/null6/test.desc | 2 +- regression/cbmc/null7/test.desc | 2 +- regression/cbmc/object-bits-parsing/non_numeric.desc | 2 +- regression/cbmc/object-bits-parsing/too_large.desc | 2 +- regression/cbmc/object-bits-parsing/valid.desc | 2 +- regression/cbmc/object-bits-parsing/zero.desc | 2 +- regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc | 2 +- regression/cbmc/path-branch-pointer-call/test.desc | 2 +- regression/cbmc/path-per-path-vccs/test.desc | 2 +- regression/cbmc/phi-merge_uninitialized_values/dynamic.desc | 2 +- regression/cbmc/phi-merge_uninitialized_values/global.desc | 2 +- regression/cbmc/phi-merge_uninitialized_values/local.desc | 2 +- .../cbmc/phi-merge_uninitialized_values/static_local.desc | 2 +- regression/cbmc/pointer-check-01/test.desc | 2 +- regression/cbmc/pointer-check-02/test.desc | 2 +- regression/cbmc/pointer-extra-checks/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- regression/cbmc/pointer-function-parameters/test.desc | 2 +- regression/cbmc/pointer-predicates/at_bounds1.desc | 2 +- regression/cbmc/pointer-predicates/in_range1.desc | 2 +- regression/cbmc/pointer-primitive-check-01/test.desc | 2 +- regression/cbmc/pointer-primitive-check-02/test.desc | 2 +- regression/cbmc/pointer-primitive-check-04/test.desc | 2 +- regression/cbmc/points-to-sets/test_json.desc | 2 +- regression/cbmc/points-to-sets/test_xml.desc | 2 +- regression/cbmc/pragma_cprover1/test.desc | 2 +- regression/cbmc/pragma_cprover3/test.desc | 2 +- regression/cbmc/pragma_cprover_enable1/test.desc | 2 +- regression/cbmc/pragma_cprover_enable2/test.desc | 2 +- regression/cbmc/pragma_cprover_enable3/test.desc | 2 +- .../cbmc/pragma_cprover_enable_disable_global_off/test.desc | 2 +- .../cbmc/pragma_cprover_enable_disable_global_on/test.desc | 2 +- .../cbmc/pragma_cprover_enable_disable_multiple/test.desc | 2 +- regression/cbmc/r_w_ok1/test.desc | 2 +- regression/cbmc/r_w_ok10/test.desc | 2 +- regression/cbmc/r_w_ok2/test.desc | 2 +- regression/cbmc/r_w_ok5/test.desc | 2 +- regression/cbmc/r_w_ok6/test.desc | 2 +- regression/cbmc/r_w_ok7/test.desc | 2 +- regression/cbmc/r_w_ok8/test.desc | 2 +- regression/cbmc/r_w_ok9/simplify.desc | 2 +- regression/cbmc/r_w_ok9/test.desc | 2 +- regression/cbmc/reachability-slice-interproc/test.desc | 2 +- regression/cbmc/reachability-slice-interproc2/test.desc | 2 +- regression/cbmc/reachability-slice-interproc3/test.desc | 2 +- regression/cbmc/reachability-slice/test.desc | 2 +- regression/cbmc/reachability-slice/test2.desc | 2 +- regression/cbmc/reachability-slice/test3.desc | 2 +- .../realloc-should-not-free-on-failure-to-allocate/test.desc | 2 +- regression/cbmc/residual-guards-1/test.desc | 2 +- regression/cbmc/residual-guards-1/test_execution.desc | 2 +- regression/cbmc/residual-guards-2/test.desc | 2 +- regression/cbmc/residual-guards-2/test_execution.desc | 2 +- regression/cbmc/residual-guards-3/test.desc | 2 +- regression/cbmc/residual-guards-3/test_execution.desc | 2 +- regression/cbmc/residual-guards-4/test.desc | 2 +- regression/cbmc/residual-guards-4/test_execution.desc | 2 +- regression/cbmc/return2/test.desc | 2 +- regression/cbmc/return3/full-slice.desc | 2 +- regression/cbmc/return6/test.desc | 2 +- regression/cbmc/return7/test.desc | 2 +- regression/cbmc/return8/test.desc | 2 +- regression/cbmc/return9/test.desc | 2 +- regression/cbmc/runtime-profiling/test.desc | 2 +- regression/cbmc/saturating_arithmetric/output-formula.desc | 2 +- regression/cbmc/saturating_arithmetric/output-goto.desc | 2 +- regression/cbmc/saturating_arithmetric/typeconflict.desc | 2 +- regression/cbmc/self_loops_to_assumptions1/default.desc | 2 +- regression/cbmc/self_loops_to_assumptions1/no-assume.desc | 2 +- .../false_implies_failure_side_effect.desc | 2 +- .../cbmc/short_circuit_implies/short-circuit-memory-checks.desc | 2 +- .../short_circuit_implies/true_implies_failure_side_effect.desc | 2 +- regression/cbmc/show-vcc/test.desc | 2 +- regression/cbmc/show_properties1/test.desc | 2 +- regression/cbmc/simplify-full-test/test.desc | 2 +- .../cbmc/simplify-function-call-array-element-pointer/test.desc | 2 +- regression/cbmc/simplify-function-call-array-pointer/test.desc | 2 +- regression/cbmc/simplify-function-call-pointer-access/test.desc | 2 +- regression/cbmc/simplify-global-array-access/test.desc | 2 +- regression/cbmc/simplify-local-array-access/test.desc | 2 +- regression/cbmc/simplify-pointer-access/test.desc | 2 +- regression/cbmc/simplify-union/test.desc | 2 +- regression/cbmc/stack-trace/test.desc | 2 +- regression/cbmc/string_assignment1/test.desc | 2 +- regression/cbmc/switch1/test.desc | 2 +- regression/cbmc/switch2/test.desc | 2 +- regression/cbmc/switch3/test.desc | 2 +- regression/cbmc/switch4/test.desc | 2 +- regression/cbmc/switch5/test.desc | 2 +- regression/cbmc/switch6/test.desc | 2 +- regression/cbmc/switch7/test.desc | 2 +- regression/cbmc/switch8/program-only.desc | 2 +- regression/cbmc/switch8/test.desc | 2 +- regression/cbmc/switch9/test.desc | 2 +- regression/cbmc/sync_X_and_fetch-1/pointer.desc | 2 +- regression/cbmc/sync_X_and_fetch-1/test.desc | 2 +- regression/cbmc/sync_X_and_fetch-1/two.desc | 2 +- regression/cbmc/sync_bool_compare-1/pointer.desc | 2 +- regression/cbmc/sync_bool_compare-1/test.desc | 2 +- regression/cbmc/sync_bool_compare-1/three.desc | 2 +- regression/cbmc/sync_fetch_and_X-1/pointer.desc | 2 +- regression/cbmc/sync_fetch_and_X-1/test.desc | 2 +- regression/cbmc/sync_fetch_and_X-1/two.desc | 2 +- regression/cbmc/sync_lock_release-1/symbol_per_type.desc | 2 +- regression/cbmc/sync_lock_release-1/test.desc | 2 +- regression/cbmc/sync_val_compare-1/pointer.desc | 2 +- regression/cbmc/sync_val_compare-1/test.desc | 2 +- regression/cbmc/sync_val_compare-1/three.desc | 2 +- regression/cbmc/trace_options_json_extended/extended.desc | 2 +- regression/cbmc/trace_options_json_extended/non-extended.desc | 2 +- regression/cbmc/ts18661_typedefs/test.desc | 2 +- regression/cbmc/typedef-anon-struct1/test.desc | 2 +- regression/cbmc/typedef-anon-struct2/test.desc | 2 +- regression/cbmc/typedef-anon-union1/test.desc | 2 +- regression/cbmc/typedef-anon-union2/test.desc | 2 +- regression/cbmc/typedef-const-struct1/test.desc | 2 +- regression/cbmc/typedef-const-type1/test.desc | 2 +- regression/cbmc/typedef-const-union1/test.desc | 2 +- regression/cbmc/typedef-param-anon-struct1/test.desc | 2 +- regression/cbmc/typedef-param-anon-union1/test.desc | 2 +- regression/cbmc/typedef-param-struct1/test.desc | 2 +- regression/cbmc/typedef-param-type1/test.desc | 2 +- regression/cbmc/typedef-param-type2/test.desc | 2 +- regression/cbmc/typedef-param-type3/test.desc | 2 +- regression/cbmc/typedef-param-union1/test.desc | 2 +- regression/cbmc/typedef-struct1/test.desc | 2 +- regression/cbmc/typedef-struct2/test.desc | 2 +- regression/cbmc/typedef-type1/test.desc | 2 +- regression/cbmc/typedef-type2/test.desc | 2 +- regression/cbmc/typedef-type3/test.desc | 2 +- regression/cbmc/typedef-type4/test.desc | 2 +- regression/cbmc/typedef-union1/test.desc | 2 +- regression/cbmc/typedef-union2/test.desc | 2 +- regression/cbmc/uncaught_exceptions_analysis1/test.desc | 2 +- regression/cbmc/uniform_array1/test.desc | 2 +- regression/cbmc/unknown-argument-suggestion/test.desc | 2 +- regression/cbmc/unreachable-goto1/test-vccs.desc | 2 +- regression/cbmc/unreachable-goto1/test.desc | 2 +- regression/cbmc/unreachable-goto2/test-vccs.desc | 2 +- regression/cbmc/unreachable-goto2/test.desc | 2 +- regression/cbmc/unreachable-goto3/test-vccs.desc | 2 +- regression/cbmc/unreachable-goto3/test.desc | 2 +- regression/cbmc/unreachable-goto4/test-vccs.desc | 2 +- regression/cbmc/unreachable-goto4/test.desc | 2 +- regression/cbmc/unreachable-goto5/test-vccs.desc | 2 +- regression/cbmc/unreachable-goto5/test.desc | 2 +- regression/cbmc/unreachable-goto6/test-vccs.desc | 2 +- regression/cbmc/unreachable-goto6/test.desc | 2 +- regression/cbmc/unsigned1/test.desc | 2 +- regression/cbmc/unsigned___int128/test.desc | 2 +- regression/cbmc/unsigned_char1/test.desc | 2 +- regression/cbmc/unwind_counters1/test.desc | 2 +- regression/cbmc/unwind_counters2/test.desc | 2 +- regression/cbmc/unwind_counters3/test.desc | 2 +- regression/cbmc/unwind_counters4/test.desc | 2 +- regression/cbmc/unwinding_assertions1/test.desc | 2 +- regression/cbmc/unwindset1/label.desc | 2 +- regression/cbmc/unwindset1/test.desc | 2 +- regression/cbmc/unwindset2/test.desc | 2 +- regression/cbmc/va_list1/test.desc | 2 +- regression/cbmc/va_list2/test.desc | 2 +- regression/cbmc/va_list4/test.desc | 2 +- regression/cbmc/variable-access-to-constant-array/test.desc | 2 +- regression/cbmc/verifier_assume_one/test.desc | 2 +- regression/cbmc/verifier_error_lhs/test.desc | 2 +- regression/cbmc/verifier_error_zero/test.desc | 2 +- regression/cbmc/vla1/program-only.desc | 2 +- regression/cbmc/void_ifthenelse/test.desc | 2 +- regression/cbmc/while1/test.desc | 2 +- regression/cbmc/while2/requires-transform.desc | 2 +- regression/cbmc/while2/test.desc | 2 +- regression/cbmc/xml-escaping/debug_output.desc | 2 +- regression/cbmc/xml-interface1/test.desc | 2 +- regression/cbmc/xml-interface1/test_wrong_flag.desc | 2 +- regression/cbmc/xml-interface1/test_wrong_option.desc | 2 +- regression/cbmc/z3/invalid.desc | 2 +- regression/cbmc/z3/valid.desc | 2 +- 592 files changed, 592 insertions(+), 592 deletions(-) diff --git a/regression/cbmc/ACSL/quantifier-precedence.desc b/regression/cbmc/ACSL/quantifier-precedence.desc index 36922c52380..82d82540504 100644 --- a/regression/cbmc/ACSL/quantifier-precedence.desc +++ b/regression/cbmc/ACSL/quantifier-precedence.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend quantifier-precedence.c ^EXIT=0$ diff --git a/regression/cbmc/ASHR1/test.desc b/regression/cbmc/ASHR1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/ASHR1/test.desc +++ b/regression/cbmc/ASHR1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Address_of1/test.desc b/regression/cbmc/Address_of1/test.desc index d891ef29be9..d18a7f927da 100644 --- a/regression/cbmc/Address_of1/test.desc +++ b/regression/cbmc/Address_of1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --stop-on-fail ^\[main\.assertion diff --git a/regression/cbmc/Address_of2/test.desc b/regression/cbmc/Address_of2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Address_of2/test.desc +++ b/regression/cbmc/Address_of2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Access1/test.desc b/regression/cbmc/Array_Access1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Array_Access1/test.desc +++ b/regression/cbmc/Array_Access1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Access2/test.desc b/regression/cbmc/Array_Access2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Array_Access2/test.desc +++ b/regression/cbmc/Array_Access2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Access3/test.desc b/regression/cbmc/Array_Access3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Array_Access3/test.desc +++ b/regression/cbmc/Array_Access3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Initialization1/test.desc b/regression/cbmc/Array_Initialization1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Array_Initialization1/test.desc +++ b/regression/cbmc/Array_Initialization1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Initialization2/test.desc b/regression/cbmc/Array_Initialization2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Array_Initialization2/test.desc +++ b/regression/cbmc/Array_Initialization2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Initialization3/test.desc b/regression/cbmc/Array_Initialization3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Array_Initialization3/test.desc +++ b/regression/cbmc/Array_Initialization3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Pointer1/test.desc b/regression/cbmc/Array_Pointer1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Array_Pointer1/test.desc +++ b/regression/cbmc/Array_Pointer1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Pointer2/test.desc b/regression/cbmc/Array_Pointer2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Array_Pointer2/test.desc +++ b/regression/cbmc/Array_Pointer2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Pointer3/test.desc b/regression/cbmc/Array_Pointer3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Array_Pointer3/test.desc +++ b/regression/cbmc/Array_Pointer3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Pointer4/test.desc b/regression/cbmc/Array_Pointer4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Array_Pointer4/test.desc +++ b/regression/cbmc/Array_Pointer4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Pointer5/test.desc b/regression/cbmc/Array_Pointer5/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Array_Pointer5/test.desc +++ b/regression/cbmc/Array_Pointer5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Pointer6/test.desc b/regression/cbmc/Array_Pointer6/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Array_Pointer6/test.desc +++ b/regression/cbmc/Array_Pointer6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Pointer7/test.desc b/regression/cbmc/Array_Pointer7/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Array_Pointer7/test.desc +++ b/regression/cbmc/Array_Pointer7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_Propagation1/test.desc b/regression/cbmc/Array_Propagation1/test.desc index c7996d86f9f..1880bbb5b32 100644 --- a/regression/cbmc/Array_Propagation1/test.desc +++ b/regression/cbmc/Array_Propagation1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Array_UF1/test.desc b/regression/cbmc/Array_UF1/test.desc index 61e3418f5e6..b87b796089e 100644 --- a/regression/cbmc/Array_UF1/test.desc +++ b/regression/cbmc/Array_UF1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 11 ^EXIT=0$ diff --git a/regression/cbmc/Array_UF10/test.desc b/regression/cbmc/Array_UF10/test.desc index a74140bd6ed..84d4733c0c3 100644 --- a/regression/cbmc/Array_UF10/test.desc +++ b/regression/cbmc/Array_UF10/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 1 ^EXIT=0$ diff --git a/regression/cbmc/Array_UF11/test.desc b/regression/cbmc/Array_UF11/test.desc index c4496ea4fd2..e231e47ae69 100644 --- a/regression/cbmc/Array_UF11/test.desc +++ b/regression/cbmc/Array_UF11/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 1 ^EXIT=10$ diff --git a/regression/cbmc/Array_UF12/test.desc b/regression/cbmc/Array_UF12/test.desc index 09c3a6e12da..618dd4be233 100644 --- a/regression/cbmc/Array_UF12/test.desc +++ b/regression/cbmc/Array_UF12/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 2 ^EXIT=10$ diff --git a/regression/cbmc/Array_UF13/test.desc b/regression/cbmc/Array_UF13/test.desc index a74140bd6ed..84d4733c0c3 100644 --- a/regression/cbmc/Array_UF13/test.desc +++ b/regression/cbmc/Array_UF13/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 1 ^EXIT=0$ diff --git a/regression/cbmc/Array_UF14/test.desc b/regression/cbmc/Array_UF14/test.desc index 2a5c51a9f90..2569d3b97ff 100644 --- a/regression/cbmc/Array_UF14/test.desc +++ b/regression/cbmc/Array_UF14/test.desc @@ -1,4 +1,4 @@ -CORE thorough-paths +CORE thorough-paths new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 6 ^EXIT=10$ diff --git a/regression/cbmc/Array_UF15/test.desc b/regression/cbmc/Array_UF15/test.desc index 15690b94615..074b36a4a1b 100644 --- a/regression/cbmc/Array_UF15/test.desc +++ b/regression/cbmc/Array_UF15/test.desc @@ -1,4 +1,4 @@ -CORE thorough-paths +CORE thorough-paths new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 11 ^EXIT=0$ diff --git a/regression/cbmc/Array_UF16/test.desc b/regression/cbmc/Array_UF16/test.desc index 09c3a6e12da..618dd4be233 100644 --- a/regression/cbmc/Array_UF16/test.desc +++ b/regression/cbmc/Array_UF16/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 2 ^EXIT=10$ diff --git a/regression/cbmc/Array_UF17/test.desc b/regression/cbmc/Array_UF17/test.desc index e9939c1e8c3..4ba91617222 100644 --- a/regression/cbmc/Array_UF17/test.desc +++ b/regression/cbmc/Array_UF17/test.desc @@ -1,4 +1,4 @@ -CORE thorough-paths +CORE thorough-paths new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 9 ^EXIT=0$ diff --git a/regression/cbmc/Array_UF18/test.desc b/regression/cbmc/Array_UF18/test.desc index 61e3418f5e6..b87b796089e 100644 --- a/regression/cbmc/Array_UF18/test.desc +++ b/regression/cbmc/Array_UF18/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 11 ^EXIT=0$ diff --git a/regression/cbmc/Array_UF19/test.desc b/regression/cbmc/Array_UF19/test.desc index d92ab778129..e22d35d5205 100644 --- a/regression/cbmc/Array_UF19/test.desc +++ b/regression/cbmc/Array_UF19/test.desc @@ -1,4 +1,4 @@ -CORE thorough-paths +CORE thorough-paths new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 3 ^EXIT=10$ diff --git a/regression/cbmc/Array_UF2/test.desc b/regression/cbmc/Array_UF2/test.desc index ebecd288e48..a3e52fdd404 100644 --- a/regression/cbmc/Array_UF2/test.desc +++ b/regression/cbmc/Array_UF2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 5 ^EXIT=0$ diff --git a/regression/cbmc/Array_UF20/test.desc b/regression/cbmc/Array_UF20/test.desc index fa4e310b875..d6516a4f9b2 100644 --- a/regression/cbmc/Array_UF20/test.desc +++ b/regression/cbmc/Array_UF20/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 12 ^EXIT=10$ diff --git a/regression/cbmc/Array_UF21/test.desc b/regression/cbmc/Array_UF21/test.desc index e9d3c4ebe15..8d4a044d982 100644 --- a/regression/cbmc/Array_UF21/test.desc +++ b/regression/cbmc/Array_UF21/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --bounds-check ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Array_UF3/test.desc b/regression/cbmc/Array_UF3/test.desc index 912cf6019b0..a55860596c0 100644 --- a/regression/cbmc/Array_UF3/test.desc +++ b/regression/cbmc/Array_UF3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 3 --no-unwinding-assertions ^EXIT=10$ diff --git a/regression/cbmc/Array_UF5/test.desc b/regression/cbmc/Array_UF5/test.desc index 09c3a6e12da..618dd4be233 100644 --- a/regression/cbmc/Array_UF5/test.desc +++ b/regression/cbmc/Array_UF5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 2 ^EXIT=10$ diff --git a/regression/cbmc/Array_UF6/test.desc b/regression/cbmc/Array_UF6/test.desc index d92ab778129..e22d35d5205 100644 --- a/regression/cbmc/Array_UF6/test.desc +++ b/regression/cbmc/Array_UF6/test.desc @@ -1,4 +1,4 @@ -CORE thorough-paths +CORE thorough-paths new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 3 ^EXIT=10$ diff --git a/regression/cbmc/Array_UF7/test.desc b/regression/cbmc/Array_UF7/test.desc index c47f81c71cc..5c423a157a9 100644 --- a/regression/cbmc/Array_UF7/test.desc +++ b/regression/cbmc/Array_UF7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 3 ^EXIT=10$ diff --git a/regression/cbmc/Array_UF9/test.desc b/regression/cbmc/Array_UF9/test.desc index b3db38477ee..abec3deb3e4 100644 --- a/regression/cbmc/Array_UF9/test.desc +++ b/regression/cbmc/Array_UF9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --arrays-uf-always --no-propagation --refine-arrays --unwind 21 ^EXIT=10$ diff --git a/regression/cbmc/BV_Arithmetic1/test.desc b/regression/cbmc/BV_Arithmetic1/test.desc index 33900ad2b78..82568cfc082 100644 --- a/regression/cbmc/BV_Arithmetic1/test.desc +++ b/regression/cbmc/BV_Arithmetic1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/BV_Arithmetic2/test.desc b/regression/cbmc/BV_Arithmetic2/test.desc index 23e981a3744..baa24854523 100644 --- a/regression/cbmc/BV_Arithmetic2/test.desc +++ b/regression/cbmc/BV_Arithmetic2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 32 ^EXIT=0$ diff --git a/regression/cbmc/BV_Arithmetic3/test.desc b/regression/cbmc/BV_Arithmetic3/test.desc index d2a7e3e7574..00f3ce2d93a 100644 --- a/regression/cbmc/BV_Arithmetic3/test.desc +++ b/regression/cbmc/BV_Arithmetic3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/BV_Arithmetic4/test.desc b/regression/cbmc/BV_Arithmetic4/test.desc index 23e981a3744..baa24854523 100644 --- a/regression/cbmc/BV_Arithmetic4/test.desc +++ b/regression/cbmc/BV_Arithmetic4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 32 ^EXIT=0$ diff --git a/regression/cbmc/BV_Arithmetic5/test.desc b/regression/cbmc/BV_Arithmetic5/test.desc index 23e981a3744..baa24854523 100644 --- a/regression/cbmc/BV_Arithmetic5/test.desc +++ b/regression/cbmc/BV_Arithmetic5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 32 ^EXIT=0$ diff --git a/regression/cbmc/BV_Arithmetic6/test.desc b/regression/cbmc/BV_Arithmetic6/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/BV_Arithmetic6/test.desc +++ b/regression/cbmc/BV_Arithmetic6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Bitfields4/test.desc b/regression/cbmc/Bitfields4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Bitfields4/test.desc +++ b/regression/cbmc/Bitfields4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Bool/bool1.desc b/regression/cbmc/Bool/bool1.desc index 0638fdff0e6..b45c1b483af 100644 --- a/regression/cbmc/Bool/bool1.desc +++ b/regression/cbmc/Bool/bool1.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend bool1.c ^EXIT=0$ diff --git a/regression/cbmc/Bool/bool4.desc b/regression/cbmc/Bool/bool4.desc index 49b4f5e01d2..48975cb2285 100644 --- a/regression/cbmc/Bool/bool4.desc +++ b/regression/cbmc/Bool/bool4.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend bool4.c ^EXIT=0$ diff --git a/regression/cbmc/Bool/bool5-full-slice.desc b/regression/cbmc/Bool/bool5-full-slice.desc index 6fc49d6b0cf..c94ef40020a 100644 --- a/regression/cbmc/Bool/bool5-full-slice.desc +++ b/regression/cbmc/Bool/bool5-full-slice.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend bool5.c --full-slice Generated 4 VCC\(s\), 0 remaining after simplification diff --git a/regression/cbmc/Bool/bool5.desc b/regression/cbmc/Bool/bool5.desc index 273ab4b0ed7..ab32f527065 100644 --- a/regression/cbmc/Bool/bool5.desc +++ b/regression/cbmc/Bool/bool5.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend bool5.c Generated 4 VCC\(s\), 0 remaining after simplification diff --git a/regression/cbmc/Bool/bool6.desc b/regression/cbmc/Bool/bool6.desc index 59c4d81608f..cf5bb8c2839 100644 --- a/regression/cbmc/Bool/bool6.desc +++ b/regression/cbmc/Bool/bool6.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend bool6.c ^EXIT=0$ diff --git a/regression/cbmc/Boolean_Guards1/test.desc b/regression/cbmc/Boolean_Guards1/test.desc index da239c1965b..6e36fa13566 100644 --- a/regression/cbmc/Boolean_Guards1/test.desc +++ b/regression/cbmc/Boolean_Guards1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --bounds-check --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Division1/test.desc b/regression/cbmc/Division1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Division1/test.desc +++ b/regression/cbmc/Division1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Division2/test.desc b/regression/cbmc/Division2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Division2/test.desc +++ b/regression/cbmc/Division2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Ellipsis1/test.desc b/regression/cbmc/Ellipsis1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Ellipsis1/test.desc +++ b/regression/cbmc/Ellipsis1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Ellipsis2/test.desc b/regression/cbmc/Ellipsis2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Ellipsis2/test.desc +++ b/regression/cbmc/Ellipsis2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/End_thread1/test.desc b/regression/cbmc/End_thread1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/End_thread1/test.desc +++ b/regression/cbmc/End_thread1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Endianness1/test.desc b/regression/cbmc/Endianness1/test.desc index 217eac96e2f..91f07e669da 100644 --- a/regression/cbmc/Endianness1/test.desc +++ b/regression/cbmc/Endianness1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/Endianness2/test.desc b/regression/cbmc/Endianness2/test.desc index 4f2eebc5e15..c6c44885fb0 100644 --- a/regression/cbmc/Endianness2/test.desc +++ b/regression/cbmc/Endianness2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --big-endian ^EXIT=0$ diff --git a/regression/cbmc/Endianness3/test.desc b/regression/cbmc/Endianness3/test.desc index 217eac96e2f..91f07e669da 100644 --- a/regression/cbmc/Endianness3/test.desc +++ b/regression/cbmc/Endianness3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/Endianness4/test.desc b/regression/cbmc/Endianness4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Endianness4/test.desc +++ b/regression/cbmc/Endianness4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Endianness5/test.desc b/regression/cbmc/Endianness5/test.desc index 4e90da351ba..e15727d18a8 100644 --- a/regression/cbmc/Endianness5/test.desc +++ b/regression/cbmc/Endianness5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Endianness6/test.desc b/regression/cbmc/Endianness6/test.desc index 81ceb4c6dc0..9457c6a3fd8 100644 --- a/regression/cbmc/Endianness6/test.desc +++ b/regression/cbmc/Endianness6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --big-endian ^EXIT=0$ diff --git a/regression/cbmc/Endianness8/test.desc b/regression/cbmc/Endianness8/test.desc index 81ceb4c6dc0..9457c6a3fd8 100644 --- a/regression/cbmc/Endianness8/test.desc +++ b/regression/cbmc/Endianness8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --big-endian ^EXIT=0$ diff --git a/regression/cbmc/Endianness9/test.desc b/regression/cbmc/Endianness9/test.desc index 81ceb4c6dc0..9457c6a3fd8 100644 --- a/regression/cbmc/Endianness9/test.desc +++ b/regression/cbmc/Endianness9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --big-endian ^EXIT=0$ diff --git a/regression/cbmc/Error_Label1/test.desc b/regression/cbmc/Error_Label1/test.desc index e14ade773e5..16eda50f23d 100644 --- a/regression/cbmc/Error_Label1/test.desc +++ b/regression/cbmc/Error_Label1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --error-label ERROR ^EXIT=10$ diff --git a/regression/cbmc/Error_Label2/test.desc b/regression/cbmc/Error_Label2/test.desc index 3631d5c8930..9d238204565 100644 --- a/regression/cbmc/Error_Label2/test.desc +++ b/regression/cbmc/Error_Label2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --error-label ERROR --no-assertions ^EXIT=10$ diff --git a/regression/cbmc/Error_Label3/test.desc b/regression/cbmc/Error_Label3/test.desc index 450e47883c7..1328552a8c1 100644 --- a/regression/cbmc/Error_Label3/test.desc +++ b/regression/cbmc/Error_Label3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --error-label ERROR1 --error-label ERROR2 ^EXIT=10$ diff --git a/regression/cbmc/Eval_Order1/test.desc b/regression/cbmc/Eval_Order1/test.desc index 33900ad2b78..82568cfc082 100644 --- a/regression/cbmc/Eval_Order1/test.desc +++ b/regression/cbmc/Eval_Order1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Exceptions1/test.desc b/regression/cbmc/Exceptions1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Exceptions1/test.desc +++ b/regression/cbmc/Exceptions1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Failed_Symbols1/test.desc b/regression/cbmc/Failed_Symbols1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Failed_Symbols1/test.desc +++ b/regression/cbmc/Failed_Symbols1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Failing_Assert1/test.desc b/regression/cbmc/Failing_Assert1/test.desc index 3acca2686a9..169e04578ea 100644 --- a/regression/cbmc/Failing_Assert1/test.desc +++ b/regression/cbmc/Failing_Assert1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --verbosity 8 ^EXIT=10$ diff --git a/regression/cbmc/Free1/test.desc b/regression/cbmc/Free1/test.desc index 950f6791fef..25c4b7ecab8 100644 --- a/regression/cbmc/Free1/test.desc +++ b/regression/cbmc/Free1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/Free2/test.desc b/regression/cbmc/Free2/test.desc index caab5ef644d..7ded8494f5b 100644 --- a/regression/cbmc/Free2/test.desc +++ b/regression/cbmc/Free2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Free3/test.desc b/regression/cbmc/Free3/test.desc index 950f6791fef..25c4b7ecab8 100644 --- a/regression/cbmc/Free3/test.desc +++ b/regression/cbmc/Free3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/Free4/test.desc b/regression/cbmc/Free4/test.desc index 950f6791fef..25c4b7ecab8 100644 --- a/regression/cbmc/Free4/test.desc +++ b/regression/cbmc/Free4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/Function12/test.desc b/regression/cbmc/Function12/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Function12/test.desc +++ b/regression/cbmc/Function12/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Function2/test.desc b/regression/cbmc/Function2/test.desc index 33900ad2b78..82568cfc082 100644 --- a/regression/cbmc/Function2/test.desc +++ b/regression/cbmc/Function2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Function3/test.desc b/regression/cbmc/Function3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Function3/test.desc +++ b/regression/cbmc/Function3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Function4/test.desc b/regression/cbmc/Function4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Function4/test.desc +++ b/regression/cbmc/Function4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Function_Eval_Order2/test.desc b/regression/cbmc/Function_Eval_Order2/test.desc index 33900ad2b78..82568cfc082 100644 --- a/regression/cbmc/Function_Eval_Order2/test.desc +++ b/regression/cbmc/Function_Eval_Order2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Function_Pointer1/test.desc b/regression/cbmc/Function_Pointer1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Function_Pointer1/test.desc +++ b/regression/cbmc/Function_Pointer1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Function_Pointer10/test.desc b/regression/cbmc/Function_Pointer10/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Function_Pointer10/test.desc +++ b/regression/cbmc/Function_Pointer10/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Function_Pointer12/test.desc b/regression/cbmc/Function_Pointer12/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Function_Pointer12/test.desc +++ b/regression/cbmc/Function_Pointer12/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Function_Pointer13/test.desc b/regression/cbmc/Function_Pointer13/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Function_Pointer13/test.desc +++ b/regression/cbmc/Function_Pointer13/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Function_Pointer14/test.desc b/regression/cbmc/Function_Pointer14/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Function_Pointer14/test.desc +++ b/regression/cbmc/Function_Pointer14/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Function_Pointer16/test.desc b/regression/cbmc/Function_Pointer16/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Function_Pointer16/test.desc +++ b/regression/cbmc/Function_Pointer16/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Function_Pointer17/test.desc b/regression/cbmc/Function_Pointer17/test.desc index c0bbb27f448..ed5e26161dc 100644 --- a/regression/cbmc/Function_Pointer17/test.desc +++ b/regression/cbmc/Function_Pointer17/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 1 ^EXIT=0$ diff --git a/regression/cbmc/Function_Pointer18/test.desc b/regression/cbmc/Function_Pointer18/test.desc index 3cd78297904..386d294e198 100644 --- a/regression/cbmc/Function_Pointer18/test.desc +++ b/regression/cbmc/Function_Pointer18/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Function_Pointer19/test.desc b/regression/cbmc/Function_Pointer19/test.desc index 278f468e130..22961959ca9 100644 --- a/regression/cbmc/Function_Pointer19/test.desc +++ b/regression/cbmc/Function_Pointer19/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Function_Pointer4/test.desc b/regression/cbmc/Function_Pointer4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Function_Pointer4/test.desc +++ b/regression/cbmc/Function_Pointer4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Function_Pointer7/test.desc b/regression/cbmc/Function_Pointer7/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Function_Pointer7/test.desc +++ b/regression/cbmc/Function_Pointer7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc b/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc index 01bd38d3647..a2ee87339e2 100644 --- a/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc +++ b/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --function foo --pointer-check ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) > 5: SUCCESS$ diff --git a/regression/cbmc/Global_Initialization1/test.desc b/regression/cbmc/Global_Initialization1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Global_Initialization1/test.desc +++ b/regression/cbmc/Global_Initialization1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Global_Initialization2/test.desc b/regression/cbmc/Global_Initialization2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Global_Initialization2/test.desc +++ b/regression/cbmc/Global_Initialization2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Initialization1/test.desc b/regression/cbmc/Initialization1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Initialization1/test.desc +++ b/regression/cbmc/Initialization1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Initialization2/test.desc b/regression/cbmc/Initialization2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Initialization2/test.desc +++ b/regression/cbmc/Initialization2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Initialization3/test.desc b/regression/cbmc/Initialization3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Initialization3/test.desc +++ b/regression/cbmc/Initialization3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/KnR1/test.desc b/regression/cbmc/KnR1/test.desc index 574296748f3..1f2c73a7350 100644 --- a/regression/cbmc/KnR1/test.desc +++ b/regression/cbmc/KnR1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Linked_List1/test.desc b/regression/cbmc/Linked_List1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Linked_List1/test.desc +++ b/regression/cbmc/Linked_List1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Linking1/test.desc b/regression/cbmc/Linking1/test.desc index af20f90c655..645f563290d 100644 --- a/regression/cbmc/Linking1/test.desc +++ b/regression/cbmc/Linking1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c module.c ^EXIT=0$ diff --git a/regression/cbmc/Linking2/test.desc b/regression/cbmc/Linking2/test.desc index af20f90c655..645f563290d 100644 --- a/regression/cbmc/Linking2/test.desc +++ b/regression/cbmc/Linking2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c module.c ^EXIT=0$ diff --git a/regression/cbmc/Linking3/test.desc b/regression/cbmc/Linking3/test.desc index bb271770fef..ca176b4ad69 100644 --- a/regression/cbmc/Linking3/test.desc +++ b/regression/cbmc/Linking3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main1.c main2.c ^EXIT=0$ diff --git a/regression/cbmc/Linking4/test.desc b/regression/cbmc/Linking4/test.desc index d88e6744dbd..eeb440dc546 100644 --- a/regression/cbmc/Linking4/test.desc +++ b/regression/cbmc/Linking4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend link1.c link2.c ^EXIT=0$ diff --git a/regression/cbmc/Linking5/test.desc b/regression/cbmc/Linking5/test.desc index d88e6744dbd..eeb440dc546 100644 --- a/regression/cbmc/Linking5/test.desc +++ b/regression/cbmc/Linking5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend link1.c link2.c ^EXIT=0$ diff --git a/regression/cbmc/Linking6/test.desc b/regression/cbmc/Linking6/test.desc index 67f1dd7303f..a5e0ad27fd7 100644 --- a/regression/cbmc/Linking6/test.desc +++ b/regression/cbmc/Linking6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c module.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Linking7/return_type.desc b/regression/cbmc/Linking7/return_type.desc index e51bc4611dd..09e102a87c1 100644 --- a/regression/cbmc/Linking7/return_type.desc +++ b/regression/cbmc/Linking7/return_type.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend return_type1.c return_type2.c ^EXIT=0$ diff --git a/regression/cbmc/Linking8/test.desc b/regression/cbmc/Linking8/test.desc index ebb8d9d1d71..d2e73a08fe0 100644 --- a/regression/cbmc/Linking8/test.desc +++ b/regression/cbmc/Linking8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend b.c a.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Local_out_of_scope1/test.desc b/regression/cbmc/Local_out_of_scope1/test.desc index 950f6791fef..25c4b7ecab8 100644 --- a/regression/cbmc/Local_out_of_scope1/test.desc +++ b/regression/cbmc/Local_out_of_scope1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/Local_out_of_scope2/test.desc b/regression/cbmc/Local_out_of_scope2/test.desc index 6de79559914..b59d561e220 100644 --- a/regression/cbmc/Local_out_of_scope2/test.desc +++ b/regression/cbmc/Local_out_of_scope2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Local_out_of_scope3/test.desc b/regression/cbmc/Local_out_of_scope3/test.desc index 6de79559914..b59d561e220 100644 --- a/regression/cbmc/Local_out_of_scope3/test.desc +++ b/regression/cbmc/Local_out_of_scope3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Local_out_of_scope4/test.desc b/regression/cbmc/Local_out_of_scope4/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Local_out_of_scope4/test.desc +++ b/regression/cbmc/Local_out_of_scope4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Malloc1/test.desc b/regression/cbmc/Malloc1/test.desc index 7561cd38b9b..f2d081192ad 100644 --- a/regression/cbmc/Malloc1/test.desc +++ b/regression/cbmc/Malloc1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Malloc11/slice-formula.desc b/regression/cbmc/Malloc11/slice-formula.desc index e95d6008560..fc9450935d6 100644 --- a/regression/cbmc/Malloc11/slice-formula.desc +++ b/regression/cbmc/Malloc11/slice-formula.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE broken-smt-backend new-smt-backend main.c --pointer-check --slice-formula ^EXIT=0$ diff --git a/regression/cbmc/Malloc11/test.desc b/regression/cbmc/Malloc11/test.desc index 5e4496882a0..0f3c3b19726 100644 --- a/regression/cbmc/Malloc11/test.desc +++ b/regression/cbmc/Malloc11/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE broken-smt-backend new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Malloc14/test.desc b/regression/cbmc/Malloc14/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/Malloc14/test.desc +++ b/regression/cbmc/Malloc14/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Malloc15/test.desc b/regression/cbmc/Malloc15/test.desc index a1b2c8b18ec..7a519ed648a 100644 --- a/regression/cbmc/Malloc15/test.desc +++ b/regression/cbmc/Malloc15/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.i --32 ^EXIT=0$ diff --git a/regression/cbmc/Malloc16/test.desc b/regression/cbmc/Malloc16/test.desc index a1b2c8b18ec..7a519ed648a 100644 --- a/regression/cbmc/Malloc16/test.desc +++ b/regression/cbmc/Malloc16/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.i --32 ^EXIT=0$ diff --git a/regression/cbmc/Malloc17/test.desc b/regression/cbmc/Malloc17/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/Malloc17/test.desc +++ b/regression/cbmc/Malloc17/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Malloc18/test.desc b/regression/cbmc/Malloc18/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/Malloc18/test.desc +++ b/regression/cbmc/Malloc18/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Malloc2/test.desc b/regression/cbmc/Malloc2/test.desc index 7561cd38b9b..f2d081192ad 100644 --- a/regression/cbmc/Malloc2/test.desc +++ b/regression/cbmc/Malloc2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Malloc21/test.desc b/regression/cbmc/Malloc21/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/Malloc21/test.desc +++ b/regression/cbmc/Malloc21/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Malloc22/test.desc b/regression/cbmc/Malloc22/test.desc index 11c11d90c5c..42f6c48b22e 100644 --- a/regression/cbmc/Malloc22/test.desc +++ b/regression/cbmc/Malloc22/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 2 --smt2 --outfile main.smt2 ^EXIT=0$ diff --git a/regression/cbmc/Malloc24/test.desc b/regression/cbmc/Malloc24/test.desc index cf64d363c65..b5dc4690136 100644 --- a/regression/cbmc/Malloc24/test.desc +++ b/regression/cbmc/Malloc24/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 4 --pointer-check --unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc/Malloc25/test.desc b/regression/cbmc/Malloc25/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Malloc25/test.desc +++ b/regression/cbmc/Malloc25/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Malloc3/test.desc b/regression/cbmc/Malloc3/test.desc index 950f6791fef..25c4b7ecab8 100644 --- a/regression/cbmc/Malloc3/test.desc +++ b/regression/cbmc/Malloc3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/Malloc4/test.desc b/regression/cbmc/Malloc4/test.desc index ac6b317a781..6c032458ae9 100644 --- a/regression/cbmc/Malloc4/test.desc +++ b/regression/cbmc/Malloc4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --bounds-check ^SIGNAL=0$ diff --git a/regression/cbmc/Malloc5/test.desc b/regression/cbmc/Malloc5/test.desc index 72b27267062..2a968fbee97 100644 --- a/regression/cbmc/Malloc5/test.desc +++ b/regression/cbmc/Malloc5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --bounds-check ^SIGNAL=0$ diff --git a/regression/cbmc/Malloc6/test.desc b/regression/cbmc/Malloc6/test.desc index 7561cd38b9b..f2d081192ad 100644 --- a/regression/cbmc/Malloc6/test.desc +++ b/regression/cbmc/Malloc6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Malloc7/test.desc b/regression/cbmc/Malloc7/test.desc index 7561cd38b9b..f2d081192ad 100644 --- a/regression/cbmc/Malloc7/test.desc +++ b/regression/cbmc/Malloc7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Malloc9/test.desc b/regression/cbmc/Malloc9/test.desc index 7561cd38b9b..f2d081192ad 100644 --- a/regression/cbmc/Malloc9/test.desc +++ b/regression/cbmc/Malloc9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Memory_leak_abort/test.desc b/regression/cbmc/Memory_leak_abort/test.desc index 7c77b3769c1..4e2fcc003e6 100644 --- a/regression/cbmc/Memory_leak_abort/test.desc +++ b/regression/cbmc/Memory_leak_abort/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --memory-leak-check --memory-cleanup-check --no-assertions ^EXIT=10$ diff --git a/regression/cbmc/Multi_Dimensional_Array1/test.desc b/regression/cbmc/Multi_Dimensional_Array1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Multi_Dimensional_Array1/test.desc +++ b/regression/cbmc/Multi_Dimensional_Array1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Multi_Dimensional_Array2/test.desc b/regression/cbmc/Multi_Dimensional_Array2/test.desc index 39d9265e8a7..87ef4101772 100644 --- a/regression/cbmc/Multi_Dimensional_Array2/test.desc +++ b/regression/cbmc/Multi_Dimensional_Array2/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE broken-smt-backend new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Multi_Dimensional_Array3/test.desc b/regression/cbmc/Multi_Dimensional_Array3/test.desc index ba46c0308cf..05eee6f8c79 100644 --- a/regression/cbmc/Multi_Dimensional_Array3/test.desc +++ b/regression/cbmc/Multi_Dimensional_Array3/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE broken-smt-backend new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Multi_Dimensional_Array4/test.desc b/regression/cbmc/Multi_Dimensional_Array4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Multi_Dimensional_Array4/test.desc +++ b/regression/cbmc/Multi_Dimensional_Array4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Multi_Dimensional_Array5/test.desc b/regression/cbmc/Multi_Dimensional_Array5/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Multi_Dimensional_Array5/test.desc +++ b/regression/cbmc/Multi_Dimensional_Array5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Multi_Dimensional_Array6/test.desc b/regression/cbmc/Multi_Dimensional_Array6/test.desc index 6694cf6e8b7..56a47365d13 100644 --- a/regression/cbmc/Multi_Dimensional_Array6/test.desc +++ b/regression/cbmc/Multi_Dimensional_Array6/test.desc @@ -1,4 +1,4 @@ -CORE thorough-paths +CORE thorough-paths new-smt-backend main.c --unwind 3 --no-unwinding-assertions ^EXIT=10$ diff --git a/regression/cbmc/Multiple_Properties1/test.desc b/regression/cbmc/Multiple_Properties1/test.desc index beb36b219c7..77fadc44fd7 100644 --- a/regression/cbmc/Multiple_Properties1/test.desc +++ b/regression/cbmc/Multiple_Properties1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --property main.assertion.1 --property main.assertion.3 activate-multi-line-match diff --git a/regression/cbmc/Pointer20/test.desc b/regression/cbmc/Pointer20/test.desc index a0af87d2c09..49c3899266f 100644 --- a/regression/cbmc/Pointer20/test.desc +++ b/regression/cbmc/Pointer20/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^SIGNAL=0$ diff --git a/regression/cbmc/Pointer21/test.desc b/regression/cbmc/Pointer21/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer21/test.desc +++ b/regression/cbmc/Pointer21/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer23/test.desc b/regression/cbmc/Pointer23/test.desc index a0af87d2c09..49c3899266f 100644 --- a/regression/cbmc/Pointer23/test.desc +++ b/regression/cbmc/Pointer23/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^SIGNAL=0$ diff --git a/regression/cbmc/Pointer3/test.desc b/regression/cbmc/Pointer3/test.desc index a0af87d2c09..49c3899266f 100644 --- a/regression/cbmc/Pointer3/test.desc +++ b/regression/cbmc/Pointer3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^SIGNAL=0$ diff --git a/regression/cbmc/Pointer31/test.desc b/regression/cbmc/Pointer31/test.desc index a0af87d2c09..49c3899266f 100644 --- a/regression/cbmc/Pointer31/test.desc +++ b/regression/cbmc/Pointer31/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^SIGNAL=0$ diff --git a/regression/cbmc/Pointer4/test.desc b/regression/cbmc/Pointer4/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer4/test.desc +++ b/regression/cbmc/Pointer4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic1/test.desc b/regression/cbmc/Pointer_Arithmetic1/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Pointer_Arithmetic1/test.desc +++ b/regression/cbmc/Pointer_Arithmetic1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic11/test.desc b/regression/cbmc/Pointer_Arithmetic11/test.desc index f5e039ba3ed..89e898790d4 100644 --- a/regression/cbmc/Pointer_Arithmetic11/test.desc +++ b/regression/cbmc/Pointer_Arithmetic11/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --little-endian ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic16/test.desc b/regression/cbmc/Pointer_Arithmetic16/test.desc index 34e9937c5ed..2377020c65b 100644 --- a/regression/cbmc/Pointer_Arithmetic16/test.desc +++ b/regression/cbmc/Pointer_Arithmetic16/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Pointer_Arithmetic8/test.desc b/regression/cbmc/Pointer_Arithmetic8/test.desc index 4b9176a942e..12fbfc53750 100644 --- a/regression/cbmc/Pointer_Arithmetic8/test.desc +++ b/regression/cbmc/Pointer_Arithmetic8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --bounds-check ^EXIT=10$ diff --git a/regression/cbmc/Pointer_Object_Type1/test.desc b/regression/cbmc/Pointer_Object_Type1/test.desc index d3aaf765740..5bc937da3ce 100644 --- a/regression/cbmc/Pointer_Object_Type1/test.desc +++ b/regression/cbmc/Pointer_Object_Type1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --bounds-check ^SIGNAL=0$ diff --git a/regression/cbmc/Pointer_array1/test.desc b/regression/cbmc/Pointer_array1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Pointer_array1/test.desc +++ b/regression/cbmc/Pointer_array1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer_array2/test.desc b/regression/cbmc/Pointer_array2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Pointer_array2/test.desc +++ b/regression/cbmc/Pointer_array2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer_array3/test.desc b/regression/cbmc/Pointer_array3/test.desc index 33c89987cc7..a7e9cb00446 100644 --- a/regression/cbmc/Pointer_array3/test.desc +++ b/regression/cbmc/Pointer_array3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --no-assertions ^EXIT=10$ diff --git a/regression/cbmc/Pointer_array4/test.desc b/regression/cbmc/Pointer_array4/test.desc index 35cc9d3cd74..0c98ed635a3 100644 --- a/regression/cbmc/Pointer_array4/test.desc +++ b/regression/cbmc/Pointer_array4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.i --32 ^EXIT=0$ diff --git a/regression/cbmc/Pointer_array6/test.desc b/regression/cbmc/Pointer_array6/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Pointer_array6/test.desc +++ b/regression/cbmc/Pointer_array6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer_array7/big-endian.desc b/regression/cbmc/Pointer_array7/big-endian.desc index 9e87bda510b..50ffd251416 100644 --- a/regression/cbmc/Pointer_array7/big-endian.desc +++ b/regression/cbmc/Pointer_array7/big-endian.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --big-endian -D__BIG_ENDIAN__ ^EXIT=0$ diff --git a/regression/cbmc/Pointer_array7/test.desc b/regression/cbmc/Pointer_array7/test.desc index 5cbdd55bc98..5ae0160a0ef 100644 --- a/regression/cbmc/Pointer_array7/test.desc +++ b/regression/cbmc/Pointer_array7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian -D__LITTLE_ENDIAN__ ^EXIT=0$ diff --git a/regression/cbmc/Pointer_byte_extract2/test.desc b/regression/cbmc/Pointer_byte_extract2/test.desc index eb98d4f78ba..af0f6ea4b3f 100644 --- a/regression/cbmc/Pointer_byte_extract2/test.desc +++ b/regression/cbmc/Pointer_byte_extract2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian ^EXIT=10$ diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc index 474026934fa..4a6b49453e9 100644 --- a/regression/cbmc/Pointer_byte_extract5/test.desc +++ b/regression/cbmc/Pointer_byte_extract5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.i --bounds-check --32 ^EXIT=10$ diff --git a/regression/cbmc/Pointer_byte_extract7/test.desc b/regression/cbmc/Pointer_byte_extract7/test.desc index 81ceb4c6dc0..9457c6a3fd8 100644 --- a/regression/cbmc/Pointer_byte_extract7/test.desc +++ b/regression/cbmc/Pointer_byte_extract7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --big-endian ^EXIT=0$ diff --git a/regression/cbmc/Pointer_byte_extract8/test.desc b/regression/cbmc/Pointer_byte_extract8/test.desc index adcea6ed3e2..7f9ece3466d 100644 --- a/regression/cbmc/Pointer_byte_extract8/test.desc +++ b/regression/cbmc/Pointer_byte_extract8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --64 --unwind 4 --unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc/Pointer_comparison2/test.desc b/regression/cbmc/Pointer_comparison2/test.desc index 278f468e130..22961959ca9 100644 --- a/regression/cbmc/Pointer_comparison2/test.desc +++ b/regression/cbmc/Pointer_comparison2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer_difference1/no-simplify.desc b/regression/cbmc/Pointer_difference1/no-simplify.desc index 2d4a398e23a..ae0b2a16edd 100644 --- a/regression/cbmc/Pointer_difference1/no-simplify.desc +++ b/regression/cbmc/Pointer_difference1/no-simplify.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --no-simplify VERIFICATION SUCCESSFUL diff --git a/regression/cbmc/Pointer_difference1/test.desc b/regression/cbmc/Pointer_difference1/test.desc index 466da18b2b5..00550a6e62f 100644 --- a/regression/cbmc/Pointer_difference1/test.desc +++ b/regression/cbmc/Pointer_difference1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Promotion1/test.desc b/regression/cbmc/Promotion1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Promotion1/test.desc +++ b/regression/cbmc/Promotion1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Promotion2/test.desc b/regression/cbmc/Promotion2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Promotion2/test.desc +++ b/regression/cbmc/Promotion2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Promotion3/test.desc b/regression/cbmc/Promotion3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Promotion3/test.desc +++ b/regression/cbmc/Promotion3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Promotion4/test.desc b/regression/cbmc/Promotion4/test.desc index 63da0758056..42e327ad1bc 100644 --- a/regression/cbmc/Promotion4/test.desc +++ b/regression/cbmc/Promotion4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.i --16 ^EXIT=0$ diff --git a/regression/cbmc/Quantifiers-simplify/rewrite_exists.desc b/regression/cbmc/Quantifiers-simplify/rewrite_exists.desc index 9b8e205c08c..aea9d163276 100644 --- a/regression/cbmc/Quantifiers-simplify/rewrite_exists.desc +++ b/regression/cbmc/Quantifiers-simplify/rewrite_exists.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend rewrite_exists.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Quantifiers-simplify/rewrite_forall.desc b/regression/cbmc/Quantifiers-simplify/rewrite_forall.desc index 516527d0ce1..c4f4fadafa4 100644 --- a/regression/cbmc/Quantifiers-simplify/rewrite_forall.desc +++ b/regression/cbmc/Quantifiers-simplify/rewrite_forall.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend rewrite_forall.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Quantifiers-simplify/simplify_not_forall.desc b/regression/cbmc/Quantifiers-simplify/simplify_not_forall.desc index 7e9a2db9699..452c5041604 100644 --- a/regression/cbmc/Quantifiers-simplify/simplify_not_forall.desc +++ b/regression/cbmc/Quantifiers-simplify/simplify_not_forall.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --program-only ASSERT\(exists \{ signed int i!0#0; !\(i!0#0 >= 0\) \}\)$ diff --git a/regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc b/regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc index 04d89eeef82..4c495b50792 100644 --- a/regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc +++ b/regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend quantifier-with-side-effect.c ^EXIT=6$ diff --git a/regression/cbmc/Quantifiers1/test.desc b/regression/cbmc/Quantifiers1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Quantifiers1/test.desc +++ b/regression/cbmc/Quantifiers1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Recursion1/test.desc b/regression/cbmc/Recursion1/test.desc index 4a9104162ed..4529b27fc92 100644 --- a/regression/cbmc/Recursion1/test.desc +++ b/regression/cbmc/Recursion1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 11 ^EXIT=0$ diff --git a/regression/cbmc/Recursion2/test.desc b/regression/cbmc/Recursion2/test.desc index 4a9104162ed..4529b27fc92 100644 --- a/regression/cbmc/Recursion2/test.desc +++ b/regression/cbmc/Recursion2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 11 ^EXIT=0$ diff --git a/regression/cbmc/Recursion3/test.desc b/regression/cbmc/Recursion3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Recursion3/test.desc +++ b/regression/cbmc/Recursion3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Recursion4/test.desc b/regression/cbmc/Recursion4/test.desc index 6cb8c550fa3..bf382a33f0f 100644 --- a/regression/cbmc/Recursion4/test.desc +++ b/regression/cbmc/Recursion4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --no-propagation --unwind 2 ^EXIT=0$ diff --git a/regression/cbmc/Recursion5/test.desc b/regression/cbmc/Recursion5/test.desc index bb6455323ca..4863f2764bc 100644 --- a/regression/cbmc/Recursion5/test.desc +++ b/regression/cbmc/Recursion5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 2 --no-unwinding-assertions ^EXIT=10$ diff --git a/regression/cbmc/Recursion6/test.desc b/regression/cbmc/Recursion6/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Recursion6/test.desc +++ b/regression/cbmc/Recursion6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Same_Basename1/test.desc b/regression/cbmc/Same_Basename1/test.desc index b7af5f0e4e4..3f3fd1dd763 100644 --- a/regression/cbmc/Same_Basename1/test.desc +++ b/regression/cbmc/Same_Basename1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend bar.c foo/bar.c ^EXIT=0$ diff --git a/regression/cbmc/Sideeffects1/test.desc b/regression/cbmc/Sideeffects1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Sideeffects1/test.desc +++ b/regression/cbmc/Sideeffects1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Sideeffects2/test.desc b/regression/cbmc/Sideeffects2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Sideeffects2/test.desc +++ b/regression/cbmc/Sideeffects2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Sideeffects3/test.desc b/regression/cbmc/Sideeffects3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Sideeffects3/test.desc +++ b/regression/cbmc/Sideeffects3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Sideeffects4/test.desc b/regression/cbmc/Sideeffects4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Sideeffects4/test.desc +++ b/regression/cbmc/Sideeffects4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Sideeffects5/test.desc b/regression/cbmc/Sideeffects5/test.desc index e69488b2e66..e4902fb709a 100644 --- a/regression/cbmc/Sideeffects5/test.desc +++ b/regression/cbmc/Sideeffects5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --div-by-zero-check ^EXIT=10$ diff --git a/regression/cbmc/Sideeffects6/test.desc b/regression/cbmc/Sideeffects6/test.desc index e69488b2e66..e4902fb709a 100644 --- a/regression/cbmc/Sideeffects6/test.desc +++ b/regression/cbmc/Sideeffects6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --div-by-zero-check ^EXIT=10$ diff --git a/regression/cbmc/Sideeffects8/test.desc b/regression/cbmc/Sideeffects8/test.desc index 565f30cc839..ca8c3172e2b 100644 --- a/regression/cbmc/Sideeffects8/test.desc +++ b/regression/cbmc/Sideeffects8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Sizeof1/test.desc b/regression/cbmc/Sizeof1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Sizeof1/test.desc +++ b/regression/cbmc/Sizeof1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Static2/test.desc b/regression/cbmc/Static2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Static2/test.desc +++ b/regression/cbmc/Static2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Static4/test.desc b/regression/cbmc/Static4/test.desc index 1d4a527e6f2..a25ad4cbd93 100644 --- a/regression/cbmc/Static4/test.desc +++ b/regression/cbmc/Static4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table ^EXIT=0$ diff --git a/regression/cbmc/Static_Functions1/test.desc b/regression/cbmc/Static_Functions1/test.desc index 8a09111c3b1..6a8056da7e4 100644 --- a/regression/cbmc/Static_Functions1/test.desc +++ b/regression/cbmc/Static_Functions1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend file1.c file2.c ^EXIT=0$ diff --git a/regression/cbmc/String1/test.desc b/regression/cbmc/String1/test.desc index 96c9b4bcd7b..5821c3e2820 100644 --- a/regression/cbmc/String1/test.desc +++ b/regression/cbmc/String1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/String4/test.desc b/regression/cbmc/String4/test.desc index 96c9b4bcd7b..5821c3e2820 100644 --- a/regression/cbmc/String4/test.desc +++ b/regression/cbmc/String4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/String5/test.desc b/regression/cbmc/String5/test.desc index 96c9b4bcd7b..5821c3e2820 100644 --- a/regression/cbmc/String5/test.desc +++ b/regression/cbmc/String5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/String7/test.desc b/regression/cbmc/String7/test.desc index 96c9b4bcd7b..5821c3e2820 100644 --- a/regression/cbmc/String7/test.desc +++ b/regression/cbmc/String7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction1/test.desc b/regression/cbmc/String_Abstraction1/test.desc index e6fb3bba609..1eb3c23641f 100644 --- a/regression/cbmc/String_Abstraction1/test.desc +++ b/regression/cbmc/String_Abstraction1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --string-abstraction --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction11/test.desc b/regression/cbmc/String_Abstraction11/test.desc index e21815b93e7..e2565276645 100644 --- a/regression/cbmc/String_Abstraction11/test.desc +++ b/regression/cbmc/String_Abstraction11/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend anon-retval.c --string-abstraction ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction12/test.desc b/regression/cbmc/String_Abstraction12/test.desc index f1bfc215f0e..13a54271fca 100644 --- a/regression/cbmc/String_Abstraction12/test.desc +++ b/regression/cbmc/String_Abstraction12/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend char-array.c --string-abstraction ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction14/test.desc b/regression/cbmc/String_Abstraction14/test.desc index 18451e6bc84..363bf3474e5 100644 --- a/regression/cbmc/String_Abstraction14/test.desc +++ b/regression/cbmc/String_Abstraction14/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend pass-in-implicit.c --string-abstraction ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction15/test.desc b/regression/cbmc/String_Abstraction15/test.desc index d7fa5b8d070..05d3fbd6365 100644 --- a/regression/cbmc/String_Abstraction15/test.desc +++ b/regression/cbmc/String_Abstraction15/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend pass-in.c --string-abstraction ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction19/test.desc b/regression/cbmc/String_Abstraction19/test.desc index 456949ab85b..f573198d9a1 100644 --- a/regression/cbmc/String_Abstraction19/test.desc +++ b/regression/cbmc/String_Abstraction19/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend structs.c --string-abstraction ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction2/test.desc b/regression/cbmc/String_Abstraction2/test.desc index e6fb3bba609..1eb3c23641f 100644 --- a/regression/cbmc/String_Abstraction2/test.desc +++ b/regression/cbmc/String_Abstraction2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --string-abstraction --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction20/test.desc b/regression/cbmc/String_Abstraction20/test.desc index 4d938229673..a847537f994 100644 --- a/regression/cbmc/String_Abstraction20/test.desc +++ b/regression/cbmc/String_Abstraction20/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend structs2.c --string-abstraction ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction22/test.desc b/regression/cbmc/String_Abstraction22/test.desc index f3145b289ad..ccde4872657 100644 --- a/regression/cbmc/String_Abstraction22/test.desc +++ b/regression/cbmc/String_Abstraction22/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --string-abstraction ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction23/test.desc b/regression/cbmc/String_Abstraction23/test.desc index e6fb3bba609..1eb3c23641f 100644 --- a/regression/cbmc/String_Abstraction23/test.desc +++ b/regression/cbmc/String_Abstraction23/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --string-abstraction --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction3/test.desc b/regression/cbmc/String_Abstraction3/test.desc index e6fb3bba609..1eb3c23641f 100644 --- a/regression/cbmc/String_Abstraction3/test.desc +++ b/regression/cbmc/String_Abstraction3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --string-abstraction --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction8/test.desc b/regression/cbmc/String_Abstraction8/test.desc index c9b7d9f6ff4..2e71211cd8a 100644 --- a/regression/cbmc/String_Abstraction8/test.desc +++ b/regression/cbmc/String_Abstraction8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --string-abstraction --unwind 5 --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/String_Abstraction9/test.desc b/regression/cbmc/String_Abstraction9/test.desc index e6fb3bba609..1eb3c23641f 100644 --- a/regression/cbmc/String_Abstraction9/test.desc +++ b/regression/cbmc/String_Abstraction9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --string-abstraction --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/Type_Error1/test.desc b/regression/cbmc/Type_Error1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Type_Error1/test.desc +++ b/regression/cbmc/Type_Error1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Typecast1/test.desc b/regression/cbmc/Typecast1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Typecast1/test.desc +++ b/regression/cbmc/Typecast1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Typecast2/test.desc b/regression/cbmc/Typecast2/test.desc index cdbe617e1f6..e75e707a552 100644 --- a/regression/cbmc/Typecast2/test.desc +++ b/regression/cbmc/Typecast2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.i --no-propagation --64 ^EXIT=0$ diff --git a/regression/cbmc/Typecast3/test.desc b/regression/cbmc/Typecast3/test.desc index fb0ba091c5b..c6e349c161c 100644 --- a/regression/cbmc/Typecast3/test.desc +++ b/regression/cbmc/Typecast3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Unbounded_Array1/test.desc b/regression/cbmc/Unbounded_Array1/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/Unbounded_Array1/test.desc +++ b/regression/cbmc/Unbounded_Array1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Unbounded_Array2/test.desc b/regression/cbmc/Unbounded_Array2/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/Unbounded_Array2/test.desc +++ b/regression/cbmc/Unbounded_Array2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Unbounded_Array3/test.desc b/regression/cbmc/Unbounded_Array3/test.desc index 33900ad2b78..82568cfc082 100644 --- a/regression/cbmc/Unbounded_Array3/test.desc +++ b/regression/cbmc/Unbounded_Array3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Unbounded_Array4/test.desc b/regression/cbmc/Unbounded_Array4/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/Unbounded_Array4/test.desc +++ b/regression/cbmc/Unbounded_Array4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Unbounded_Array5/test.desc b/regression/cbmc/Unbounded_Array5/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/Unbounded_Array5/test.desc +++ b/regression/cbmc/Unbounded_Array5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Undefined_Function1/test.desc b/regression/cbmc/Undefined_Function1/test.desc index 431b8dc42b1..035e5aec631 100644 --- a/regression/cbmc/Undefined_Function1/test.desc +++ b/regression/cbmc/Undefined_Function1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Undefined_Function2/test.desc b/regression/cbmc/Undefined_Function2/test.desc index bf3843459f5..31ef9c4330d 100644 --- a/regression/cbmc/Undefined_Function2/test.desc +++ b/regression/cbmc/Undefined_Function2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Undefined_Shift1/test.desc b/regression/cbmc/Undefined_Shift1/test.desc index 06417908cee..2100ae1bf2f 100644 --- a/regression/cbmc/Undefined_Shift1/test.desc +++ b/regression/cbmc/Undefined_Shift1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --undefined-shift-check ^EXIT=10$ diff --git a/regression/cbmc/Unwinding_Locality1/test.desc b/regression/cbmc/Unwinding_Locality1/test.desc index 33900ad2b78..82568cfc082 100644 --- a/regression/cbmc/Unwinding_Locality1/test.desc +++ b/regression/cbmc/Unwinding_Locality1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/Variadic1/test.desc b/regression/cbmc/Variadic1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Variadic1/test.desc +++ b/regression/cbmc/Variadic1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Visual_Studio_Types1/test.desc b/regression/cbmc/Visual_Studio_Types1/test.desc index 982c46d6c98..8a0bf496c8f 100644 --- a/regression/cbmc/Visual_Studio_Types1/test.desc +++ b/regression/cbmc/Visual_Studio_Types1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.i --i386-win32 ^EXIT=0$ diff --git a/regression/cbmc/Visual_Studio_Types2/test.desc b/regression/cbmc/Visual_Studio_Types2/test.desc index 254b9942989..1fa3a10bf4c 100644 --- a/regression/cbmc/Visual_Studio_Types2/test.desc +++ b/regression/cbmc/Visual_Studio_Types2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.i --winx64 ^EXIT=0$ diff --git a/regression/cbmc/Zero_Initialization1/test.desc b/regression/cbmc/Zero_Initialization1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Zero_Initialization1/test.desc +++ b/regression/cbmc/Zero_Initialization1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/__func__1/test.desc b/regression/cbmc/__func__1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/__func__1/test.desc +++ b/regression/cbmc/__func__1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/always_inline2/test.desc b/regression/cbmc/always_inline2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/always_inline2/test.desc +++ b/regression/cbmc/always_inline2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/always_inline3/test.desc b/regression/cbmc/always_inline3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/always_inline3/test.desc +++ b/regression/cbmc/always_inline3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/apply_condition1/test.desc b/regression/cbmc/apply_condition1/test.desc index c0dd22e954d..1af4a06c3bd 100644 --- a/regression/cbmc/apply_condition1/test.desc +++ b/regression/cbmc/apply_condition1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^VERIFICATION FAILED$ diff --git a/regression/cbmc/argc-and-argv/argc1.desc b/regression/cbmc/argc-and-argv/argc1.desc index 5f6348ffbe0..75a33f47f83 100644 --- a/regression/cbmc/argc-and-argv/argc1.desc +++ b/regression/cbmc/argc-and-argv/argc1.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend argc1.c --bounds-check --pointer-check --unwind 0 ^EXIT=10$ diff --git a/regression/cbmc/argc-and-argv/argv1.desc b/regression/cbmc/argc-and-argv/argv1.desc index 1f379687b2b..978f764059d 100644 --- a/regression/cbmc/argc-and-argv/argv1.desc +++ b/regression/cbmc/argc-and-argv/argv1.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend argv1.c --bounds-check --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/argv2/test.desc b/regression/cbmc/argv2/test.desc index e41bbe1df7a..672e7d28024 100644 --- a/regression/cbmc/argv2/test.desc +++ b/regression/cbmc/argv2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.i --32 ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/array-cell-sensitivity1/test_execution.desc b/regression/cbmc/array-cell-sensitivity1/test_execution.desc index 9280dcb19be..bae66a2dd4b 100644 --- a/regression/cbmc/array-cell-sensitivity1/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity1/test_execution.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/array-cell-sensitivity11/test.desc b/regression/cbmc/array-cell-sensitivity11/test.desc index 876777e3cf6..39040e6ec57 100644 --- a/regression/cbmc/array-cell-sensitivity11/test.desc +++ b/regression/cbmc/array-cell-sensitivity11/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --show-vcc main::1::array!0@1#2\[\[0\]\]..y = diff --git a/regression/cbmc/array-cell-sensitivity13/test.desc b/regression/cbmc/array-cell-sensitivity13/test.desc index 36d5cc34e1a..f1e573e7548 100644 --- a/regression/cbmc/array-cell-sensitivity13/test.desc +++ b/regression/cbmc/array-cell-sensitivity13/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --show-vcc main::1::node1!0@1#2\.\.data = diff --git a/regression/cbmc/array-cell-sensitivity14/test.desc b/regression/cbmc/array-cell-sensitivity14/test.desc index 3395875c67d..56536513f0d 100644 --- a/regression/cbmc/array-cell-sensitivity14/test.desc +++ b/regression/cbmc/array-cell-sensitivity14/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --show-vcc main::1::node1!0@1#2\.\.data = diff --git a/regression/cbmc/array-cell-sensitivity15/test.desc b/regression/cbmc/array-cell-sensitivity15/test.desc index 84c4b927b7c..ebcd06ece7b 100644 --- a/regression/cbmc/array-cell-sensitivity15/test.desc +++ b/regression/cbmc/array-cell-sensitivity15/test.desc @@ -1,4 +1,4 @@ -CORE paths-lifo-expected-failure +CORE paths-lifo-expected-failure new-smt-backend access.c --program-only ^EXIT=0$ diff --git a/regression/cbmc/array-cell-sensitivity2/test.desc b/regression/cbmc/array-cell-sensitivity2/test.desc index 65b734796e9..e36c2d65cb0 100644 --- a/regression/cbmc/array-cell-sensitivity2/test.desc +++ b/regression/cbmc/array-cell-sensitivity2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --show-vcc main::1::array!0@1#2 = with\(main::1::array!0@1#1, cast\(main::argc!0@1#1 \+ -1, signedbv\[64\]\), 1\) diff --git a/regression/cbmc/array-cell-sensitivity2/test_execution.desc b/regression/cbmc/array-cell-sensitivity2/test_execution.desc index 9280dcb19be..bae66a2dd4b 100644 --- a/regression/cbmc/array-cell-sensitivity2/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity2/test_execution.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/array-cell-sensitivity3/test_execution.desc b/regression/cbmc/array-cell-sensitivity3/test_execution.desc index 52bf413ffd9..4f8a74b4cea 100644 --- a/regression/cbmc/array-cell-sensitivity3/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity3/test_execution.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^VERIFICATION FAILED$ diff --git a/regression/cbmc/array-cell-sensitivity4/test_execution.desc b/regression/cbmc/array-cell-sensitivity4/test_execution.desc index 9280dcb19be..bae66a2dd4b 100644 --- a/regression/cbmc/array-cell-sensitivity4/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity4/test_execution.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/array-cell-sensitivity5/test_execution.desc b/regression/cbmc/array-cell-sensitivity5/test_execution.desc index 9280dcb19be..bae66a2dd4b 100644 --- a/regression/cbmc/array-cell-sensitivity5/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity5/test_execution.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/array-cell-sensitivity6/test_execution.desc b/regression/cbmc/array-cell-sensitivity6/test_execution.desc index 9280dcb19be..bae66a2dd4b 100644 --- a/regression/cbmc/array-cell-sensitivity6/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity6/test_execution.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/array-constraint/test.desc b/regression/cbmc/array-constraint/test.desc index f450ca322fb..04dcc2aee65 100644 --- a/regression/cbmc/array-constraint/test.desc +++ b/regression/cbmc/array-constraint/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-array-constraints ^EXIT=1$ diff --git a/regression/cbmc/array-constraint/test_xml.desc b/regression/cbmc/array-constraint/test_xml.desc index 8a5e92b42b1..8288e2de3e3 100644 --- a/regression/cbmc/array-constraint/test_xml.desc +++ b/regression/cbmc/array-constraint/test_xml.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-array-constraints --xml-ui ^EXIT=1$ diff --git a/regression/cbmc/array-tests/test.desc b/regression/cbmc/array-tests/test.desc index 3380b5e9b74..2d1516825f8 100644 --- a/regression/cbmc/array-tests/test.desc +++ b/regression/cbmc/array-tests/test.desc @@ -1,4 +1,4 @@ -CORE thorough-paths thorough-smt-backend +CORE thorough-paths thorough-smt-backend new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/array-tests/uf-always.desc b/regression/cbmc/array-tests/uf-always.desc index c51f158c2f5..9cf249b3c8b 100644 --- a/regression/cbmc/array-tests/uf-always.desc +++ b/regression/cbmc/array-tests/uf-always.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend uf-always.c --arrays-uf-always ^EXIT=0$ diff --git a/regression/cbmc/array-tests/zero-sized.desc b/regression/cbmc/array-tests/zero-sized.desc index b6c60848e18..2ffc9eeb700 100644 --- a/regression/cbmc/array-tests/zero-sized.desc +++ b/regression/cbmc/array-tests/zero-sized.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend zero-sized.c ^EXIT=10$ diff --git a/regression/cbmc/assert_rtn_four/test.desc b/regression/cbmc/assert_rtn_four/test.desc index 4e6ca7b2d9e..e60cf9c0eac 100644 --- a/regression/cbmc/assert_rtn_four/test.desc +++ b/regression/cbmc/assert_rtn_four/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c function .* is not declared diff --git a/regression/cbmc/assigning_nullpointers_should_not_crash_symex/test.desc b/regression/cbmc/assigning_nullpointers_should_not_crash_symex/test.desc index 7871b85de89..a0514f57efb 100644 --- a/regression/cbmc/assigning_nullpointers_should_not_crash_symex/test.desc +++ b/regression/cbmc/assigning_nullpointers_should_not_crash_symex/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/atomic_X_fetch-1/pointer.desc b/regression/cbmc/atomic_X_fetch-1/pointer.desc index cf2de2e0ffc..1befe221131 100644 --- a/regression/cbmc/atomic_X_fetch-1/pointer.desc +++ b/regression/cbmc/atomic_X_fetch-1/pointer.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend pointer.c ^EXIT=6$ diff --git a/regression/cbmc/atomic_X_fetch-1/test.desc b/regression/cbmc/atomic_X_fetch-1/test.desc index 27a28993ba5..6032b0b3c6a 100644 --- a/regression/cbmc/atomic_X_fetch-1/test.desc +++ b/regression/cbmc/atomic_X_fetch-1/test.desc @@ -1,4 +1,4 @@ -CORE gcc-only +CORE gcc-only new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/atomic_X_fetch-1/two.desc b/regression/cbmc/atomic_X_fetch-1/two.desc index 2470348ff1b..a3a5eae1881 100644 --- a/regression/cbmc/atomic_X_fetch-1/two.desc +++ b/regression/cbmc/atomic_X_fetch-1/two.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend two.c ^EXIT=6$ diff --git a/regression/cbmc/atomic_fetch_X-1/pointer.desc b/regression/cbmc/atomic_fetch_X-1/pointer.desc index cf2de2e0ffc..1befe221131 100644 --- a/regression/cbmc/atomic_fetch_X-1/pointer.desc +++ b/regression/cbmc/atomic_fetch_X-1/pointer.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend pointer.c ^EXIT=6$ diff --git a/regression/cbmc/atomic_fetch_X-1/two.desc b/regression/cbmc/atomic_fetch_X-1/two.desc index 2470348ff1b..a3a5eae1881 100644 --- a/regression/cbmc/atomic_fetch_X-1/two.desc +++ b/regression/cbmc/atomic_fetch_X-1/two.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend two.c ^EXIT=6$ diff --git a/regression/cbmc/atomic_load_store-1/test.desc b/regression/cbmc/atomic_load_store-1/test.desc index 27a28993ba5..6032b0b3c6a 100644 --- a/regression/cbmc/atomic_load_store-1/test.desc +++ b/regression/cbmc/atomic_load_store-1/test.desc @@ -1,4 +1,4 @@ -CORE gcc-only +CORE gcc-only new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/bad_option/test.desc b/regression/cbmc/bad_option/test.desc index c7f22f5b873..318af32d2c1 100644 --- a/regression/cbmc/bad_option/test.desc +++ b/regression/cbmc/bad_option/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c -foo ^EXIT=(64|1)$ diff --git a/regression/cbmc/bad_option/test_multiple.desc b/regression/cbmc/bad_option/test_multiple.desc index 30697b2267d..284316a7332 100644 --- a/regression/cbmc/bad_option/test_multiple.desc +++ b/regression/cbmc/bad_option/test_multiple.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --trace --foo --refine-strings ^EXIT=(64|1)$ diff --git a/regression/cbmc/big-endian-array1/test.desc b/regression/cbmc/big-endian-array1/test.desc index 81ceb4c6dc0..9457c6a3fd8 100644 --- a/regression/cbmc/big-endian-array1/test.desc +++ b/regression/cbmc/big-endian-array1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --big-endian ^EXIT=0$ diff --git a/regression/cbmc/bounds_check2/test.desc b/regression/cbmc/bounds_check2/test.desc index ca9d85d6fd5..67ec0a948f9 100644 --- a/regression/cbmc/bounds_check2/test.desc +++ b/regression/cbmc/bounds_check2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --bounds-check --retain-trivial-checks ^Generated \d+ VCC\(s\), 0 remaining after simplification$ diff --git a/regression/cbmc/byte-op-metric/test.desc b/regression/cbmc/byte-op-metric/test.desc index 24bbd8fd760..6bc95cb6e1a 100644 --- a/regression/cbmc/byte-op-metric/test.desc +++ b/regression/cbmc/byte-op-metric/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-byte-ops ^EXIT=0$ diff --git a/regression/cbmc/byte-op-metric/test_json.desc b/regression/cbmc/byte-op-metric/test_json.desc index fa0e5ac90d0..e2f47725375 100644 --- a/regression/cbmc/byte-op-metric/test_json.desc +++ b/regression/cbmc/byte-op-metric/test_json.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-byte-ops --json-ui activate-multi-line-match diff --git a/regression/cbmc/byte_update1/test.desc b/regression/cbmc/byte_update1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/byte_update1/test.desc +++ b/regression/cbmc/byte_update1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/byte_update10/test.desc b/regression/cbmc/byte_update10/test.desc index e4acf874325..db605da9634 100644 --- a/regression/cbmc/byte_update10/test.desc +++ b/regression/cbmc/byte_update10/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/byte_update2/test.desc b/regression/cbmc/byte_update2/test.desc index 9845e70d84b..b177f2412ca 100644 --- a/regression/cbmc/byte_update2/test.desc +++ b/regression/cbmc/byte_update2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/byte_update3/test.desc b/regression/cbmc/byte_update3/test.desc index 9845e70d84b..b177f2412ca 100644 --- a/regression/cbmc/byte_update3/test.desc +++ b/regression/cbmc/byte_update3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/byte_update4/test.desc b/regression/cbmc/byte_update4/test.desc index 9845e70d84b..b177f2412ca 100644 --- a/regression/cbmc/byte_update4/test.desc +++ b/regression/cbmc/byte_update4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/byte_update5/full-slice.desc b/regression/cbmc/byte_update5/full-slice.desc index 35702fdf3a2..ba47d78e7e8 100644 --- a/regression/cbmc/byte_update5/full-slice.desc +++ b/regression/cbmc/byte_update5/full-slice.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian --full-slice ^EXIT=0$ diff --git a/regression/cbmc/byte_update5/test.desc b/regression/cbmc/byte_update5/test.desc index 9845e70d84b..b177f2412ca 100644 --- a/regression/cbmc/byte_update5/test.desc +++ b/regression/cbmc/byte_update5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/byte_update6/test.desc b/regression/cbmc/byte_update6/test.desc index 9845e70d84b..b177f2412ca 100644 --- a/regression/cbmc/byte_update6/test.desc +++ b/regression/cbmc/byte_update6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/byte_update7/test.desc b/regression/cbmc/byte_update7/test.desc index 9845e70d84b..b177f2412ca 100644 --- a/regression/cbmc/byte_update7/test.desc +++ b/regression/cbmc/byte_update7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/byte_update8/test.desc b/regression/cbmc/byte_update8/test.desc index 9845e70d84b..b177f2412ca 100644 --- a/regression/cbmc/byte_update8/test.desc +++ b/regression/cbmc/byte_update8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/byte_update9/test.desc b/regression/cbmc/byte_update9/test.desc index 81ceb4c6dc0..9457c6a3fd8 100644 --- a/regression/cbmc/byte_update9/test.desc +++ b/regression/cbmc/byte_update9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --big-endian ^EXIT=0$ diff --git a/regression/cbmc/character_handling1/test.desc b/regression/cbmc/character_handling1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/character_handling1/test.desc +++ b/regression/cbmc/character_handling1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/clang_builtins/bitreverse-typeconflict.desc b/regression/cbmc/clang_builtins/bitreverse-typeconflict.desc index 7cf28b1c1f2..03599581a2e 100644 --- a/regression/cbmc/clang_builtins/bitreverse-typeconflict.desc +++ b/regression/cbmc/clang_builtins/bitreverse-typeconflict.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend bitreverse-typeconflict.c file bitreverse-typeconflict.c line 5 function main: error: __builtin_bitreverse8 expects one operand ^EXIT=6$ diff --git a/regression/cbmc/comma1/test.desc b/regression/cbmc/comma1/test.desc index 12fc8ce06e1..ad10409bb6f 100644 --- a/regression/cbmc/comma1/test.desc +++ b/regression/cbmc/comma1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/compound-assignment/compound_promotion.desc b/regression/cbmc/compound-assignment/compound_promotion.desc index 975a85b1f9d..492043a627a 100644 --- a/regression/cbmc/compound-assignment/compound_promotion.desc +++ b/regression/cbmc/compound-assignment/compound_promotion.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend compound_promotion.c ^EXIT=0$ diff --git a/regression/cbmc/compound_literal1/test.desc b/regression/cbmc/compound_literal1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/compound_literal1/test.desc +++ b/regression/cbmc/compound_literal1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/condition-propagation-1/test.desc b/regression/cbmc/condition-propagation-1/test.desc index cc3baab01eb..ef37fdd4c7f 100644 --- a/regression/cbmc/condition-propagation-1/test.desc +++ b/regression/cbmc/condition-propagation-1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^EXIT=0$ diff --git a/regression/cbmc/condition-propagation-2/test.desc b/regression/cbmc/condition-propagation-2/test.desc index cc3baab01eb..ef37fdd4c7f 100644 --- a/regression/cbmc/condition-propagation-2/test.desc +++ b/regression/cbmc/condition-propagation-2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^EXIT=0$ diff --git a/regression/cbmc/condition-propagation-3/test.desc b/regression/cbmc/condition-propagation-3/test.desc index cc3baab01eb..ef37fdd4c7f 100644 --- a/regression/cbmc/condition-propagation-3/test.desc +++ b/regression/cbmc/condition-propagation-3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^EXIT=0$ diff --git a/regression/cbmc/condition-propagation-4/test.desc b/regression/cbmc/condition-propagation-4/test.desc index cc3baab01eb..ef37fdd4c7f 100644 --- a/regression/cbmc/condition-propagation-4/test.desc +++ b/regression/cbmc/condition-propagation-4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^EXIT=0$ diff --git a/regression/cbmc/const_ptr1/test.desc b/regression/cbmc/const_ptr1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/const_ptr1/test.desc +++ b/regression/cbmc/const_ptr1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/constant_folding1/test.desc b/regression/cbmc/constant_folding1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/constant_folding1/test.desc +++ b/regression/cbmc/constant_folding1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/constant_folding2/test.desc b/regression/cbmc/constant_folding2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/constant_folding2/test.desc +++ b/regression/cbmc/constant_folding2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/constructor1/test.desc b/regression/cbmc/constructor1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/constructor1/test.desc +++ b/regression/cbmc/constructor1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc index 0544dcdb715..9f7882b842f 100644 --- a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc +++ b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc @@ -1,4 +1,4 @@ -CORE paths-lifo-expected-failure +CORE paths-lifo-expected-failure new-smt-backend test.c --cover location --pointer-check --malloc-may-fail --malloc-fail-null \[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED diff --git a/regression/cbmc/cover-failed-assertions/test.desc b/regression/cbmc/cover-failed-assertions/test.desc index 2b07b32fe2d..99d367e7a1c 100644 --- a/regression/cbmc/cover-failed-assertions/test.desc +++ b/regression/cbmc/cover-failed-assertions/test.desc @@ -1,4 +1,4 @@ -CORE paths-lifo-expected-failure +CORE paths-lifo-expected-failure new-smt-backend test.c --cover location --cover-failed-assertions --pointer-check --malloc-may-fail --malloc-fail-null \[main.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED diff --git a/regression/cbmc/coverage_report1/paths.desc b/regression/cbmc/coverage_report1/paths.desc index 6a5b7a085d3..73ae23cf459 100644 --- a/regression/cbmc/coverage_report1/paths.desc +++ b/regression/cbmc/coverage_report1/paths.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --symex-coverage-report - --paths lifo diff --git a/regression/cbmc/coverage_report1/test.desc b/regression/cbmc/coverage_report1/test.desc index 81ec99da0b5..fb67a8b3164 100644 --- a/regression/cbmc/coverage_report1/test.desc +++ b/regression/cbmc/coverage_report1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --symex-coverage-report - diff --git a/regression/cbmc/cprover_bool1/test.desc b/regression/cbmc/cprover_bool1/test.desc index 20a1bea26ec..3771d0ca6f2 100644 --- a/regression/cbmc/cprover_bool1/test.desc +++ b/regression/cbmc/cprover_bool1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --trace ^EXIT=10$ diff --git a/regression/cbmc/cprover_fence_one/test.desc b/regression/cbmc/cprover_fence_one/test.desc index 123db195ec1..9b00e953ecf 100644 --- a/regression/cbmc/cprover_fence_one/test.desc +++ b/regression/cbmc/cprover_fence_one/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=6$ diff --git a/regression/cbmc/cprover_havoc_object_one/test.desc b/regression/cbmc/cprover_havoc_object_one/test.desc index bca33a5dd6d..9f1aa2be3b0 100644 --- a/regression/cbmc/cprover_havoc_object_one/test.desc +++ b/regression/cbmc/cprover_havoc_object_one/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=6$ diff --git a/regression/cbmc/cprover_id1/test.desc b/regression/cbmc/cprover_id1/test.desc index 6d0c9efb95c..2f27ba321a2 100644 --- a/regression/cbmc/cprover_id1/test.desc +++ b/regression/cbmc/cprover_id1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/cprover_postcondition/test.desc b/regression/cbmc/cprover_postcondition/test.desc index 33900ad2b78..82568cfc082 100644 --- a/regression/cbmc/cprover_postcondition/test.desc +++ b/regression/cbmc/cprover_postcondition/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/cprover_precondition/test.desc b/regression/cbmc/cprover_precondition/test.desc index 33900ad2b78..82568cfc082 100644 --- a/regression/cbmc/cprover_precondition/test.desc +++ b/regression/cbmc/cprover_precondition/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/dereference-cache-flag/test-no-cache.desc b/regression/cbmc/dereference-cache-flag/test-no-cache.desc index 23ee595f1e5..233947512d9 100644 --- a/regression/cbmc/dereference-cache-flag/test-no-cache.desc +++ b/regression/cbmc/dereference-cache-flag/test-no-cache.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --show-vcc \(main::1::p!0@1#2 = address_of diff --git a/regression/cbmc/dereference-cache-flag/test-with-cache.desc b/regression/cbmc/dereference-cache-flag/test-with-cache.desc index b4342f18c76..68a04bdfe0c 100644 --- a/regression/cbmc/dereference-cache-flag/test-with-cache.desc +++ b/regression/cbmc/dereference-cache-flag/test-with-cache.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --show-vcc --symex-cache-dereferences symex::dereference_cache!0#1 = 0 diff --git a/regression/cbmc/destructor1/test.desc b/regression/cbmc/destructor1/test.desc index d386a6e31ac..0c9df6413f5 100644 --- a/regression/cbmc/destructor1/test.desc +++ b/regression/cbmc/destructor1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^\[assert_false.assertion.1\] line 10 assertion 0: FAILURE$ diff --git a/regression/cbmc/destructors/compound_literal.desc b/regression/cbmc/destructors/compound_literal.desc index 47c217fed18..0b34672576b 100644 --- a/regression/cbmc/destructors/compound_literal.desc +++ b/regression/cbmc/destructors/compound_literal.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 10 --show-goto-functions activate-multi-line-match diff --git a/regression/cbmc/destructors/enter_lexical_block.desc b/regression/cbmc/destructors/enter_lexical_block.desc index 751e929d85d..b088d95998f 100644 --- a/regression/cbmc/destructors/enter_lexical_block.desc +++ b/regression/cbmc/destructors/enter_lexical_block.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 10 --show-goto-functions activate-multi-line-match diff --git a/regression/cbmc/double_deref/double_deref.desc b/regression/cbmc/double_deref/double_deref.desc index b5daf7673f3..93b5aaf0e7a 100644 --- a/regression/cbmc/double_deref/double_deref.desc +++ b/regression/cbmc/double_deref/double_deref.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend double_deref.c --show-vcc \{1\} \(main::1::pptr!0@1#2 = address_of\(main::1::ptr[12]!0@1\) \? main::argc!0@1#1 = [12] : main::argc!0@1#1 = [12]\) diff --git a/regression/cbmc/double_deref/double_deref_single_alias.desc b/regression/cbmc/double_deref/double_deref_single_alias.desc index c759890f632..992763a2680 100644 --- a/regression/cbmc/double_deref/double_deref_single_alias.desc +++ b/regression/cbmc/double_deref/double_deref_single_alias.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend double_deref_single_alias.c --show-vcc \{1\} main::argc!0@1#1 = 1 diff --git a/regression/cbmc/double_deref/double_deref_with_cast.desc b/regression/cbmc/double_deref/double_deref_with_cast.desc index e5b1f592416..e3e9d6f08a4 100644 --- a/regression/cbmc/double_deref/double_deref_with_cast.desc +++ b/regression/cbmc/double_deref/double_deref_with_cast.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend double_deref_with_cast.c --show-vcc \{1\} \(cast\(main::1::pptr!0@1#2, signedbv\[32\]\*\*\) = address_of\(main::1::ptr2!0@1\) \? main::argc!0@1#1 = 2 \: main::argc!0@1#1 = 1\) diff --git a/regression/cbmc/double_deref/double_deref_with_cast_single_alias.desc b/regression/cbmc/double_deref/double_deref_with_cast_single_alias.desc index 6be9a4d83da..9a7f78cb573 100644 --- a/regression/cbmc/double_deref/double_deref_with_cast_single_alias.desc +++ b/regression/cbmc/double_deref/double_deref_with_cast_single_alias.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend double_deref_with_cast_single_alias.c --show-vcc \{1\} main::argc!0@1#1 = 1 diff --git a/regression/cbmc/double_deref/double_deref_with_member.desc b/regression/cbmc/double_deref/double_deref_with_member.desc index 85156557ba2..c861dbddfb2 100644 --- a/regression/cbmc/double_deref/double_deref_with_member.desc +++ b/regression/cbmc/double_deref/double_deref_with_member.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend double_deref_with_member.c --show-vcc ^\{1\} \(main::1::cptr!0@1#2 = address_of\(main::1::container2!0@1\) \? main::argc!0@1#1 = 2 : main::argc!0@1#1 = 1\) diff --git a/regression/cbmc/double_deref/double_deref_with_member_single_alias.desc b/regression/cbmc/double_deref/double_deref_with_member_single_alias.desc index 0e4313b1877..dfd2f251fec 100644 --- a/regression/cbmc/double_deref/double_deref_with_member_single_alias.desc +++ b/regression/cbmc/double_deref/double_deref_with_member_single_alias.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend double_deref_with_member_single_alias.c --show-vcc \{1\} main::argc!0@1#1 = 1 diff --git a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc index 146ed420549..a0033264617 100644 --- a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc +++ b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend double_deref_with_pointer_arithmetic.c --show-vcc ^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object#3\[\[0\]\], symex_dynamic::dynamic_object#3\[\[1\]\] \}\[cast\(mod\(main::argc!0@1#1, 2\), signedbv\[64\]\)\] diff --git a/regression/cbmc/dynamic_size1/test.desc b/regression/cbmc/dynamic_size1/test.desc index d110065a9cf..c7bf1bb822d 100644 --- a/regression/cbmc/dynamic_size1/test.desc +++ b/regression/cbmc/dynamic_size1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/dynamic_sizeof1/test.desc b/regression/cbmc/dynamic_sizeof1/test.desc index 832578a5964..23a6930cf4e 100644 --- a/regression/cbmc/dynamic_sizeof1/test.desc +++ b/regression/cbmc/dynamic_sizeof1/test.desc @@ -1,4 +1,4 @@ -CORE broken-z3-smt-backend +CORE broken-z3-smt-backend new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/enum1/test.desc b/regression/cbmc/enum1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/enum1/test.desc +++ b/regression/cbmc/enum1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/enum2/test.desc b/regression/cbmc/enum2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/enum2/test.desc +++ b/regression/cbmc/enum2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/enum4/test.desc b/regression/cbmc/enum4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/enum4/test.desc +++ b/regression/cbmc/enum4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/enum6/test.desc b/regression/cbmc/enum6/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/enum6/test.desc +++ b/regression/cbmc/enum6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/enum7/test.desc b/regression/cbmc/enum7/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/enum7/test.desc +++ b/regression/cbmc/enum7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/enum8/test.desc b/regression/cbmc/enum8/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/enum8/test.desc +++ b/regression/cbmc/enum8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/enum_is_in_range/enum_test3-simplified.desc b/regression/cbmc/enum_is_in_range/enum_test3-simplified.desc index a13c311d41c..d1c7ba53cbc 100644 --- a/regression/cbmc/enum_is_in_range/enum_test3-simplified.desc +++ b/regression/cbmc/enum_is_in_range/enum_test3-simplified.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend enum_test3.c --show-goto-functions 0 ≤ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ∧ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ≤ 4$ diff --git a/regression/cbmc/enum_is_in_range/enum_test3.desc b/regression/cbmc/enum_is_in_range/enum_test3.desc index f5a94e90126..3acc973c35e 100644 --- a/regression/cbmc/enum_is_in_range/enum_test3.desc +++ b/regression/cbmc/enum_is_in_range/enum_test3.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend enum_test3.c ^EXIT=0$ diff --git a/regression/cbmc/enum_is_in_range/enum_test7.desc b/regression/cbmc/enum_is_in_range/enum_test7.desc index 613a2cbc8f9..abd2b22e843 100644 --- a/regression/cbmc/enum_is_in_range/enum_test7.desc +++ b/regression/cbmc/enum_is_in_range/enum_test7.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend enum_test7.c ^EXIT=0$ diff --git a/regression/cbmc/enum_is_in_range/format.desc b/regression/cbmc/enum_is_in_range/format.desc index 6de3db06fa6..8efd942f74a 100644 --- a/regression/cbmc/enum_is_in_range/format.desc +++ b/regression/cbmc/enum_is_in_range/format.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend no_duplicate.c --show-goto-functions main::1::e = 1 ∨ main::1::e = 2 ∨ main::1::e = 4 ∨ main::1::e = 8 diff --git a/regression/cbmc/enum_is_in_range/no_duplicate.desc b/regression/cbmc/enum_is_in_range/no_duplicate.desc index 20c2ce2693b..f9ba922ed11 100644 --- a/regression/cbmc/enum_is_in_range/no_duplicate.desc +++ b/regression/cbmc/enum_is_in_range/no_duplicate.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend no_duplicate.c --enum-range-check ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/enum_underlying_type_01/test.desc b/regression/cbmc/enum_underlying_type_01/test.desc index b9a3d7c2794..cf442150f67 100644 --- a/regression/cbmc/enum_underlying_type_01/test.desc +++ b/regression/cbmc/enum_underlying_type_01/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/enum_underlying_type_02/test.desc b/regression/cbmc/enum_underlying_type_02/test.desc index 1bb30ef4b5d..0efecca0335 100644 --- a/regression/cbmc/enum_underlying_type_02/test.desc +++ b/regression/cbmc/enum_underlying_type_02/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=6$ diff --git a/regression/cbmc/enum_underlying_type_03/test.desc b/regression/cbmc/enum_underlying_type_03/test.desc index 41f9982a334..77751f8aefc 100644 --- a/regression/cbmc/enum_underlying_type_03/test.desc +++ b/regression/cbmc/enum_underlying_type_03/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=6$ diff --git a/regression/cbmc/equality_through_array1/test.desc b/regression/cbmc/equality_through_array1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/equality_through_array1/test.desc +++ b/regression/cbmc/equality_through_array1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/equality_through_array2/test.desc b/regression/cbmc/equality_through_array2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/equality_through_array2/test.desc +++ b/regression/cbmc/equality_through_array2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/equality_through_array3/test.desc b/regression/cbmc/equality_through_array3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/equality_through_array3/test.desc +++ b/regression/cbmc/equality_through_array3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/equality_through_array4/test.desc b/regression/cbmc/equality_through_array4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/equality_through_array4/test.desc +++ b/regression/cbmc/equality_through_array4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/equality_through_array5/test.desc b/regression/cbmc/equality_through_array5/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/equality_through_array5/test.desc +++ b/regression/cbmc/equality_through_array5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/equality_through_array6/test.desc b/regression/cbmc/equality_through_array6/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/equality_through_array6/test.desc +++ b/regression/cbmc/equality_through_array6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/extern1/test.desc b/regression/cbmc/extern1/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/extern1/test.desc +++ b/regression/cbmc/extern1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/extern2/test.desc b/regression/cbmc/extern2/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/extern2/test.desc +++ b/regression/cbmc/extern2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/extern3/test.desc b/regression/cbmc/extern3/test.desc index 578c27b1fa2..8ec8f46374e 100644 --- a/regression/cbmc/extern3/test.desc +++ b/regression/cbmc/extern3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/extern4/test.desc b/regression/cbmc/extern4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/extern4/test.desc +++ b/regression/cbmc/extern4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/extern5/test.desc b/regression/cbmc/extern5/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/extern5/test.desc +++ b/regression/cbmc/extern5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/extern_initialization1/test.desc b/regression/cbmc/extern_initialization1/test.desc index 73b0a6abe16..934fbe2fe2d 100644 --- a/regression/cbmc/extern_initialization1/test.desc +++ b/regression/cbmc/extern_initialization1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend file1.c file2.c ^EXIT=10$ diff --git a/regression/cbmc/extern_initialization2/test.desc b/regression/cbmc/extern_initialization2/test.desc index 8a09111c3b1..6a8056da7e4 100644 --- a/regression/cbmc/extern_initialization2/test.desc +++ b/regression/cbmc/extern_initialization2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend file1.c file2.c ^EXIT=0$ diff --git a/regression/cbmc/field-sensitivity10/test.desc b/regression/cbmc/field-sensitivity10/test.desc index b1d83b1c4c2..0ac74f6391c 100644 --- a/regression/cbmc/field-sensitivity10/test.desc +++ b/regression/cbmc/field-sensitivity10/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --show-vcc main::1::a1!0@1#2\.\.y = diff --git a/regression/cbmc/field-sensitivity14/test.desc b/regression/cbmc/field-sensitivity14/test.desc index d1748c78147..fbc7cec277d 100644 --- a/regression/cbmc/field-sensitivity14/test.desc +++ b/regression/cbmc/field-sensitivity14/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^Generated \d+ VCC\(s\), 0 remaining after simplification$ diff --git a/regression/cbmc/field-sensitivity6/test.desc b/regression/cbmc/field-sensitivity6/test.desc index a976d428bb5..6a5e6b588e2 100644 --- a/regression/cbmc/field-sensitivity6/test.desc +++ b/regression/cbmc/field-sensitivity6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --show-vcc main::1::b1!0@1#2\.\.a\.\.x = diff --git a/regression/cbmc/field-sensitivity7/test.desc b/regression/cbmc/field-sensitivity7/test.desc index 7b97c8c7d95..b473d8d934a 100644 --- a/regression/cbmc/field-sensitivity7/test.desc +++ b/regression/cbmc/field-sensitivity7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --show-vcc main::1::a1!0@1#2\.\.y = diff --git a/regression/cbmc/field-sensitivity8/test.desc b/regression/cbmc/field-sensitivity8/test.desc index 0d0db3d2bff..4219fec651e 100644 --- a/regression/cbmc/field-sensitivity8/test.desc +++ b/regression/cbmc/field-sensitivity8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --show-vcc main::1::a1!0@1#2\.\.y = diff --git a/regression/cbmc/for-break1/test.desc b/regression/cbmc/for-break1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/for-break1/test.desc +++ b/regression/cbmc/for-break1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/full_slice3/test.desc b/regression/cbmc/full_slice3/test.desc index 9f1003d166a..b3eaff9c7a1 100644 --- a/regression/cbmc/full_slice3/test.desc +++ b/regression/cbmc/full_slice3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --full-slice ^EXIT=0$ diff --git a/regression/cbmc/function-return-no-body1/test.desc b/regression/cbmc/function-return-no-body1/test.desc index 17f1370937f..e500f2698e5 100644 --- a/regression/cbmc/function-return-no-body1/test.desc +++ b/regression/cbmc/function-return-no-body1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --xml-ui activate-multi-line-match diff --git a/regression/cbmc/function_option1/test.desc b/regression/cbmc/function_option1/test.desc index 521d7365c2f..0aa58545b2f 100644 --- a/regression/cbmc/function_option1/test.desc +++ b/regression/cbmc/function_option1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --function f ^EXIT=0$ diff --git a/regression/cbmc/gcc_attribute_alias1/test.desc b/regression/cbmc/gcc_attribute_alias1/test.desc index 466da18b2b5..00550a6e62f 100644 --- a/regression/cbmc/gcc_attribute_alias1/test.desc +++ b/regression/cbmc/gcc_attribute_alias1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/gcc_builtin_add_overflow/type-conflict-2.desc b/regression/cbmc/gcc_builtin_add_overflow/type-conflict-2.desc index d936698a5ca..4db9cb24eb1 100644 --- a/regression/cbmc/gcc_builtin_add_overflow/type-conflict-2.desc +++ b/regression/cbmc/gcc_builtin_add_overflow/type-conflict-2.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend type-conflict.c line 14 function main: __builtin_add_overflow takes exactly 3 arguments, but 2 were provided$ diff --git a/regression/cbmc/gcc_builtin_add_overflow/type-conflict.desc b/regression/cbmc/gcc_builtin_add_overflow/type-conflict.desc index 61831ad63ab..3b0ddcd2eb3 100644 --- a/regression/cbmc/gcc_builtin_add_overflow/type-conflict.desc +++ b/regression/cbmc/gcc_builtin_add_overflow/type-conflict.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend type-conflict.c -DCONFLICT1 line 12 function main: error: __builtin_add_overflow has signature __builtin_add_overflow\(integral, integral, integral\*\), but argument 3 \(r\) has type `signed int`$ diff --git a/regression/cbmc/gcc_builtin_va_arg_one/test.desc b/regression/cbmc/gcc_builtin_va_arg_one/test.desc index ccc7c4dd8e7..7bb309317e2 100644 --- a/regression/cbmc/gcc_builtin_va_arg_one/test.desc +++ b/regression/cbmc/gcc_builtin_va_arg_one/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c function .* is not declared diff --git a/regression/cbmc/gcc_c99-bool-1/test.desc b/regression/cbmc/gcc_c99-bool-1/test.desc index d82c02459fc..db9df6a498e 100644 --- a/regression/cbmc/gcc_c99-bool-1/test.desc +++ b/regression/cbmc/gcc_c99-bool-1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend c99-bool-1.c ^EXIT=0$ diff --git a/regression/cbmc/gcc_conditional_expr1/test.desc b/regression/cbmc/gcc_conditional_expr1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/gcc_conditional_expr1/test.desc +++ b/regression/cbmc/gcc_conditional_expr1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/gcc_local_label1/test.desc b/regression/cbmc/gcc_local_label1/test.desc index bb760ec3230..bb401e87482 100644 --- a/regression/cbmc/gcc_local_label1/test.desc +++ b/regression/cbmc/gcc_local_label1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 1 --no-unwinding-assertions ^EXIT=10$ diff --git a/regression/cbmc/gcc_statement_expression1/test.desc b/regression/cbmc/gcc_statement_expression1/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/gcc_statement_expression1/test.desc +++ b/regression/cbmc/gcc_statement_expression1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/gcc_statement_expression2/test.desc b/regression/cbmc/gcc_statement_expression2/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/gcc_statement_expression2/test.desc +++ b/regression/cbmc/gcc_statement_expression2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/gcc_statement_expression3/test.desc b/regression/cbmc/gcc_statement_expression3/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/gcc_statement_expression3/test.desc +++ b/regression/cbmc/gcc_statement_expression3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/gcc_statement_expression4/test.desc b/regression/cbmc/gcc_statement_expression4/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/gcc_statement_expression4/test.desc +++ b/regression/cbmc/gcc_statement_expression4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/gcc_statement_expression5/test.desc b/regression/cbmc/gcc_statement_expression5/test.desc index 9c96469df12..9f5bd9e1119 100644 --- a/regression/cbmc/gcc_statement_expression5/test.desc +++ b/regression/cbmc/gcc_statement_expression5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/gcc_switch_case_range1/test.desc b/regression/cbmc/gcc_switch_case_range1/test.desc index 8bcbbb03111..f3a9f1a2097 100644 --- a/regression/cbmc/gcc_switch_case_range1/test.desc +++ b/regression/cbmc/gcc_switch_case_range1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/gcc_switch_case_range2/test.desc b/regression/cbmc/gcc_switch_case_range2/test.desc index cfa6e0b1e20..819b231c7c3 100644 --- a/regression/cbmc/gcc_switch_case_range2/test.desc +++ b/regression/cbmc/gcc_switch_case_range2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/gcc_vector2/test.desc b/regression/cbmc/gcc_vector2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/gcc_vector2/test.desc +++ b/regression/cbmc/gcc_vector2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/gcc_vector3/test.desc b/regression/cbmc/gcc_vector3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/gcc_vector3/test.desc +++ b/regression/cbmc/gcc_vector3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/goto2/test.desc b/regression/cbmc/goto2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/goto2/test.desc +++ b/regression/cbmc/goto2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/goto3/test.desc b/regression/cbmc/goto3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/goto3/test.desc +++ b/regression/cbmc/goto3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/goto5/test.desc b/regression/cbmc/goto5/test.desc index 6de79559914..b59d561e220 100644 --- a/regression/cbmc/goto5/test.desc +++ b/regression/cbmc/goto5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/havoc_slice/test_array_slice_1.desc b/regression/cbmc/havoc_slice/test_array_slice_1.desc index fc0c3c011d0..5792188b700 100644 --- a/regression/cbmc/havoc_slice/test_array_slice_1.desc +++ b/regression/cbmc/havoc_slice/test_array_slice_1.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test_array_slice_1.c ^EXIT=10$ diff --git a/regression/cbmc/havoc_slice/test_array_slice_2.desc b/regression/cbmc/havoc_slice/test_array_slice_2.desc index a6ae75f2598..14155278b3e 100644 --- a/regression/cbmc/havoc_slice/test_array_slice_2.desc +++ b/regression/cbmc/havoc_slice/test_array_slice_2.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test_array_slice_2.c ^EXIT=10$ diff --git a/regression/cbmc/havoc_slice/test_whole_array.desc b/regression/cbmc/havoc_slice/test_whole_array.desc index 93b0da7bc5d..7c6102e062f 100644 --- a/regression/cbmc/havoc_slice/test_whole_array.desc +++ b/regression/cbmc/havoc_slice/test_whole_array.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test_whole_array.c ^EXIT=10$ diff --git a/regression/cbmc/havoc_slice/test_whole_array_with_offset.desc b/regression/cbmc/havoc_slice/test_whole_array_with_offset.desc index 13751786467..2794cf08ab4 100644 --- a/regression/cbmc/havoc_slice/test_whole_array_with_offset.desc +++ b/regression/cbmc/havoc_slice/test_whole_array_with_offset.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test_whole_array_with_offset.c ^EXIT=10$ diff --git a/regression/cbmc/havoc_slice_checks/full-slice.desc b/regression/cbmc/havoc_slice_checks/full-slice.desc index 01af361a4ba..40d201dbe26 100644 --- a/regression/cbmc/havoc_slice_checks/full-slice.desc +++ b/regression/cbmc/havoc_slice_checks/full-slice.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --full-slice ^\[main\.assertion\.\d+\] line 9 assertion havoc_slice W_OK.*: FAILURE$ diff --git a/regression/cbmc/havoc_undefined_functions/test.desc b/regression/cbmc/havoc_undefined_functions/test.desc index 9a9f9b98bd0..047a6acab1e 100644 --- a/regression/cbmc/havoc_undefined_functions/test.desc +++ b/regression/cbmc/havoc_undefined_functions/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --havoc-undefined-functions ^EXIT=10$ diff --git a/regression/cbmc/hex_string1/test.desc b/regression/cbmc/hex_string1/test.desc index 12fc8ce06e1..ad10409bb6f 100644 --- a/regression/cbmc/hex_string1/test.desc +++ b/regression/cbmc/hex_string1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/if2/test.desc b/regression/cbmc/if2/test.desc index 6de79559914..b59d561e220 100644 --- a/regression/cbmc/if2/test.desc +++ b/regression/cbmc/if2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/incomplete-sizeof/array.desc b/regression/cbmc/incomplete-sizeof/array.desc index 2287c0b74b7..a1dd65b48f4 100644 --- a/regression/cbmc/incomplete-sizeof/array.desc +++ b/regression/cbmc/incomplete-sizeof/array.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend array.c ^EXIT=6$ diff --git a/regression/cbmc/incomplete-sizeof/enum.desc b/regression/cbmc/incomplete-sizeof/enum.desc index 0b8b1902d86..1130d80ebf1 100644 --- a/regression/cbmc/incomplete-sizeof/enum.desc +++ b/regression/cbmc/incomplete-sizeof/enum.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend enum.c ^EXIT=6$ diff --git a/regression/cbmc/incomplete-sizeof/struct.desc b/regression/cbmc/incomplete-sizeof/struct.desc index ba39504cbb4..28d6e1ba462 100644 --- a/regression/cbmc/incomplete-sizeof/struct.desc +++ b/regression/cbmc/incomplete-sizeof/struct.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend struct.c ^EXIT=6$ diff --git a/regression/cbmc/incomplete-sizeof/union.desc b/regression/cbmc/incomplete-sizeof/union.desc index 7571d615926..d334155e59e 100644 --- a/regression/cbmc/incomplete-sizeof/union.desc +++ b/regression/cbmc/incomplete-sizeof/union.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend union.c ^EXIT=6$ diff --git a/regression/cbmc/incomplete-structs/test.desc b/regression/cbmc/incomplete-structs/test.desc index 47de5a75263..0a09ba18b36 100644 --- a/regression/cbmc/incomplete-structs/test.desc +++ b/regression/cbmc/incomplete-structs/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend typesmain.c types1.c types2.c types3.c reason for conflict at \*#this.u: number of members is different \(3/0\) diff --git a/regression/cbmc/inequality-with-constant-normalisation/test.desc b/regression/cbmc/inequality-with-constant-normalisation/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/inequality-with-constant-normalisation/test.desc +++ b/regression/cbmc/inequality-with-constant-normalisation/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/inequality-with-constant-normalisation1/test.desc b/regression/cbmc/inequality-with-constant-normalisation1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/inequality-with-constant-normalisation1/test.desc +++ b/regression/cbmc/inequality-with-constant-normalisation1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/inline1/test.desc b/regression/cbmc/inline1/test.desc index af20f90c655..645f563290d 100644 --- a/regression/cbmc/inline1/test.desc +++ b/regression/cbmc/inline1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c module.c ^EXIT=0$ diff --git a/regression/cbmc/integer-assignments1/integer-typecheck.desc b/regression/cbmc/integer-assignments1/integer-typecheck.desc index 612dfad45eb..a4662f6fd42 100644 --- a/regression/cbmc/integer-assignments1/integer-typecheck.desc +++ b/regression/cbmc/integer-assignments1/integer-typecheck.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-goto-functions ^[[:space:]]*ASSIGN main::1::b := main::1::b \* cast\(100, ℤ\)$ diff --git a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc index 2369a0bd857..c733fcb1217 100644 --- a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc +++ b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc @@ -1,4 +1,4 @@ -CORE smt-backend +CORE smt-backend new-smt-backend short.c --smt2 ^EXIT=0$ diff --git a/regression/cbmc/json-interface1/test.desc b/regression/cbmc/json-interface1/test.desc index 083df61a021..998a2a65201 100644 --- a/regression/cbmc/json-interface1/test.desc +++ b/regression/cbmc/json-interface1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend --json-interface < test.json activate-multi-line-match diff --git a/regression/cbmc/json-interface1/test_wrong_flag.desc b/regression/cbmc/json-interface1/test_wrong_flag.desc index b1210068e2e..b57e4d64a9a 100644 --- a/regression/cbmc/json-interface1/test_wrong_flag.desc +++ b/regression/cbmc/json-interface1/test_wrong_flag.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend --json-interface < test_wrong_flag.json ^EXIT=6$ diff --git a/regression/cbmc/json-interface1/test_wrong_option.desc b/regression/cbmc/json-interface1/test_wrong_option.desc index c1b57e8574b..08080cbf4f5 100644 --- a/regression/cbmc/json-interface1/test_wrong_option.desc +++ b/regression/cbmc/json-interface1/test_wrong_option.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend --json-interface < test_wrong_option.json ^EXIT=6$ diff --git a/regression/cbmc/json-ui/no_entry.desc b/regression/cbmc/json-ui/no_entry.desc index ea376532787..88514dddbe5 100644 --- a/regression/cbmc/json-ui/no_entry.desc +++ b/regression/cbmc/json-ui/no_entry.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend no_entry.c --json-ui activate-multi-line-match diff --git a/regression/cbmc/json-ui/syntax_error.desc b/regression/cbmc/json-ui/syntax_error.desc index b7c3530a7bc..4a4942ac72d 100644 --- a/regression/cbmc/json-ui/syntax_error.desc +++ b/regression/cbmc/json-ui/syntax_error.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend syntax_error.c --json-ui activate-multi-line-match diff --git a/regression/cbmc/json1/test.desc b/regression/cbmc/json1/test.desc index b9eb6a30118..1a15bc47af9 100644 --- a/regression/cbmc/json1/test.desc +++ b/regression/cbmc/json1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --json-ui --stop-on-fail activate-multi-line-match diff --git a/regression/cbmc/link_json_symtabs/test.desc b/regression/cbmc/link_json_symtabs/test.desc index c6f6ebe9068..c5a0c306551 100644 --- a/regression/cbmc/link_json_symtabs/test.desc +++ b/regression/cbmc/link_json_symtabs/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend one.json_symtab two.json_symtab ^EXIT=0$ diff --git a/regression/cbmc/little-endian-array1/test.desc b/regression/cbmc/little-endian-array1/test.desc index 9845e70d84b..b177f2412ca 100644 --- a/regression/cbmc/little-endian-array1/test.desc +++ b/regression/cbmc/little-endian-array1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/locations1/test.desc b/regression/cbmc/locations1/test.desc index 12c44d464cd..1f1a6e1ed93 100644 --- a/regression/cbmc/locations1/test.desc +++ b/regression/cbmc/locations1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --signed-overflow-check ^EXIT=0$ diff --git a/regression/cbmc/loophead-trace/test-json.desc b/regression/cbmc/loophead-trace/test-json.desc index 9754b659021..a8c254405af 100644 --- a/regression/cbmc/loophead-trace/test-json.desc +++ b/regression/cbmc/loophead-trace/test-json.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --unwind 6 test.c --trace --json-ui --partial-loops --slice-formula activate-multi-line-match diff --git a/regression/cbmc/loophead-trace/test-xml.desc b/regression/cbmc/loophead-trace/test-xml.desc index b039701d87d..17bfd844b3f 100644 --- a/regression/cbmc/loophead-trace/test-xml.desc +++ b/regression/cbmc/loophead-trace/test-xml.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --unwind 6 test.c --trace --xml-ui --partial-loops --slice-formula activate-multi-line-match diff --git a/regression/cbmc/malloc-may-fail/test.desc b/regression/cbmc/malloc-may-fail/test.desc index fb64c203397..383fe856bee 100644 --- a/regression/cbmc/malloc-may-fail/test.desc +++ b/regression/cbmc/malloc-may-fail/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --malloc-may-fail --malloc-fail-null ^EXIT=10$ diff --git a/regression/cbmc/malloc-may-fail/test_without_option.desc b/regression/cbmc/malloc-may-fail/test_without_option.desc index f0c5e3ae1ef..776b1df6563 100644 --- a/regression/cbmc/malloc-may-fail/test_without_option.desc +++ b/regression/cbmc/malloc-may-fail/test_without_option.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/malloc-too-large/largest_representable.desc b/regression/cbmc/malloc-too-large/largest_representable.desc index d6f9fd63d14..8f0bbae1bd7 100644 --- a/regression/cbmc/malloc-too-large/largest_representable.desc +++ b/regression/cbmc/malloc-too-large/largest_representable.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend largest_representable.c --malloc-fail-assert ^EXIT=0$ diff --git a/regression/cbmc/malloc-too-large/max_size.desc b/regression/cbmc/malloc-too-large/max_size.desc index 783470072e3..79bc9dd5320 100644 --- a/regression/cbmc/malloc-too-large/max_size.desc +++ b/regression/cbmc/malloc-too-large/max_size.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend max_size.c --malloc-fail-assert ^EXIT=10$ diff --git a/regression/cbmc/malloc-too-large/one_byte_too_large.desc b/regression/cbmc/malloc-too-large/one_byte_too_large.desc index dbec5e98957..e1a2505daf8 100644 --- a/regression/cbmc/malloc-too-large/one_byte_too_large.desc +++ b/regression/cbmc/malloc-too-large/one_byte_too_large.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend one_byte_too_large.c --malloc-fail-null ^EXIT=10$ diff --git a/regression/cbmc/member1/test.desc b/regression/cbmc/member1/test.desc index 22feeb5e857..9dfd17b7527 100644 --- a/regression/cbmc/member1/test.desc +++ b/regression/cbmc/member1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc index e40bdd895b1..011e23bce3b 100644 --- a/regression/cbmc/memory_allocation1/test.desc +++ b/regression/cbmc/memory_allocation1/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE broken-smt-backend new-smt-backend main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/memory_allocation2/test.desc b/regression/cbmc/memory_allocation2/test.desc index c88637311c2..6dc86f1f08e 100644 --- a/regression/cbmc/memory_allocation2/test.desc +++ b/regression/cbmc/memory_allocation2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --bounds-check ^EXIT=10$ diff --git a/regression/cbmc/memset2/test.desc b/regression/cbmc/memset2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/memset2/test.desc +++ b/regression/cbmc/memset2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/memset3/test.desc b/regression/cbmc/memset3/test.desc index be58134bdcb..fea96178727 100644 --- a/regression/cbmc/memset3/test.desc +++ b/regression/cbmc/memset3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/mm_io1/test.desc b/regression/cbmc/mm_io1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/mm_io1/test.desc +++ b/regression/cbmc/mm_io1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/nested_label1/test.desc b/regression/cbmc/nested_label1/test.desc index 401b46a8d28..22a71cb70eb 100644 --- a/regression/cbmc/nested_label1/test.desc +++ b/regression/cbmc/nested_label1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/nondet-pointer/nondet-pointer1.desc b/regression/cbmc/nondet-pointer/nondet-pointer1.desc index d4834e848eb..eef0545637e 100644 --- a/regression/cbmc/nondet-pointer/nondet-pointer1.desc +++ b/regression/cbmc/nondet-pointer/nondet-pointer1.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend nondet-pointer1.c ^EXIT=0$ diff --git a/regression/cbmc/nondet-pointer/nondet-pointer2.desc b/regression/cbmc/nondet-pointer/nondet-pointer2.desc index d4834e848eb..eef0545637e 100644 --- a/regression/cbmc/nondet-pointer/nondet-pointer2.desc +++ b/regression/cbmc/nondet-pointer/nondet-pointer2.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend nondet-pointer1.c ^EXIT=0$ diff --git a/regression/cbmc/nondet-pointer/nondet-pointer3.desc b/regression/cbmc/nondet-pointer/nondet-pointer3.desc index d4834e848eb..eef0545637e 100644 --- a/regression/cbmc/nondet-pointer/nondet-pointer3.desc +++ b/regression/cbmc/nondet-pointer/nondet-pointer3.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend nondet-pointer1.c ^EXIT=0$ diff --git a/regression/cbmc/nondet-pointer/nondet-pointer4.desc b/regression/cbmc/nondet-pointer/nondet-pointer4.desc index d4834e848eb..eef0545637e 100644 --- a/regression/cbmc/nondet-pointer/nondet-pointer4.desc +++ b/regression/cbmc/nondet-pointer/nondet-pointer4.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend nondet-pointer1.c ^EXIT=0$ diff --git a/regression/cbmc/nondet-pointer/nondet-pointer5.desc b/regression/cbmc/nondet-pointer/nondet-pointer5.desc index d4834e848eb..eef0545637e 100644 --- a/regression/cbmc/nondet-pointer/nondet-pointer5.desc +++ b/regression/cbmc/nondet-pointer/nondet-pointer5.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend nondet-pointer1.c ^EXIT=0$ diff --git a/regression/cbmc/noop2/test.desc b/regression/cbmc/noop2/test.desc index 7057e2afbe7..86980b336e4 100644 --- a/regression/cbmc/noop2/test.desc +++ b/regression/cbmc/noop2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c -win32 ^EXIT=0$ diff --git a/regression/cbmc/null2/test.desc b/regression/cbmc/null2/test.desc index 1d6654a4859..a8631c101f9 100644 --- a/regression/cbmc/null2/test.desc +++ b/regression/cbmc/null2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/null3/test.desc b/regression/cbmc/null3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/null3/test.desc +++ b/regression/cbmc/null3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/null5/test.desc b/regression/cbmc/null5/test.desc index 926be8072d2..f6507f3600b 100644 --- a/regression/cbmc/null5/test.desc +++ b/regression/cbmc/null5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/null6/test.desc b/regression/cbmc/null6/test.desc index b312cea5fe3..9a8e1f01802 100644 --- a/regression/cbmc/null6/test.desc +++ b/regression/cbmc/null6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/null7/test.desc b/regression/cbmc/null7/test.desc index 45989540170..33fddc1a285 100644 --- a/regression/cbmc/null7/test.desc +++ b/regression/cbmc/null7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/object-bits-parsing/non_numeric.desc b/regression/cbmc/object-bits-parsing/non_numeric.desc index ca52caf9c89..b4ad2a40335 100644 --- a/regression/cbmc/object-bits-parsing/non_numeric.desc +++ b/regression/cbmc/object-bits-parsing/non_numeric.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --object-bits foobar Value of "foobar" given for object-bits is not a valid unsigned integer. diff --git a/regression/cbmc/object-bits-parsing/too_large.desc b/regression/cbmc/object-bits-parsing/too_large.desc index 4bf82c9dc95..41581fd9d7c 100644 --- a/regression/cbmc/object-bits-parsing/too_large.desc +++ b/regression/cbmc/object-bits-parsing/too_large.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --object-bits 65 Value of "65" given for object-bits is out of range. diff --git a/regression/cbmc/object-bits-parsing/valid.desc b/regression/cbmc/object-bits-parsing/valid.desc index 6cf345f5522..bfde0d5699f 100644 --- a/regression/cbmc/object-bits-parsing/valid.desc +++ b/regression/cbmc/object-bits-parsing/valid.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --object-bits 8 ^EXIT=0$ diff --git a/regression/cbmc/object-bits-parsing/zero.desc b/regression/cbmc/object-bits-parsing/zero.desc index 4471b3c7337..1603bf99d37 100644 --- a/regression/cbmc/object-bits-parsing/zero.desc +++ b/regression/cbmc/object-bits-parsing/zero.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --object-bits 0 Value of "0" given for object-bits is out of range. diff --git a/regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc b/regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc index 4059cdb1c85..6e59198bcab 100644 --- a/regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc +++ b/regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend leftshift_overflow.c --signed-overflow-check --c99 --full-slice ^EXIT=10$ diff --git a/regression/cbmc/path-branch-pointer-call/test.desc b/regression/cbmc/path-branch-pointer-call/test.desc index 5ea1d977cab..a3434a8d52e 100644 --- a/regression/cbmc/path-branch-pointer-call/test.desc +++ b/regression/cbmc/path-branch-pointer-call/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --paths lifo ^EXIT=0$ diff --git a/regression/cbmc/path-per-path-vccs/test.desc b/regression/cbmc/path-per-path-vccs/test.desc index d399e5b2ddb..09f6e02de12 100644 --- a/regression/cbmc/path-per-path-vccs/test.desc +++ b/regression/cbmc/path-per-path-vccs/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --paths lifo --unwind 1 --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/phi-merge_uninitialized_values/dynamic.desc b/regression/cbmc/phi-merge_uninitialized_values/dynamic.desc index 94054b4d376..23fe3760425 100644 --- a/regression/cbmc/phi-merge_uninitialized_values/dynamic.desc +++ b/regression/cbmc/phi-merge_uninitialized_values/dynamic.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --function dynamicAllocationUninitialized --show-vcc activate-multi-line-match diff --git a/regression/cbmc/phi-merge_uninitialized_values/global.desc b/regression/cbmc/phi-merge_uninitialized_values/global.desc index 5891ab3a6bb..b561d311e7e 100644 --- a/regression/cbmc/phi-merge_uninitialized_values/global.desc +++ b/regression/cbmc/phi-merge_uninitialized_values/global.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --function globalUninitialized --show-vcc activate-multi-line-match diff --git a/regression/cbmc/phi-merge_uninitialized_values/local.desc b/regression/cbmc/phi-merge_uninitialized_values/local.desc index d588bf234e2..b9c91fa87f1 100644 --- a/regression/cbmc/phi-merge_uninitialized_values/local.desc +++ b/regression/cbmc/phi-merge_uninitialized_values/local.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --function localUninitialized --show-vcc activate-multi-line-match diff --git a/regression/cbmc/phi-merge_uninitialized_values/static_local.desc b/regression/cbmc/phi-merge_uninitialized_values/static_local.desc index 0896809ce1d..37f196ebabe 100644 --- a/regression/cbmc/phi-merge_uninitialized_values/static_local.desc +++ b/regression/cbmc/phi-merge_uninitialized_values/static_local.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --function staticLocalUninitialized --show-vcc activate-multi-line-match diff --git a/regression/cbmc/pointer-check-01/test.desc b/regression/cbmc/pointer-check-01/test.desc index f86851a0aa1..fea45a594cb 100644 --- a/regression/cbmc/pointer-check-01/test.desc +++ b/regression/cbmc/pointer-check-01/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/pointer-check-02/test.desc b/regression/cbmc/pointer-check-02/test.desc index 2e0645ee56a..9cebe7a9203 100644 --- a/regression/cbmc/pointer-check-02/test.desc +++ b/regression/cbmc/pointer-check-02/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/pointer-extra-checks/test.desc b/regression/cbmc/pointer-extra-checks/test.desc index b793e876bf8..528cf397a1b 100644 --- a/regression/cbmc/pointer-extra-checks/test.desc +++ b/regression/cbmc/pointer-extra-checks/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc index 7b82cc87646..bf0755102ff 100644 --- a/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc +++ b/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc index 716670ff6f7..d14ccb163be 100644 --- a/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc +++ b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --function func --min-null-tree-depth 10 --max-nondet-tree-depth 2 --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc index 7b82cc87646..bf0755102ff 100644 --- a/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc +++ b/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/cbmc/pointer-function-parameters/test.desc index 7529d7e143f..b9bf5e8ae2a 100644 --- a/regression/cbmc/pointer-function-parameters/test.desc +++ b/regression/cbmc/pointer-function-parameters/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --function f ^EXIT=0$ diff --git a/regression/cbmc/pointer-predicates/at_bounds1.desc b/regression/cbmc/pointer-predicates/at_bounds1.desc index 376ddfa608d..5cbaf19b023 100644 --- a/regression/cbmc/pointer-predicates/at_bounds1.desc +++ b/regression/cbmc/pointer-predicates/at_bounds1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE broken-smt-backend new-smt-backend at_bounds1.c --pointer-primitive-check --malloc-fail-null ^\[main.pointer_primitives.\d+\] line 13 pointer outside object bounds in R_OK\(q \+ (\(signed (long (long )?)?int\))?1, (\(unsigned (long (long )?)?int\))?0\): FAILURE$ diff --git a/regression/cbmc/pointer-predicates/in_range1.desc b/regression/cbmc/pointer-predicates/in_range1.desc index 3465178e375..c33bb53ca08 100644 --- a/regression/cbmc/pointer-predicates/in_range1.desc +++ b/regression/cbmc/pointer-predicates/in_range1.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend in_range1.c ^EXIT=0$ diff --git a/regression/cbmc/pointer-primitive-check-01/test.desc b/regression/cbmc/pointer-primitive-check-01/test.desc index fb52df0c4de..721e9542d0b 100644 --- a/regression/cbmc/pointer-primitive-check-01/test.desc +++ b/regression/cbmc/pointer-primitive-check-01/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-primitive-check ^EXIT=10$ diff --git a/regression/cbmc/pointer-primitive-check-02/test.desc b/regression/cbmc/pointer-primitive-check-02/test.desc index 315e2d255c7..dae95109dcf 100644 --- a/regression/cbmc/pointer-primitive-check-02/test.desc +++ b/regression/cbmc/pointer-primitive-check-02/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-primitive-check ^EXIT=0$ diff --git a/regression/cbmc/pointer-primitive-check-04/test.desc b/regression/cbmc/pointer-primitive-check-04/test.desc index 3c9f2d5f074..160942f8359 100644 --- a/regression/cbmc/pointer-primitive-check-04/test.desc +++ b/regression/cbmc/pointer-primitive-check-04/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-primitive-check ^EXIT=10$ diff --git a/regression/cbmc/points-to-sets/test_json.desc b/regression/cbmc/points-to-sets/test_json.desc index 3e62c77d638..cafb55493e1 100644 --- a/regression/cbmc/points-to-sets/test_json.desc +++ b/regression/cbmc/points-to-sets/test_json.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-points-to-sets --json-ui activate-multi-line-match diff --git a/regression/cbmc/points-to-sets/test_xml.desc b/regression/cbmc/points-to-sets/test_xml.desc index d4bf269cbb3..f4a3654cd5b 100644 --- a/regression/cbmc/points-to-sets/test_xml.desc +++ b/regression/cbmc/points-to-sets/test_xml.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-points-to-sets --xml-ui ^EXIT=1$ diff --git a/regression/cbmc/pragma_cprover1/test.desc b/regression/cbmc/pragma_cprover1/test.desc index 2ed565c0062..64834a9dde9 100644 --- a/regression/cbmc/pragma_cprover1/test.desc +++ b/regression/cbmc/pragma_cprover1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --signed-overflow-check --bounds-check line 14 array 'y' upper bound in y\[\(signed long( long)? int\)1\]: FAILURE$ diff --git a/regression/cbmc/pragma_cprover3/test.desc b/regression/cbmc/pragma_cprover3/test.desc index c7e1faaa966..b00169d9ce2 100644 --- a/regression/cbmc/pragma_cprover3/test.desc +++ b/regression/cbmc/pragma_cprover3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-primitive-check ^main.c function main$ diff --git a/regression/cbmc/pragma_cprover_enable1/test.desc b/regression/cbmc/pragma_cprover_enable1/test.desc index 8113775430e..d00a262ecec 100644 --- a/regression/cbmc/pragma_cprover_enable1/test.desc +++ b/regression/cbmc/pragma_cprover_enable1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^\[main\.array_bounds\.1\] line \d+ array 'y' upper bound.*FAILURE$ diff --git a/regression/cbmc/pragma_cprover_enable2/test.desc b/regression/cbmc/pragma_cprover_enable2/test.desc index 9ddbded4bb7..038a1451b1e 100644 --- a/regression/cbmc/pragma_cprover_enable2/test.desc +++ b/regression/cbmc/pragma_cprover_enable2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^\[main\.overflow\.1\] line 13 arithmetic overflow on signed \+ in n \+ n: FAILURE$ diff --git a/regression/cbmc/pragma_cprover_enable3/test.desc b/regression/cbmc/pragma_cprover_enable3/test.desc index 951dc2c266d..e794568de05 100644 --- a/regression/cbmc/pragma_cprover_enable3/test.desc +++ b/regression/cbmc/pragma_cprover_enable3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^main.c function main$ diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc b/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc index c9e8430a6b4..c2c6ade8f9b 100644 --- a/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc +++ b/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^main.c function main$ diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc b/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc index 9e72ed21ec6..eb2eed4c87c 100644 --- a/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc +++ b/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-primitive-check ^main.c function main$ diff --git a/regression/cbmc/pragma_cprover_enable_disable_multiple/test.desc b/regression/cbmc/pragma_cprover_enable_disable_multiple/test.desc index 9a39bcf1b94..08129024a8d 100644 --- a/regression/cbmc/pragma_cprover_enable_disable_multiple/test.desc +++ b/regression/cbmc/pragma_cprover_enable_disable_multiple/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^file main.c line \d+ function main: Found enable and disable pragmas for pointer-primitive-check diff --git a/regression/cbmc/r_w_ok1/test.desc b/regression/cbmc/r_w_ok1/test.desc index 6a461a6a137..325c6fbf73a 100644 --- a/regression/cbmc/r_w_ok1/test.desc +++ b/regression/cbmc/r_w_ok1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c __CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$ diff --git a/regression/cbmc/r_w_ok10/test.desc b/regression/cbmc/r_w_ok10/test.desc index 54479c1b6d3..000e3e962ca 100644 --- a/regression/cbmc/r_w_ok10/test.desc +++ b/regression/cbmc/r_w_ok10/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-primitive-check ^EXIT=10$ diff --git a/regression/cbmc/r_w_ok2/test.desc b/regression/cbmc/r_w_ok2/test.desc index 278f468e130..22961959ca9 100644 --- a/regression/cbmc/r_w_ok2/test.desc +++ b/regression/cbmc/r_w_ok2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/r_w_ok5/test.desc b/regression/cbmc/r_w_ok5/test.desc index a39b6d1bf4b..21f3ffc9142 100644 --- a/regression/cbmc/r_w_ok5/test.desc +++ b/regression/cbmc/r_w_ok5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c \[main.assertion.1\] .*: SUCCESS diff --git a/regression/cbmc/r_w_ok6/test.desc b/regression/cbmc/r_w_ok6/test.desc index 4ec12d76677..78ce9c8e76e 100644 --- a/regression/cbmc/r_w_ok6/test.desc +++ b/regression/cbmc/r_w_ok6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c \[main.assertion.1\] .*: SUCCESS diff --git a/regression/cbmc/r_w_ok7/test.desc b/regression/cbmc/r_w_ok7/test.desc index a5d7e85c7dc..b3f90047725 100644 --- a/regression/cbmc/r_w_ok7/test.desc +++ b/regression/cbmc/r_w_ok7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c \[main.assertion.1\] .*: SUCCESS diff --git a/regression/cbmc/r_w_ok8/test.desc b/regression/cbmc/r_w_ok8/test.desc index 4102d81cb91..8ba781658d5 100644 --- a/regression/cbmc/r_w_ok8/test.desc +++ b/regression/cbmc/r_w_ok8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c \[main.assertion.1\] .*: SUCCESS diff --git a/regression/cbmc/r_w_ok9/simplify.desc b/regression/cbmc/r_w_ok9/simplify.desc index 55a118cca67..1b06cbb7098 100644 --- a/regression/cbmc/r_w_ok9/simplify.desc +++ b/regression/cbmc/r_w_ok9/simplify.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-goto-functions ^EXIT=0$ diff --git a/regression/cbmc/r_w_ok9/test.desc b/regression/cbmc/r_w_ok9/test.desc index c626baf6332..47c17aad3f3 100644 --- a/regression/cbmc/r_w_ok9/test.desc +++ b/regression/cbmc/r_w_ok9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c VERIFICATION SUCCESSFUL diff --git a/regression/cbmc/reachability-slice-interproc/test.desc b/regression/cbmc/reachability-slice-interproc/test.desc index c04ff07afc4..e44781801d1 100644 --- a/regression/cbmc/reachability-slice-interproc/test.desc +++ b/regression/cbmc/reachability-slice-interproc/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --reachability-slice-fb --show-goto-functions ^EXIT=0$ diff --git a/regression/cbmc/reachability-slice-interproc2/test.desc b/regression/cbmc/reachability-slice-interproc2/test.desc index b10acfc02b3..d566401f934 100644 --- a/regression/cbmc/reachability-slice-interproc2/test.desc +++ b/regression/cbmc/reachability-slice-interproc2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --reachability-slice --show-goto-functions ^EXIT=0$ diff --git a/regression/cbmc/reachability-slice-interproc3/test.desc b/regression/cbmc/reachability-slice-interproc3/test.desc index ccf9d04e679..58dfd98f172 100644 --- a/regression/cbmc/reachability-slice-interproc3/test.desc +++ b/regression/cbmc/reachability-slice-interproc3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --reachability-slice-fb --show-goto-functions ^EXIT=0$ diff --git a/regression/cbmc/reachability-slice/test.desc b/regression/cbmc/reachability-slice/test.desc index a8976affbe4..29c589ccbee 100644 --- a/regression/cbmc/reachability-slice/test.desc +++ b/regression/cbmc/reachability-slice/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --reachability-slice --show-goto-functions --cover location --property foo.coverage.2 ^EXIT=0$ diff --git a/regression/cbmc/reachability-slice/test2.desc b/regression/cbmc/reachability-slice/test2.desc index c20147249da..b61223c79d2 100644 --- a/regression/cbmc/reachability-slice/test2.desc +++ b/regression/cbmc/reachability-slice/test2.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --reachability-slice-fb --show-goto-functions --cover location --property foo.coverage.2 ^EXIT=0$ diff --git a/regression/cbmc/reachability-slice/test3.desc b/regression/cbmc/reachability-slice/test3.desc index 49191de1d92..c56f2a473f4 100644 --- a/regression/cbmc/reachability-slice/test3.desc +++ b/regression/cbmc/reachability-slice/test3.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --reachability-slice --show-goto-functions --cover location ^EXIT=0$ diff --git a/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc b/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc index a5bf8ec70eb..e47d8a997b3 100644 --- a/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc +++ b/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --malloc-may-fail --malloc-fail-null ^\[main.precondition_instance.\d+] line \d+ double free: SUCCESS$ diff --git a/regression/cbmc/residual-guards-1/test.desc b/regression/cbmc/residual-guards-1/test.desc index 2edbd291637..bd5d4122edb 100644 --- a/regression/cbmc/residual-guards-1/test.desc +++ b/regression/cbmc/residual-guards-1/test.desc @@ -1,4 +1,4 @@ -CORE paths-lifo-expected-failure +CORE paths-lifo-expected-failure new-smt-backend test.c --show-vcc --unwind 10 ^\{1\} main::argc!0@1#1 = 1$ diff --git a/regression/cbmc/residual-guards-1/test_execution.desc b/regression/cbmc/residual-guards-1/test_execution.desc index e73e7239f23..06e9033f4ee 100644 --- a/regression/cbmc/residual-guards-1/test_execution.desc +++ b/regression/cbmc/residual-guards-1/test_execution.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --unwind 10 ^\[main\.assertion\.[0-9]+\] line [0-9]+ assertion argc == 1: FAILURE$ diff --git a/regression/cbmc/residual-guards-2/test.desc b/regression/cbmc/residual-guards-2/test.desc index 0c2247e36d0..25b792cd968 100644 --- a/regression/cbmc/residual-guards-2/test.desc +++ b/regression/cbmc/residual-guards-2/test.desc @@ -1,4 +1,4 @@ -CORE paths-lifo-expected-failure +CORE paths-lifo-expected-failure new-smt-backend test.c --show-vcc --unwind 10 ^\{1\} main::argc!0@1#1 = 1$ diff --git a/regression/cbmc/residual-guards-2/test_execution.desc b/regression/cbmc/residual-guards-2/test_execution.desc index e73e7239f23..06e9033f4ee 100644 --- a/regression/cbmc/residual-guards-2/test_execution.desc +++ b/regression/cbmc/residual-guards-2/test_execution.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --unwind 10 ^\[main\.assertion\.[0-9]+\] line [0-9]+ assertion argc == 1: FAILURE$ diff --git a/regression/cbmc/residual-guards-3/test.desc b/regression/cbmc/residual-guards-3/test.desc index 21c34f474b0..fe51f9dbf1c 100644 --- a/regression/cbmc/residual-guards-3/test.desc +++ b/regression/cbmc/residual-guards-3/test.desc @@ -1,4 +1,4 @@ -CORE paths-lifo-expected-failure +CORE paths-lifo-expected-failure new-smt-backend test.c --show-vcc --depth 1000 ^\{1\} main::argc!0@1#1 = 1$ diff --git a/regression/cbmc/residual-guards-3/test_execution.desc b/regression/cbmc/residual-guards-3/test_execution.desc index d196319c904..98e216323af 100644 --- a/regression/cbmc/residual-guards-3/test_execution.desc +++ b/regression/cbmc/residual-guards-3/test_execution.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --depth 1000 ^\[main\.assertion\.[0-9]+\] line [0-9]+ assertion argc == 1: FAILURE$ diff --git a/regression/cbmc/residual-guards-4/test.desc b/regression/cbmc/residual-guards-4/test.desc index 7a51b34f874..397f542ae5d 100644 --- a/regression/cbmc/residual-guards-4/test.desc +++ b/regression/cbmc/residual-guards-4/test.desc @@ -1,4 +1,4 @@ -CORE paths-lifo-expected-failure +CORE paths-lifo-expected-failure new-smt-backend test.c --show-vcc ^\{1\} main::argc!0@1#1 = 1$ diff --git a/regression/cbmc/residual-guards-4/test_execution.desc b/regression/cbmc/residual-guards-4/test_execution.desc index 1ab6c2e23da..b288521e470 100644 --- a/regression/cbmc/residual-guards-4/test_execution.desc +++ b/regression/cbmc/residual-guards-4/test_execution.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^\[main\.assertion\.[0-9]+\] line [0-9]+ assertion argc == 1: FAILURE$ diff --git a/regression/cbmc/return2/test.desc b/regression/cbmc/return2/test.desc index b655b34a10f..1801a57c61d 100644 --- a/regression/cbmc/return2/test.desc +++ b/regression/cbmc/return2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/return3/full-slice.desc b/regression/cbmc/return3/full-slice.desc index 3793f7374e1..fef2038f244 100644 --- a/regression/cbmc/return3/full-slice.desc +++ b/regression/cbmc/return3/full-slice.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --full-slice ^EXIT=0$ diff --git a/regression/cbmc/return6/test.desc b/regression/cbmc/return6/test.desc index bf09360fa4c..d2175a98e32 100644 --- a/regression/cbmc/return6/test.desc +++ b/regression/cbmc/return6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c f_def.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/return7/test.desc b/regression/cbmc/return7/test.desc index 1d3f29ded69..88fdd20c5c7 100644 --- a/regression/cbmc/return7/test.desc +++ b/regression/cbmc/return7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^VERIFICATION FAILED$ diff --git a/regression/cbmc/return8/test.desc b/regression/cbmc/return8/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/return8/test.desc +++ b/regression/cbmc/return8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/return9/test.desc b/regression/cbmc/return9/test.desc index e913b101242..5ca4807ec69 100644 --- a/regression/cbmc/return9/test.desc +++ b/regression/cbmc/return9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend tcas_v23_523.c --bounds-check ^EXIT=10$ diff --git a/regression/cbmc/runtime-profiling/test.desc b/regression/cbmc/runtime-profiling/test.desc index a7d3a1198a1..ed871184560 100644 --- a/regression/cbmc/runtime-profiling/test.desc +++ b/regression/cbmc/runtime-profiling/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/saturating_arithmetric/output-formula.desc b/regression/cbmc/saturating_arithmetric/output-formula.desc index 11d26aada17..41a99e2a0d2 100644 --- a/regression/cbmc/saturating_arithmetric/output-formula.desc +++ b/regression/cbmc/saturating_arithmetric/output-formula.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --program-only ASSERT\(__CPROVER_saturating_minus\(.*\) diff --git a/regression/cbmc/saturating_arithmetric/output-goto.desc b/regression/cbmc/saturating_arithmetric/output-goto.desc index fc144ed0a24..6808b36fe88 100644 --- a/regression/cbmc/saturating_arithmetric/output-goto.desc +++ b/regression/cbmc/saturating_arithmetric/output-goto.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-goto-functions ASSERT saturating-\(.*\) diff --git a/regression/cbmc/saturating_arithmetric/typeconflict.desc b/regression/cbmc/saturating_arithmetric/typeconflict.desc index 9b00049f109..5a78973bce6 100644 --- a/regression/cbmc/saturating_arithmetric/typeconflict.desc +++ b/regression/cbmc/saturating_arithmetric/typeconflict.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend typeconflict.c file typeconflict.c line 3 function main: error: __CPROVER_saturating_minus takes exactly two arguments, but 1 were provided ^EXIT=6$ diff --git a/regression/cbmc/self_loops_to_assumptions1/default.desc b/regression/cbmc/self_loops_to_assumptions1/default.desc index 5cec41df787..e616b8295e7 100644 --- a/regression/cbmc/self_loops_to_assumptions1/default.desc +++ b/regression/cbmc/self_loops_to_assumptions1/default.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 1 --unwinding-assertions ^replacing self-loop at file main.c line 3 function main by assume\(FALSE\)$ diff --git a/regression/cbmc/self_loops_to_assumptions1/no-assume.desc b/regression/cbmc/self_loops_to_assumptions1/no-assume.desc index b75ec34a1bc..10a258c84bc 100644 --- a/regression/cbmc/self_loops_to_assumptions1/no-assume.desc +++ b/regression/cbmc/self_loops_to_assumptions1/no-assume.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 1 --unwinding-assertions --no-self-loops-to-assumptions ^EXIT=10$ diff --git a/regression/cbmc/short_circuit_implies/false_implies_failure_side_effect.desc b/regression/cbmc/short_circuit_implies/false_implies_failure_side_effect.desc index ab4313d22ad..31a695307d1 100644 --- a/regression/cbmc/short_circuit_implies/false_implies_failure_side_effect.desc +++ b/regression/cbmc/short_circuit_implies/false_implies_failure_side_effect.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend false_implies_failure_side_effect.c ^EXIT=0$ diff --git a/regression/cbmc/short_circuit_implies/short-circuit-memory-checks.desc b/regression/cbmc/short_circuit_implies/short-circuit-memory-checks.desc index 1b37eefb313..8c4dab2fd2f 100644 --- a/regression/cbmc/short_circuit_implies/short-circuit-memory-checks.desc +++ b/regression/cbmc/short_circuit_implies/short-circuit-memory-checks.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend short-circuit-memory-checks.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/short_circuit_implies/true_implies_failure_side_effect.desc b/regression/cbmc/short_circuit_implies/true_implies_failure_side_effect.desc index e53d14615e4..157aa113746 100644 --- a/regression/cbmc/short_circuit_implies/true_implies_failure_side_effect.desc +++ b/regression/cbmc/short_circuit_implies/true_implies_failure_side_effect.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend true_implies_failure_side_effect.c ^EXIT=10$ diff --git a/regression/cbmc/show-vcc/test.desc b/regression/cbmc/show-vcc/test.desc index bb01b2fa853..1582778b7ae 100644 --- a/regression/cbmc/show-vcc/test.desc +++ b/regression/cbmc/show-vcc/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-vcc ^EXIT=0$ diff --git a/regression/cbmc/show_properties1/test.desc b/regression/cbmc/show_properties1/test.desc index 96b4816a1fb..0876cac2923 100644 --- a/regression/cbmc/show_properties1/test.desc +++ b/regression/cbmc/show_properties1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --show-properties ^EXIT=0$ diff --git a/regression/cbmc/simplify-full-test/test.desc b/regression/cbmc/simplify-full-test/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/simplify-full-test/test.desc +++ b/regression/cbmc/simplify-full-test/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/simplify-function-call-array-element-pointer/test.desc b/regression/cbmc/simplify-function-call-array-element-pointer/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/simplify-function-call-array-element-pointer/test.desc +++ b/regression/cbmc/simplify-function-call-array-element-pointer/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/simplify-function-call-array-pointer/test.desc b/regression/cbmc/simplify-function-call-array-pointer/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/simplify-function-call-array-pointer/test.desc +++ b/regression/cbmc/simplify-function-call-array-pointer/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/simplify-function-call-pointer-access/test.desc b/regression/cbmc/simplify-function-call-pointer-access/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/simplify-function-call-pointer-access/test.desc +++ b/regression/cbmc/simplify-function-call-pointer-access/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/simplify-global-array-access/test.desc b/regression/cbmc/simplify-global-array-access/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/simplify-global-array-access/test.desc +++ b/regression/cbmc/simplify-global-array-access/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/simplify-local-array-access/test.desc b/regression/cbmc/simplify-local-array-access/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/simplify-local-array-access/test.desc +++ b/regression/cbmc/simplify-local-array-access/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/simplify-pointer-access/test.desc b/regression/cbmc/simplify-pointer-access/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/simplify-pointer-access/test.desc +++ b/regression/cbmc/simplify-pointer-access/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/simplify-union/test.desc b/regression/cbmc/simplify-union/test.desc index de8c67be832..b34ddf1241d 100644 --- a/regression/cbmc/simplify-union/test.desc +++ b/regression/cbmc/simplify-union/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^Generated 1 VCC\(s\), 0 remaining after simplification$ diff --git a/regression/cbmc/stack-trace/test.desc b/regression/cbmc/stack-trace/test.desc index eceab4a2d07..70f6deaf734 100644 --- a/regression/cbmc/stack-trace/test.desc +++ b/regression/cbmc/stack-trace/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --stack-trace activate-multi-line-match diff --git a/regression/cbmc/string_assignment1/test.desc b/regression/cbmc/string_assignment1/test.desc index 44427b32e3b..9f085793f76 100644 --- a/regression/cbmc/string_assignment1/test.desc +++ b/regression/cbmc/string_assignment1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/switch1/test.desc b/regression/cbmc/switch1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/switch1/test.desc +++ b/regression/cbmc/switch1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/switch2/test.desc b/regression/cbmc/switch2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/switch2/test.desc +++ b/regression/cbmc/switch2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/switch3/test.desc b/regression/cbmc/switch3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/switch3/test.desc +++ b/regression/cbmc/switch3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/switch4/test.desc b/regression/cbmc/switch4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/switch4/test.desc +++ b/regression/cbmc/switch4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/switch5/test.desc b/regression/cbmc/switch5/test.desc index 33900ad2b78..82568cfc082 100644 --- a/regression/cbmc/switch5/test.desc +++ b/regression/cbmc/switch5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/switch6/test.desc b/regression/cbmc/switch6/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/switch6/test.desc +++ b/regression/cbmc/switch6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/switch7/test.desc b/regression/cbmc/switch7/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/switch7/test.desc +++ b/regression/cbmc/switch7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/switch8/program-only.desc b/regression/cbmc/switch8/program-only.desc index 15885c2d7e5..03bf14bf3e3 100644 --- a/regression/cbmc/switch8/program-only.desc +++ b/regression/cbmc/switch8/program-only.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --program-only ^EXIT=0$ diff --git a/regression/cbmc/switch8/test.desc b/regression/cbmc/switch8/test.desc index 62e8b9730ae..5b7760a38df 100644 --- a/regression/cbmc/switch8/test.desc +++ b/regression/cbmc/switch8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/switch9/test.desc b/regression/cbmc/switch9/test.desc index 8438cf07aac..2aa63fe318d 100644 --- a/regression/cbmc/switch9/test.desc +++ b/regression/cbmc/switch9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --malloc-may-fail --malloc-fail-null activate-multi-line-match diff --git a/regression/cbmc/sync_X_and_fetch-1/pointer.desc b/regression/cbmc/sync_X_and_fetch-1/pointer.desc index 47e35dd8f38..111eb593a8d 100644 --- a/regression/cbmc/sync_X_and_fetch-1/pointer.desc +++ b/regression/cbmc/sync_X_and_fetch-1/pointer.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend pointer.c ^EXIT=6$ diff --git a/regression/cbmc/sync_X_and_fetch-1/test.desc b/regression/cbmc/sync_X_and_fetch-1/test.desc index 27a28993ba5..6032b0b3c6a 100644 --- a/regression/cbmc/sync_X_and_fetch-1/test.desc +++ b/regression/cbmc/sync_X_and_fetch-1/test.desc @@ -1,4 +1,4 @@ -CORE gcc-only +CORE gcc-only new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/sync_X_and_fetch-1/two.desc b/regression/cbmc/sync_X_and_fetch-1/two.desc index f30efdf57b3..8f2f1ecae22 100644 --- a/regression/cbmc/sync_X_and_fetch-1/two.desc +++ b/regression/cbmc/sync_X_and_fetch-1/two.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend two.c ^EXIT=6$ diff --git a/regression/cbmc/sync_bool_compare-1/pointer.desc b/regression/cbmc/sync_bool_compare-1/pointer.desc index 2711f883b23..13e4c643dd0 100644 --- a/regression/cbmc/sync_bool_compare-1/pointer.desc +++ b/regression/cbmc/sync_bool_compare-1/pointer.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend pointer.c ^EXIT=6$ diff --git a/regression/cbmc/sync_bool_compare-1/test.desc b/regression/cbmc/sync_bool_compare-1/test.desc index 27a28993ba5..6032b0b3c6a 100644 --- a/regression/cbmc/sync_bool_compare-1/test.desc +++ b/regression/cbmc/sync_bool_compare-1/test.desc @@ -1,4 +1,4 @@ -CORE gcc-only +CORE gcc-only new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/sync_bool_compare-1/three.desc b/regression/cbmc/sync_bool_compare-1/three.desc index a6fdead1415..609dba47d70 100644 --- a/regression/cbmc/sync_bool_compare-1/three.desc +++ b/regression/cbmc/sync_bool_compare-1/three.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend three.c ^EXIT=6$ diff --git a/regression/cbmc/sync_fetch_and_X-1/pointer.desc b/regression/cbmc/sync_fetch_and_X-1/pointer.desc index 47e35dd8f38..111eb593a8d 100644 --- a/regression/cbmc/sync_fetch_and_X-1/pointer.desc +++ b/regression/cbmc/sync_fetch_and_X-1/pointer.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend pointer.c ^EXIT=6$ diff --git a/regression/cbmc/sync_fetch_and_X-1/test.desc b/regression/cbmc/sync_fetch_and_X-1/test.desc index 27a28993ba5..6032b0b3c6a 100644 --- a/regression/cbmc/sync_fetch_and_X-1/test.desc +++ b/regression/cbmc/sync_fetch_and_X-1/test.desc @@ -1,4 +1,4 @@ -CORE gcc-only +CORE gcc-only new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/sync_fetch_and_X-1/two.desc b/regression/cbmc/sync_fetch_and_X-1/two.desc index f30efdf57b3..8f2f1ecae22 100644 --- a/regression/cbmc/sync_fetch_and_X-1/two.desc +++ b/regression/cbmc/sync_fetch_and_X-1/two.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend two.c ^EXIT=6$ diff --git a/regression/cbmc/sync_lock_release-1/symbol_per_type.desc b/regression/cbmc/sync_lock_release-1/symbol_per_type.desc index 358d0a47eeb..90da66a65f3 100644 --- a/regression/cbmc/sync_lock_release-1/symbol_per_type.desc +++ b/regression/cbmc/sync_lock_release-1/symbol_per_type.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-goto-functions ^EXIT=0$ diff --git a/regression/cbmc/sync_lock_release-1/test.desc b/regression/cbmc/sync_lock_release-1/test.desc index c985459baff..de2901b284e 100644 --- a/regression/cbmc/sync_lock_release-1/test.desc +++ b/regression/cbmc/sync_lock_release-1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/sync_val_compare-1/pointer.desc b/regression/cbmc/sync_val_compare-1/pointer.desc index 98114eb2101..9c10fef964c 100644 --- a/regression/cbmc/sync_val_compare-1/pointer.desc +++ b/regression/cbmc/sync_val_compare-1/pointer.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend pointer.c ^EXIT=6$ diff --git a/regression/cbmc/sync_val_compare-1/test.desc b/regression/cbmc/sync_val_compare-1/test.desc index 27a28993ba5..6032b0b3c6a 100644 --- a/regression/cbmc/sync_val_compare-1/test.desc +++ b/regression/cbmc/sync_val_compare-1/test.desc @@ -1,4 +1,4 @@ -CORE gcc-only +CORE gcc-only new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/sync_val_compare-1/three.desc b/regression/cbmc/sync_val_compare-1/three.desc index a6fdead1415..609dba47d70 100644 --- a/regression/cbmc/sync_val_compare-1/three.desc +++ b/regression/cbmc/sync_val_compare-1/three.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend three.c ^EXIT=6$ diff --git a/regression/cbmc/trace_options_json_extended/extended.desc b/regression/cbmc/trace_options_json_extended/extended.desc index beafa0649de..b36daf7cad3 100644 --- a/regression/cbmc/trace_options_json_extended/extended.desc +++ b/regression/cbmc/trace_options_json_extended/extended.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --trace --json-ui --trace-json-extended ^EXIT=10$ diff --git a/regression/cbmc/trace_options_json_extended/non-extended.desc b/regression/cbmc/trace_options_json_extended/non-extended.desc index 5d03ca97bc1..1821b9f454c 100644 --- a/regression/cbmc/trace_options_json_extended/non-extended.desc +++ b/regression/cbmc/trace_options_json_extended/non-extended.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c --trace --json-ui ^EXIT=10$ diff --git a/regression/cbmc/ts18661_typedefs/test.desc b/regression/cbmc/ts18661_typedefs/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/ts18661_typedefs/test.desc +++ b/regression/cbmc/ts18661_typedefs/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/typedef-anon-struct1/test.desc b/regression/cbmc/typedef-anon-struct1/test.desc index 4129f0344f1..306e7e8557e 100644 --- a/regression/cbmc/typedef-anon-struct1/test.desc +++ b/regression/cbmc/typedef-anon-struct1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-anon-struct2/test.desc b/regression/cbmc/typedef-anon-struct2/test.desc index 86e220fafcd..8cd4357382a 100644 --- a/regression/cbmc/typedef-anon-struct2/test.desc +++ b/regression/cbmc/typedef-anon-struct2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-anon-union1/test.desc b/regression/cbmc/typedef-anon-union1/test.desc index 190b89262bb..c3c177c5907 100644 --- a/regression/cbmc/typedef-anon-union1/test.desc +++ b/regression/cbmc/typedef-anon-union1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-anon-union2/test.desc b/regression/cbmc/typedef-anon-union2/test.desc index 3d5ab817226..3e15c5eb4ca 100644 --- a/regression/cbmc/typedef-anon-union2/test.desc +++ b/regression/cbmc/typedef-anon-union2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-const-struct1/test.desc b/regression/cbmc/typedef-const-struct1/test.desc index 4ed2abc2821..d426b8a5ee8 100644 --- a/regression/cbmc/typedef-const-struct1/test.desc +++ b/regression/cbmc/typedef-const-struct1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-const-type1/test.desc b/regression/cbmc/typedef-const-type1/test.desc index 9dfc4035aaa..8a323995246 100644 --- a/regression/cbmc/typedef-const-type1/test.desc +++ b/regression/cbmc/typedef-const-type1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-const-union1/test.desc b/regression/cbmc/typedef-const-union1/test.desc index 96b3a3107e4..f777829bf69 100644 --- a/regression/cbmc/typedef-const-union1/test.desc +++ b/regression/cbmc/typedef-const-union1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-param-anon-struct1/test.desc b/regression/cbmc/typedef-param-anon-struct1/test.desc index aff1030eac9..d6a87fb0c25 100644 --- a/regression/cbmc/typedef-param-anon-struct1/test.desc +++ b/regression/cbmc/typedef-param-anon-struct1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-param-anon-union1/test.desc b/regression/cbmc/typedef-param-anon-union1/test.desc index be6ef9f8db3..e3b7be24f1f 100644 --- a/regression/cbmc/typedef-param-anon-union1/test.desc +++ b/regression/cbmc/typedef-param-anon-union1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-param-struct1/test.desc b/regression/cbmc/typedef-param-struct1/test.desc index 763e2311b54..c6ef91ec53f 100644 --- a/regression/cbmc/typedef-param-struct1/test.desc +++ b/regression/cbmc/typedef-param-struct1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-param-type1/test.desc b/regression/cbmc/typedef-param-type1/test.desc index af9864cde3a..af3a1dcb6ad 100644 --- a/regression/cbmc/typedef-param-type1/test.desc +++ b/regression/cbmc/typedef-param-type1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-param-type2/test.desc b/regression/cbmc/typedef-param-type2/test.desc index f6f46e30ec8..3e3d2f6d27e 100644 --- a/regression/cbmc/typedef-param-type2/test.desc +++ b/regression/cbmc/typedef-param-type2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-param-type3/test.desc b/regression/cbmc/typedef-param-type3/test.desc index 9713651869a..1baba2e69ca 100644 --- a/regression/cbmc/typedef-param-type3/test.desc +++ b/regression/cbmc/typedef-param-type3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-param-union1/test.desc b/regression/cbmc/typedef-param-union1/test.desc index b97bca4db0c..411b26e9f85 100644 --- a/regression/cbmc/typedef-param-union1/test.desc +++ b/regression/cbmc/typedef-param-union1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-struct1/test.desc b/regression/cbmc/typedef-struct1/test.desc index a2782102e8f..ae67568c86f 100644 --- a/regression/cbmc/typedef-struct1/test.desc +++ b/regression/cbmc/typedef-struct1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-struct2/test.desc b/regression/cbmc/typedef-struct2/test.desc index a2782102e8f..ae67568c86f 100644 --- a/regression/cbmc/typedef-struct2/test.desc +++ b/regression/cbmc/typedef-struct2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-type1/test.desc b/regression/cbmc/typedef-type1/test.desc index 96795704d3b..de9d2d0cc7c 100644 --- a/regression/cbmc/typedef-type1/test.desc +++ b/regression/cbmc/typedef-type1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-type2/test.desc b/regression/cbmc/typedef-type2/test.desc index c1dd8aa6755..5cb220ee80e 100644 --- a/regression/cbmc/typedef-type2/test.desc +++ b/regression/cbmc/typedef-type2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-type3/test.desc b/regression/cbmc/typedef-type3/test.desc index 330e4d4ca1a..92f6cf637bb 100644 --- a/regression/cbmc/typedef-type3/test.desc +++ b/regression/cbmc/typedef-type3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-type4/test.desc b/regression/cbmc/typedef-type4/test.desc index a958f3923a6..66522a6ec9f 100644 --- a/regression/cbmc/typedef-type4/test.desc +++ b/regression/cbmc/typedef-type4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-union1/test.desc b/regression/cbmc/typedef-union1/test.desc index 6c392e390d6..f4e64f14254 100644 --- a/regression/cbmc/typedef-union1/test.desc +++ b/regression/cbmc/typedef-union1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/typedef-union2/test.desc b/regression/cbmc/typedef-union2/test.desc index 99fe01a98ea..a21267cc609 100644 --- a/regression/cbmc/typedef-union2/test.desc +++ b/regression/cbmc/typedef-union2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-symbol-table --function fun // Enable multi-line checking diff --git a/regression/cbmc/uncaught_exceptions_analysis1/test.desc b/regression/cbmc/uncaught_exceptions_analysis1/test.desc index f8823e7d524..962782268ea 100644 --- a/regression/cbmc/uncaught_exceptions_analysis1/test.desc +++ b/regression/cbmc/uncaught_exceptions_analysis1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/uniform_array1/test.desc b/regression/cbmc/uniform_array1/test.desc index 1b1641fd47a..6c8aae65d3e 100644 --- a/regression/cbmc/uniform_array1/test.desc +++ b/regression/cbmc/uniform_array1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/unknown-argument-suggestion/test.desc b/regression/cbmc/unknown-argument-suggestion/test.desc index bf1204f5842..d9341e021b1 100644 --- a/regression/cbmc/unknown-argument-suggestion/test.desc +++ b/regression/cbmc/unknown-argument-suggestion/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend dummy.c --traec did you mean --trace diff --git a/regression/cbmc/unreachable-goto1/test-vccs.desc b/regression/cbmc/unreachable-goto1/test-vccs.desc index 9091c97751a..7abdda07dab 100644 --- a/regression/cbmc/unreachable-goto1/test-vccs.desc +++ b/regression/cbmc/unreachable-goto1/test-vccs.desc @@ -1,4 +1,4 @@ -CORE paths-lifo-expected-failure +CORE paths-lifo-expected-failure new-smt-backend test.c --show-vcc ^Generated 1 VCC\(s\), 1 remaining after simplification$ diff --git a/regression/cbmc/unreachable-goto1/test.desc b/regression/cbmc/unreachable-goto1/test.desc index d9ac83f95d4..3e9d22b2a2f 100644 --- a/regression/cbmc/unreachable-goto1/test.desc +++ b/regression/cbmc/unreachable-goto1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^VERIFICATION FAILED$ diff --git a/regression/cbmc/unreachable-goto2/test-vccs.desc b/regression/cbmc/unreachable-goto2/test-vccs.desc index d18e596fd5f..36740a80afb 100644 --- a/regression/cbmc/unreachable-goto2/test-vccs.desc +++ b/regression/cbmc/unreachable-goto2/test-vccs.desc @@ -1,4 +1,4 @@ -CORE paths-lifo-expected-failure +CORE paths-lifo-expected-failure new-smt-backend test.c --show-vcc ^Generated 1 VCC\(s\), 1 remaining after simplification$ diff --git a/regression/cbmc/unreachable-goto2/test.desc b/regression/cbmc/unreachable-goto2/test.desc index 330528f4237..1d7e3e4313f 100644 --- a/regression/cbmc/unreachable-goto2/test.desc +++ b/regression/cbmc/unreachable-goto2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^VERIFICATION FAILED$ diff --git a/regression/cbmc/unreachable-goto3/test-vccs.desc b/regression/cbmc/unreachable-goto3/test-vccs.desc index 54f5a88444d..c95deabe9a8 100644 --- a/regression/cbmc/unreachable-goto3/test-vccs.desc +++ b/regression/cbmc/unreachable-goto3/test-vccs.desc @@ -1,4 +1,4 @@ -CORE paths-lifo-expected-failure +CORE paths-lifo-expected-failure new-smt-backend test.c --show-vcc ^Generated 1 VCC\(s\), 1 remaining after simplification$ diff --git a/regression/cbmc/unreachable-goto3/test.desc b/regression/cbmc/unreachable-goto3/test.desc index ee2169c0cb5..4f00aa41e70 100644 --- a/regression/cbmc/unreachable-goto3/test.desc +++ b/regression/cbmc/unreachable-goto3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^VERIFICATION FAILED$ diff --git a/regression/cbmc/unreachable-goto4/test-vccs.desc b/regression/cbmc/unreachable-goto4/test-vccs.desc index 434b0b05cd0..8e7d45cddd8 100644 --- a/regression/cbmc/unreachable-goto4/test-vccs.desc +++ b/regression/cbmc/unreachable-goto4/test-vccs.desc @@ -1,4 +1,4 @@ -CORE paths-lifo-expected-failure +CORE paths-lifo-expected-failure new-smt-backend test.c --show-vcc ^Generated 1 VCC\(s\), 1 remaining after simplification$ diff --git a/regression/cbmc/unreachable-goto4/test.desc b/regression/cbmc/unreachable-goto4/test.desc index ee2169c0cb5..4f00aa41e70 100644 --- a/regression/cbmc/unreachable-goto4/test.desc +++ b/regression/cbmc/unreachable-goto4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^VERIFICATION FAILED$ diff --git a/regression/cbmc/unreachable-goto5/test-vccs.desc b/regression/cbmc/unreachable-goto5/test-vccs.desc index dc7ef0de936..ad6b25958b9 100644 --- a/regression/cbmc/unreachable-goto5/test-vccs.desc +++ b/regression/cbmc/unreachable-goto5/test-vccs.desc @@ -1,4 +1,4 @@ -CORE paths-lifo-expected-failure +CORE paths-lifo-expected-failure new-smt-backend test.c --show-vcc ^Generated 1 VCC\(s\), 1 remaining after simplification$ diff --git a/regression/cbmc/unreachable-goto5/test.desc b/regression/cbmc/unreachable-goto5/test.desc index aca472865e0..d494e422509 100644 --- a/regression/cbmc/unreachable-goto5/test.desc +++ b/regression/cbmc/unreachable-goto5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^VERIFICATION FAILED$ diff --git a/regression/cbmc/unreachable-goto6/test-vccs.desc b/regression/cbmc/unreachable-goto6/test-vccs.desc index dcfb2c2a5e3..f687a87af7f 100644 --- a/regression/cbmc/unreachable-goto6/test-vccs.desc +++ b/regression/cbmc/unreachable-goto6/test-vccs.desc @@ -1,4 +1,4 @@ -CORE paths-lifo-expected-failure +CORE paths-lifo-expected-failure new-smt-backend test.c --show-vcc ^Generated 1 VCC\(s\), 1 remaining after simplification$ diff --git a/regression/cbmc/unreachable-goto6/test.desc b/regression/cbmc/unreachable-goto6/test.desc index ead69482cbb..fe7c85aece9 100644 --- a/regression/cbmc/unreachable-goto6/test.desc +++ b/regression/cbmc/unreachable-goto6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend test.c ^VERIFICATION FAILED$ diff --git a/regression/cbmc/unsigned1/test.desc b/regression/cbmc/unsigned1/test.desc index a1e381cbf60..08a06bb8651 100644 --- a/regression/cbmc/unsigned1/test.desc +++ b/regression/cbmc/unsigned1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --show-goto-functions ^EXIT=0$ diff --git a/regression/cbmc/unsigned___int128/test.desc b/regression/cbmc/unsigned___int128/test.desc index 67b0294bc90..ab1d61e16c9 100644 --- a/regression/cbmc/unsigned___int128/test.desc +++ b/regression/cbmc/unsigned___int128/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unsigned-overflow-check --signed-overflow-check --function reduce ^EXIT=0$ diff --git a/regression/cbmc/unsigned_char1/test.desc b/regression/cbmc/unsigned_char1/test.desc index 0f995fec257..26850765a77 100644 --- a/regression/cbmc/unsigned_char1/test.desc +++ b/regression/cbmc/unsigned_char1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unsigned-char ^EXIT=0$ diff --git a/regression/cbmc/unwind_counters1/test.desc b/regression/cbmc/unwind_counters1/test.desc index 46efb30683e..ca28d22716b 100644 --- a/regression/cbmc/unwind_counters1/test.desc +++ b/regression/cbmc/unwind_counters1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 11 --unwinding-assertions ^EXIT=0$ diff --git a/regression/cbmc/unwind_counters2/test.desc b/regression/cbmc/unwind_counters2/test.desc index 70b64ab793d..9202d246798 100644 --- a/regression/cbmc/unwind_counters2/test.desc +++ b/regression/cbmc/unwind_counters2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 3 --unwinding-assertions ^EXIT=10$ diff --git a/regression/cbmc/unwind_counters3/test.desc b/regression/cbmc/unwind_counters3/test.desc index 70b64ab793d..9202d246798 100644 --- a/regression/cbmc/unwind_counters3/test.desc +++ b/regression/cbmc/unwind_counters3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 3 --unwinding-assertions ^EXIT=10$ diff --git a/regression/cbmc/unwind_counters4/test.desc b/regression/cbmc/unwind_counters4/test.desc index f60b11caa10..6d425aa2dbe 100644 --- a/regression/cbmc/unwind_counters4/test.desc +++ b/regression/cbmc/unwind_counters4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 2 ^EXIT=10$ diff --git a/regression/cbmc/unwinding_assertions1/test.desc b/regression/cbmc/unwinding_assertions1/test.desc index 33d9d83a074..fb604d6187b 100644 --- a/regression/cbmc/unwinding_assertions1/test.desc +++ b/regression/cbmc/unwinding_assertions1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 3 --unwinding-assertions ^EXIT=10$ diff --git a/regression/cbmc/unwindset1/label.desc b/regression/cbmc/unwindset1/label.desc index 6515b21f9a7..c97aae6bf54 100644 --- a/regression/cbmc/unwindset1/label.desc +++ b/regression/cbmc/unwindset1/label.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwindset main.for_loop:2,main.1:6 ^VERIFICATION FAILED$ diff --git a/regression/cbmc/unwindset1/test.desc b/regression/cbmc/unwindset1/test.desc index b96eb4cdcc5..6f6048ff145 100644 --- a/regression/cbmc/unwindset1/test.desc +++ b/regression/cbmc/unwindset1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwindset main.0:2,main.2:2 ^loop identifier main.2 provided with unwindset does not match any loop$ diff --git a/regression/cbmc/unwindset2/test.desc b/regression/cbmc/unwindset2/test.desc index e870637450c..375bb3b4de3 100644 --- a/regression/cbmc/unwindset2/test.desc +++ b/regression/cbmc/unwindset2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwindset main.for_loop:2 --unwinding-assertions ^loop identifier main.for_loop provided with unwindset is ambiguous$ diff --git a/regression/cbmc/va_list1/test.desc b/regression/cbmc/va_list1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/va_list1/test.desc +++ b/regression/cbmc/va_list1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/va_list2/test.desc b/regression/cbmc/va_list2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/va_list2/test.desc +++ b/regression/cbmc/va_list2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/va_list4/test.desc b/regression/cbmc/va_list4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/va_list4/test.desc +++ b/regression/cbmc/va_list4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/variable-access-to-constant-array/test.desc b/regression/cbmc/variable-access-to-constant-array/test.desc index 212fd7b6674..98870d013c2 100644 --- a/regression/cbmc/variable-access-to-constant-array/test.desc +++ b/regression/cbmc/variable-access-to-constant-array/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/verifier_assume_one/test.desc b/regression/cbmc/verifier_assume_one/test.desc index bca33a5dd6d..9f1aa2be3b0 100644 --- a/regression/cbmc/verifier_assume_one/test.desc +++ b/regression/cbmc/verifier_assume_one/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=6$ diff --git a/regression/cbmc/verifier_error_lhs/test.desc b/regression/cbmc/verifier_error_lhs/test.desc index 694fa96c475..92104b36f3e 100644 --- a/regression/cbmc/verifier_error_lhs/test.desc +++ b/regression/cbmc/verifier_error_lhs/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c function .* is not declared diff --git a/regression/cbmc/verifier_error_zero/test.desc b/regression/cbmc/verifier_error_zero/test.desc index f6beb5f5ef4..d6e02f70ba8 100644 --- a/regression/cbmc/verifier_error_zero/test.desc +++ b/regression/cbmc/verifier_error_zero/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c function .* is not declared diff --git a/regression/cbmc/vla1/program-only.desc b/regression/cbmc/vla1/program-only.desc index 35f671bf4a5..7c0b75016f3 100644 --- a/regression/cbmc/vla1/program-only.desc +++ b/regression/cbmc/vla1/program-only.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --program-only ^EXIT=0$ diff --git a/regression/cbmc/void_ifthenelse/test.desc b/regression/cbmc/void_ifthenelse/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/void_ifthenelse/test.desc +++ b/regression/cbmc/void_ifthenelse/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/while1/test.desc b/regression/cbmc/while1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/while1/test.desc +++ b/regression/cbmc/while1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/while2/requires-transform.desc b/regression/cbmc/while2/requires-transform.desc index 8aa536c7210..cee57365fb7 100644 --- a/regression/cbmc/while2/requires-transform.desc +++ b/regression/cbmc/while2/requires-transform.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend requires-transform.c ^EXIT=0$ diff --git a/regression/cbmc/while2/test.desc b/regression/cbmc/while2/test.desc index aa4d4a6f507..d42c6416fa2 100644 --- a/regression/cbmc/while2/test.desc +++ b/regression/cbmc/while2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/xml-escaping/debug_output.desc b/regression/cbmc/xml-escaping/debug_output.desc index af4f42c9fa8..92f36790f10 100644 --- a/regression/cbmc/xml-escaping/debug_output.desc +++ b/regression/cbmc/xml-escaping/debug_output.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --verbosity 10 --xml-ui ^EXIT=10$ diff --git a/regression/cbmc/xml-interface1/test.desc b/regression/cbmc/xml-interface1/test.desc index 7f33c189af2..1a25e12ba3c 100644 --- a/regression/cbmc/xml-interface1/test.desc +++ b/regression/cbmc/xml-interface1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend --xml-interface < test.xml ^EXIT=10$ diff --git a/regression/cbmc/xml-interface1/test_wrong_flag.desc b/regression/cbmc/xml-interface1/test_wrong_flag.desc index 25f277064c9..e665facbd22 100644 --- a/regression/cbmc/xml-interface1/test_wrong_flag.desc +++ b/regression/cbmc/xml-interface1/test_wrong_flag.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend --xml-interface < test_wrong_flag.xml ^EXIT=6$ diff --git a/regression/cbmc/xml-interface1/test_wrong_option.desc b/regression/cbmc/xml-interface1/test_wrong_option.desc index 77dd991ba5f..08637d3b933 100644 --- a/regression/cbmc/xml-interface1/test_wrong_option.desc +++ b/regression/cbmc/xml-interface1/test_wrong_option.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend --xml-interface < test_wrong_option.xml ^EXIT=6$ diff --git a/regression/cbmc/z3/invalid.desc b/regression/cbmc/z3/invalid.desc index a2f83971f8f..90358d14954 100644 --- a/regression/cbmc/z3/invalid.desc +++ b/regression/cbmc/z3/invalid.desc @@ -1,4 +1,4 @@ -CORE smt-backend +CORE smt-backend new-smt-backend invalid.c --trace --smt2 --z3 ^EXIT=10$ diff --git a/regression/cbmc/z3/valid.desc b/regression/cbmc/z3/valid.desc index ca634f915aa..5cbbb0c81c5 100644 --- a/regression/cbmc/z3/valid.desc +++ b/regression/cbmc/z3/valid.desc @@ -1,4 +1,4 @@ -CORE smt-backend +CORE smt-backend new-smt-backend valid.c --trace --smt2 --z3 ^EXIT=0$