diffblue · tautschnig · Dec 9, 2022 · Jan 20, 2022 · Jan 21, 2022 · Feb 28, 2019
diff --git a/regression/cbmc-concurrency/thread_chain_cbmc1/main.c b/regression/cbmc-concurrency/thread_chain_cbmc1/main.c
@@ -18,7 +18,7 @@
 typedef unsigned long thread_id_t;
 
 // Internal unbounded array indexed by local thread identifiers
-extern __CPROVER_bool __CPROVER_threads_exited[];
+__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
 
 // A thread_chain is like a chain of threads `f, g, ...` where `f`
 // must terminate before `g` can start to run, and so forth.

diff --git a/regression/cbmc-concurrency/thread_chain_cbmc2/main.c b/regression/cbmc-concurrency/thread_chain_cbmc2/main.c
@@ -18,7 +18,7 @@
 typedef unsigned long thread_id_t;
 
 // Internal unbounded array indexed by local thread identifiers
-extern __CPROVER_bool __CPROVER_threads_exited[];
+__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
 
 // A thread_chain is like a chain of threads `f, g, ...` where `f`
 // must terminate before `g` can start to run, and so forth.

diff --git a/regression/cbmc-library/__atomic_always_lock_free-01/main.c b/regression/cbmc-library/__atomic_always_lock_free-01/main.c
@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+_Bool __atomic_always_lock_free(__CPROVER_size_t, void *);
+#endif
+
 int main()
 {
   assert(__atomic_always_lock_free(sizeof(int), 0));

diff --git a/regression/cbmc-library/__atomic_clear-01/main.c b/regression/cbmc-library/__atomic_clear-01/main.c
@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+void __atomic_clear(_Bool *, int);
+#endif
+
 int main()
 {
   _Bool n;

diff --git a/regression/cbmc-library/__atomic_is_lock_free-01/main.c b/regression/cbmc-library/__atomic_is_lock_free-01/main.c
@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+_Bool __atomic_is_lock_free(__CPROVER_size_t, void *);
+#endif
+
 int main()
 {
   assert(__atomic_is_lock_free(sizeof(int), 0));

diff --git a/regression/cbmc-library/__atomic_signal_fence-01/main.c b/regression/cbmc-library/__atomic_signal_fence-01/main.c
@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+void __atomic_signal_fence(int);
+#endif
+
 int main()
 {
   __atomic_signal_fence(0);

diff --git a/regression/cbmc-library/__atomic_test_and_set-01/main.c b/regression/cbmc-library/__atomic_test_and_set-01/main.c
@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+_Bool __atomic_test_and_set(void *, int);
+#endif
+
 int main()
 {
   char c = 0;

diff --git a/regression/cbmc-library/__atomic_thread_fence-01/main.c b/regression/cbmc-library/__atomic_thread_fence-01/main.c
@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+void __atomic_thread_fence(int);
+#endif
+
 int main()
 {
   __atomic_thread_fence(0);

diff --git a/regression/cbmc-library/__errno_location-01/main.c b/regression/cbmc-library/__errno_location-01/main.c
@@ -1,9 +1,9 @@
 #include <assert.h>
 #include <errno.h>
 
-int main()
+int main(int arc, char *argv[])
 {
-  __errno_location();
-  assert(0);
+  // errno expands to use of __errno_location() with glibc
+  assert(errno == 0);
   return 0;
 }
diff --git a/regression/cbmc-library/__errno_location-01/test.desc b/regression/cbmc-library/__errno_location-01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

diff --git a/regression/cbmc-library/_longjmp-01/main.c b/regression/cbmc-library/_longjmp-01/main.c
@@ -1,5 +1,9 @@
 #include <setjmp.h>
 
+#ifndef __GNUC__
+#  define _longjmp(a, b) longjmp(a, b)
+#endif
+
 static jmp_buf env;
 
 int main()

diff --git a/regression/cbmc-library/_longjmp-01/test.desc b/regression/cbmc-library/_longjmp-01/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --pointer-check --bounds-check
-^\[_longjmp.assertion.1\] line 12 _longjmp requires instrumentation: FAILURE$
-^\[main.assertion.1\] line 8 unreachable: SUCCESS$
+^\[_?longjmp.assertion.1\] line 12 _?longjmp requires instrumentation: FAILURE$
+^\[main.assertion.1\] line 12 unreachable: SUCCESS$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

diff --git a/regression/cbmc-library/alloca-02/main.c b/regression/cbmc-library/alloca-02/main.c
@@ -4,9 +4,14 @@
 void *alloca(size_t alloca_size);
 #endif
 
+// intentionally type conflicting: the built-in library uses const void*; this
+// is to check that object type updates are performed
+extern const char *__CPROVER_alloca_object;
+
 int *foo()
 {
   int *foo_ptr = alloca(sizeof(int));
+  __CPROVER_assert(foo_ptr == __CPROVER_alloca_object, "may fail");
   return foo_ptr;
 }
 

diff --git a/regression/cbmc-library/alloca-02/test.desc b/regression/cbmc-library/alloca-02/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --pointer-check
 dereference failure: dead object in \*from_foo: FAILURE$
-^\*\* 1 of 6 failed
+^\*\* 2 of 7 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

diff --git a/regression/cbmc-library/memcpy-07/main.c b/regression/cbmc-library/memcpy-07/main.c
@@ -1,4 +1,5 @@
 // #include <string.h> intentionally omitted
+void *memcpy();
 
 struct c
 {

diff --git a/regression/cbmc/String_Abstraction17/strcpy-no-decl.c b/regression/cbmc/String_Abstraction17/strcpy-no-decl.c
@@ -1,4 +1,5 @@
-void *malloc(unsigned);
+#include <stdlib.h>
+// string.h intentionally omitted
 
 char *make_str()
 {

diff --git a/regression/cbmc/String_Abstraction17/test.desc b/regression/cbmc/String_Abstraction17/test.desc
@@ -1,11 +1,13 @@
 CORE
 strcpy-no-decl.c
 --string-abstraction --validate-goto-model
-Condition: strlen type inconsistency
-^EXIT=(127|134)$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-While this test currently passes when omitting --validate-goto-model, we should
-expect a report of type inconsistencies as no forward declarations are present.
+The linker is able to fix up type inconsistencies of the missing function
+declarations, but the absence of a declaration of strlen results in not picking
+up the library model. Consequently the assumption does not work as intended, and
+verification fails. Adding #include <string.h> makes verification pass as
+expected.
diff --git a/regression/cbmc/array_of_bool_as_bitvec/main.c b/regression/cbmc/array_of_bool_as_bitvec/main.c
@@ -3,6 +3,7 @@
 #include <stdlib.h>
 
 __CPROVER_bool w[8];
+__CPROVER_bool v[__CPROVER_constant_infinity_uint];
 
 void main()
 {

diff --git a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc
@@ -1,15 +1,15 @@
 CORE broken-smt-backend
 main.c
 --smt2 --outfile -
-\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\)
-\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\)
-\(= \(select array\.3 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\)
+\(= \(select array_of\.0 i\) \(ite false #b1 #b0\)\)
+\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\)
+\(= \(select array\.1 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
-\(= \(select array_of\.2 i\) false\)
-\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
-\(= \(select array\.3 \(_ bv\d+ 64\)\) false\)
+\(= \(select array_of\.0 i\) false\)
+\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
+\(= \(select array\.1 \(_ bv\d+ 64\)\) false\)
 --
 This test checks for correctness of BitVec-array encoding of Boolean arrays.
 

diff --git a/regression/cbmc/enum-trace1/main.c b/regression/cbmc/enum-trace1/main.c
@@ -16,6 +16,9 @@ typedef enum ENUMT
 
 void test(enum ENUM e, enum_t t)
 {
+  // ensure sane input values
+  __CPROVER_assume(__CPROVER_enum_is_in_range(e));
+  __CPROVER_assume(__CPROVER_enum_is_in_range(t));
   enum ENUM ee = e;
   enum_t tt = t;
 

diff --git a/regression/cbmc/xml-escaping/debug_output.desc b/regression/cbmc/xml-escaping/debug_output.desc
@@ -4,7 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-⇔ false
 \¬main\:\:1\:\:x\!0\@1\#1
 --
 XML does not support escaping non-printable character

diff --git a/regression/cbmc/xml-trace/test.desc b/regression/cbmc/xml-trace/test.desc
@@ -7,7 +7,7 @@ activate-multi-line-match
 VERIFICATION FAILED
 <assignment assignment_type="actual_parameter" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>union myunion</full_lhs_type>\n\s*<full_lhs>u</full_lhs>
 <value>\{ \.i=\d+ll? \}</value>\n\s*<value_expression>\n\s*<union>\n\s*<member member_name="i">\n\s*<integer binary="\d+" c_type=".*int.*" width="\d+">\d+</integer>\n\s*</member>\n\s*</union>\n\s*</value_expression>
-<assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" function="test" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>signed long( long)? int</full_lhs_type>\n\s*<full_lhs>u\.i</full_lhs>\n\s*<full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>\n\s*</assignment>
+<assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" function="test" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>(signed long( long)? int|int64_t)</full_lhs_type>\n\s*<full_lhs>u\.i</full_lhs>\n\s*<full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>\n\s*</assignment>
 --
 ^warning: ignoring
 --

diff --git a/regression/cprover/arrays/array1.desc b/regression/cprover/arrays/array1.desc
@@ -3,11 +3,11 @@ array1.c
 --text --solve --inline --no-safety
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
 ^\[main\.assertion\.3\] line \d+ property 3: REFUTED$

diff --git a/regression/cprover/arrays/array2.desc b/regression/cprover/arrays/array2.desc
@@ -3,9 +3,9 @@ array2.c
 --text --solve --inline --no-safety
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. \(S23\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S24\(ς\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$
+^\(\d+\) ∀ ς : state \. \(S13\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S14\(ς\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --
diff --git a/regression/cprover/basic/assume1.desc b/regression/cprover/basic/assume1.desc
@@ -6,9 +6,9 @@ assume1.c
 ^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$
 ^ \(\d+\) S0 = SInitial$
 ^ \(\d+\) S1 = S0$
-^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S21\(ς\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
+^\(\d+\) ∀ ς : state \. \(S10\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S11\(ς\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --
diff --git a/regression/cprover/basic/basic1.desc b/regression/cprover/basic/basic1.desc
@@ -5,8 +5,8 @@ basic1.c
 ^SIGNAL=0$
 ^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$
 ^ \(\d+\) S0 = SInitial$
-^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/basic/basic2.desc b/regression/cprover/basic/basic2.desc
@@ -3,11 +3,11 @@ basic2.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
-^\(\d+\) S19 = S18$
-^\(\d+\) S20 = S19$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(\d+\) S22 = S21$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)$
+^\(\d+\) S9 = S8$
+^\(\d+\) S10 = S9$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
+^\(\d+\) S12 = S11$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/basic/basic3.desc b/regression/cprover/basic/basic3.desc
@@ -3,10 +3,10 @@ basic3.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)
-\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝y❞:=0\]\)
-\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=1\]\)
-\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝y❞:=2\]\)
-\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝x❞\) = 1\)
+\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)
+\(\d+\) ∀ ς : state \. S8\(ς\) ⇒ S9\(ς\[❝y❞:=0\]\)
+\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝x❞:=1\]\)
+\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝y❞:=2\]\)
+\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(❝x❞\) = 1\)
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/basic/basic4.desc b/regression/cprover/basic/basic4.desc
@@ -3,9 +3,9 @@ basic4.c
 --text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=2\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝x❞:=2\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
 ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
 --
diff --git a/regression/cprover/basic/basic5.desc b/regression/cprover/basic/basic5.desc
@@ -3,12 +3,12 @@ basic5.c
 --text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
-^\(\d+\) S25 = S24$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
+^\(\d+\) S15 = S14$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --
diff --git a/regression/cprover/basic/basic6.desc b/regression/cprover/basic/basic6.desc
@@ -3,11 +3,11 @@ basic6.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(23\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(24\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
-^\(25\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
-^\(26\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
-^\(27\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
-^\(28\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$
+^\(13\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
+^\(14\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
+^\(15\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
+^\(16\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
+^\(17\) ∀ ς : state \. S14\(ς\) ⇒ S15\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
+^\(18\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/basic/nondet1.desc b/regression/cprover/basic/nondet1.desc
@@ -3,13 +3,13 @@ nondet1.c
 --text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state, nondet::S22-0 : signedbv\[32\] \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=nondet::S22-0\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
-^\(\d+\) S23 = S22$
-^\(\d+\) ∀ ς : state, nondet::S24-0 : signedbv\[32\] \. S23\(ς\) ⇒ S24\(ς\[❝main::1::y❞:=nondet::S24-0\]\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
-^\(\d+\) S25 = S24$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$
+^\(\d+\) ∀ ς : state, nondet::S12-0 : signedbv\[32\] \. S11\(ς\) ⇒ S12\(ς\[❝main::1::x❞:=nondet::S12-0\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
+^\(\d+\) S13 = S12$
+^\(\d+\) ∀ ς : state, nondet::S14-0 : signedbv\[32\] \. S13\(ς\) ⇒ S14\(ς\[❝main::1::y❞:=nondet::S14-0\]\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
+^\(\d+\) S15 = S14$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ S16\(ς\[❝return'❞:=0\]\)$
 ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --