fix tests

kroening · kroening · commit 676b3596b3b3 · 2022-03-09T12:42:08.000Z
diff --git a/regression/cprover/arrays/array1.desc b/regression/cprover/arrays/array1.desc
@@ -3,9 +3,9 @@ array1.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(19\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, 1\):=10\]\)$
-^\(20\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[element_address\(❝array❞, 2\):=20\]\)$
-^\(21\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, 1\)\) = 10\)$
-^\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, 2\)\) = 20\)$
-^\(25\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝array❞, 2\)\) = 30\)$
+^\(\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\)$
 --
diff --git a/regression/cprover/arrays/array2.desc b/regression/cprover/arrays/array2.desc
@@ -3,7 +3,7 @@ array2.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(\(ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S24\(ς\)\)$
-^\(24\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$
-^\(26\) ∀ ς : 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 \. 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\]\)\)\)\)$
 --
diff --git a/regression/cprover/basic/assume1.desc b/regression/cprover/basic/assume1.desc
@@ -3,11 +3,11 @@ assume1.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^ \(1\) ∀ ς : state \. SInitial\(ς\)$
-^ \(2\) S0 = SInitial$
-^ \(3\) S1 = S0$
-^\(20\) ∀ ς : state \. S20\(ς\) ⇒ \(\(ς\(❝main::1::x❞\) ≥ 10\) ⇒ S21\(ς\)\)$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
-^\(23\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
-^\(26\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝return'❞:=nondet25\]\)$
+^ \(\d+\) ∀ ς : 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 \. S24\(ς\) ⇒ S25\(ς\[❝return'❞:=nondet25\]\)$
 --
diff --git a/regression/cprover/basic/basic1.desc b/regression/cprover/basic/basic1.desc
@@ -3,9 +3,9 @@ basic1.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^ \(1\) ∀ ς : state \. SInitial\(ς\)$
-^ \(2\) S0 = SInitial$
-^\(17\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
-^\(20\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^ \(\d+\) ∀ ς : state \. SInitial\(ς\)$
+^ \(\d+\) S0 = SInitial$
+^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
 --
diff --git a/regression/cprover/basic/basic2.desc b/regression/cprover/basic/basic2.desc
@@ -3,10 +3,10 @@ basic2.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(17\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
-^\(18\) S19 = S18$
-^\(19\) S20 = S19$
-^\(20\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(21\) S22 = S21$
-^\(22\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^\(\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\)$
 --
diff --git a/regression/cprover/basic/basic3.desc b/regression/cprover/basic/basic3.desc
@@ -3,9 +3,9 @@ basic3.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-\(17\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)
-\(18\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝y❞:=0\]\)
-\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=1\]\)
-\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝y❞:=2\]\)
-\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝x❞\) = 1\)
+\(\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\)
 --
diff --git a/regression/cprover/basic/basic4.desc b/regression/cprover/basic/basic4.desc
@@ -3,8 +3,8 @@ basic4.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(17\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
-^\(20\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=2\]\)$
-^\(22\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=2\]\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
 --
diff --git a/regression/cprover/basic/basic5.desc b/regression/cprover/basic/basic5.desc
@@ -3,10 +3,10 @@ basic5.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
-^\(22\) S23 = S22$
-^\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
-^\(24\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
-^\(25\) S25 = S24$
-^\(26\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
+^\(\d+\) S23 = S22$
+^\(\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❞\)\)$
 --
diff --git a/regression/cprover/basic/nondet1.desc b/regression/cprover/basic/nondet1.desc
@@ -3,11 +3,11 @@ nondet1.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=nondet22\]\)$
-^\(22\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
-^\(23\) S23 = S22$
-^\(24\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::y❞:=nondet24\]\)$
-^\(25\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
-^\(26\) S25 = S24$
-^\(27\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=nondet22\]\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
+^\(\d+\) S23 = S22$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::y❞:=nondet24\]\)$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
+^\(\d+\) S25 = S24$
+^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$
 --
diff --git a/regression/cprover/branching/branching1.desc b/regression/cprover/branching/branching1.desc
@@ -3,17 +3,17 @@ branching1.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(20\) ∀ ς : state \. S20\(ς\) ⇒ \(¬\(ς\(❝main::1::x❞\) ≥ 5\) \? S21T\(ς\) : S21\(ς\)\)$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
-^\(22\) S22 = S21$
-^\(23\) ∀ ς : state \. S22\(ς\) ⇒ \(0 ≠ 0\)$
-^\(24\) S23 = S22$
-^\(25\) S24 = S23$
-^\(26\) ∀ ς : state \. S21T\(ς\) ⇒ \(ς\(❝main::1::x❞\) < 5\)$
-^\(27\) S25 = S21T$
-^\(28\) ∀ ς : state \. S25\(ς\) ⇒ \(0 ≠ 0\)$
-^\(29\) S26 = S25$
-^\(30\) ∀ ς : state \. S24\(ς\) ⇒ S27in\(ς\)$
-^\(31\) ∀ ς : state \. S26\(ς\) ⇒ S27in\(ς\)$
-^\(32\) S27 = S27in$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(¬\(ς\(❝main::1::x❞\) ≥ 5\) \? S21T\(ς\) : S21\(ς\)\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
+^\(\d+\) S22 = S21$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(0 ≠ 0\)$
+^\(\d+\) S23 = S22$
+^\(\d+\) S24 = S23$
+^\(\d+\) ∀ ς : state \. S21T\(ς\) ⇒ \(ς\(❝main::1::x❞\) < 5\)$
+^\(\d+\) S25 = S21T$
+^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(0 ≠ 0\)$
+^\(\d+\) S26 = S25$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S27in\(ς\)$
+^\(\d+\) ∀ ς : state \. S26\(ς\) ⇒ S27in\(ς\)$
+^\(\d+\) S27 = S27in$
 --
diff --git a/regression/cprover/branching/branching2.desc b/regression/cprover/branching/branching2.desc
@@ -3,11 +3,11 @@ branching2.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(¬\(ς\(❝main::1::a❞\) ≥ 5\) \? S22T\(ς\) : S22\(ς\)\)$
-^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::b❞:=1\]\)$
-^\(23\) S24 = S23$
-^\(24\) ∀ ς : state \. S22T\(ς\) ⇒ S25\(ς\[❝main::1::b❞:=0\]\)$
-^\(25\) ∀ ς : state \. S24\(ς\) ⇒ S26in\(ς\)$
-^\(26\) ∀ ς : state \. S25\(ς\) ⇒ S26in\(ς\)$
-^\(27\) S26 = S26in$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(¬\(ς\(❝main::1::a❞\) ≥ 5\) \? S22T\(ς\) : S22\(ς\)\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::b❞:=1\]\)$
+^\(\d+\) S24 = S23$
+^\(\d+\) ∀ ς : state \. S22T\(ς\) ⇒ S25\(ς\[❝main::1::b❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S26in\(ς\)$
+^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26in\(ς\)$
+^\(\d+\) S26 = S26in$
 --
diff --git a/regression/cprover/pointers/char_pointers2.desc b/regression/cprover/pointers/char_pointers2.desc
@@ -3,14 +3,14 @@ char_pointers2.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(20\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::x❞:=16909060\]\)$
-^\(21\) S22 = S21$
-^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=cast\(address_of\(ς\(❝main::1::x❞\)\), signedbv\[8\]\*\)\]\)$
-^\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(0, signedbv\[64\]\)\), signedbv\[32\]\) = 4\)$
-^\(24\) S24 = S23$
-^\(25\) ∀ ς : state \. S24\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(1, signedbv\[64\]\)\), signedbv\[32\]\) = 3\)$
-^\(26\) S25 = S24$
-^\(27\) ∀ ς : state \. S25\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(2, signedbv\[64\]\)\), signedbv\[32\]\) = 2\)$
-^\(28\) S26 = S25$
-^\(29\) ∀ ς : state \. S26\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(3, signedbv\[64\]\)\), signedbv\[32\]\) = 1\)$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::x❞:=16909060\]\)$
+^\(\d+\) S22 = S21$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=cast\(address_of\(ς\(❝main::1::x❞\)\), signedbv\[8\]\*\)\]\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(0, signedbv\[64\]\)\), signedbv\[32\]\) = 4\)$
+^\(\d+\) S24 = S23$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(1, signedbv\[64\]\)\), signedbv\[32\]\) = 3\)$
+^\(\d+\) S25 = S24$
+^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(2, signedbv\[64\]\)\), signedbv\[32\]\) = 2\)$
+^\(\d+\) S26 = S25$
+^\(\d+\) ∀ ς : state \. S26\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(3, signedbv\[64\]\)\), signedbv\[32\]\) = 1\)$
 --
diff --git a/regression/cprover/pointers/pointers1.desc b/regression/cprover/pointers/pointers1.desc
@@ -3,8 +3,8 @@ pointers1.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=10\]\)$
-^\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝p❞:=address_of\(ς\(❝x❞\)\)\]\)$
-^\(24\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝y❞:=ς\(ς\(❝p❞\)\)\]\)$
-^\(25\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝y❞\) = 10\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=10\]\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝p❞:=address_of\(ς\(❝x❞\)\)\]\)$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝y❞:=ς\(ς\(❝p❞\)\)\]\)$
+^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝y❞\) = 10\)$
 --
diff --git a/regression/cprover/pointers/pointers10.desc b/regression/cprover/pointers/pointers10.desc
@@ -3,7 +3,7 @@ pointers10.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(¬\(ς\(❝main::1::p❞\) = address_of\(ς\(❝main::1::x❞\)\)\) \? S22T\(ς\) : S22\(ς\)\)$
-^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[ς\(❝main::1::p❞\):=123\]\)$
-^\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 123\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(¬\(ς\(❝main::1::p❞\) = address_of\(ς\(❝main::1::x❞\)\)\) \? S22T\(ς\) : S22\(ς\)\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[ς\(❝main::1::p❞\):=123\]\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 123\)$
 --
diff --git a/regression/cprover/pointers/pointers2.desc b/regression/cprover/pointers/pointers2.desc
@@ -3,10 +3,10 @@ pointers2.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=10\]\)$
-^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝p❞:=address_of\(ς\(❝x❞\)\)\]\)$
-^\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝p❞\):=20\]\)$
-^\(24\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 20\)$
-^\(25\) S25 = S24$
-^\(26\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=10\]\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝p❞:=address_of\(ς\(❝x❞\)\)\]\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝p❞\):=20\]\)$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 20\)$
+^\(\d+\) S25 = S24$
+^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$
 --
diff --git a/regression/cprover/pointers/pointers3.desc b/regression/cprover/pointers/pointers3.desc
@@ -3,6 +3,6 @@ pointers3.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(20\) ∀ ς : state \. S20\(ς\) ⇒ \(\(ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S21\(ς\)\)$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(\(ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S21\(ς\)\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$
 --
diff --git a/regression/cprover/pointers/pointers4.desc b/regression/cprover/pointers/pointers4.desc
@@ -3,8 +3,8 @@ pointers4.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(17\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(\(ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S22\(ς\)\)$
-^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=address_of\(ς\(❝x❞\)\)\]\)$
-^\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(\(ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S22\(ς\)\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=address_of\(ς\(❝x❞\)\)\]\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$
 --
diff --git a/regression/cprover/pointers/pointers5.desc b/regression/cprover/pointers/pointers5.desc
@@ -3,7 +3,7 @@ pointers5.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(17\) ∀ ς18 : state \. S17\(ς18\) ⇒ S18\(ς18\[❝x❞:=0\]\)$
-^\(22\) ∀ ς23 : state \. S22\(ς23\) ⇒ \(\(S22\(❝main::1::p❞\) = S22\(❝main::1::q❞\)\) ⇒ S23\(ς23\)\)$
-^\(23\) ∀ ς24 : state \. S23\(ς24\) ⇒ \(ς24\(S23\(❝main::1::p❞\)\) = ς24\(S23\(❝main::1::q❞\)\)\)$
+^\(\d+\) ∀ ς18 : state \. S17\(ς18\) ⇒ S18\(ς18\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς23 : state \. S22\(ς23\) ⇒ \(\(S22\(❝main::1::p❞\) = S22\(❝main::1::q❞\)\) ⇒ S23\(ς23\)\)$
+^\(\d+\) ∀ ς24 : state \. S23\(ς24\) ⇒ \(ς24\(S23\(❝main::1::p❞\)\) = ς24\(S23\(❝main::1::q❞\)\)\)$
 --
diff --git a/regression/cprover/pointers/pointers6.desc b/regression/cprover/pointers/pointers6.desc
@@ -3,8 +3,8 @@ pointers6.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=address_of\(ς\(❝x❞\)\)\]\)$
-\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝main::1::p❞\):=10\]\)$
-\(24\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝main::1::q❞:=address_of\(ς\(❝x❞\)\)\]\)$
-\(25\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(ς\(❝main::1::q❞\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=address_of\(ς\(❝x❞\)\)\]\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝main::1::p❞\):=10\]\)$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝main::1::q❞:=address_of\(ς\(❝x❞\)\)\]\)$
+^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(ς\(❝main::1::q❞\)\) = 10\)$
 --
diff --git a/regression/cprover/pointers/pointers7.desc b/regression/cprover/pointers/pointers7.desc
@@ -3,13 +3,13 @@ pointers7.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(17\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝p❞:=NULL\]\)$
-^\(18\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝x❞:=0\]\)$
-^\(19\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝y❞:=0\]\)$
-^\(20\) S21 = S20$
-^\(21\) S22 = S21$
-^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=10\]\)$
-^\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝p❞:=address_of\(ς\(❝y❞\)\)\]\)$
-^\(24\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[ς\(❝p❞\):=20\]\)$
-^\(25\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$
+^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝p❞:=NULL\]\)$
+^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝y❞:=0\]\)$
+^\(\d+\) S21 = S20$
+^\(\d+\) S22 = S21$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=10\]\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝p❞:=address_of\(ς\(❝y❞\)\)\]\)$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[ς\(❝p❞\):=20\]\)$
+^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$
 --
diff --git a/regression/cprover/pointers/pointers8.desc b/regression/cprover/pointers/pointers8.desc
@@ -3,11 +3,11 @@ pointers8.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(20\) ∀ ς : state \. S20\(ς\) ⇒ \(¬\(pointer_object\(cast\(ς\(❝main::1::p❞\), empty\*\)\) = pointer_object\(cast\(address_of\(ς\(❝main::1::p❞\)\), empty\*\)\)\) ⇒ S21\(ς\)\)$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[ς\(❝main::1::p❞\):=123\]\)$
-^\(22\) S23 = S22$
-^\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::p_value❞:=ς\(ς\(❝main::1::p❞\)\)\]\)$
-^\(24\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::p_value❞\) = 123\)$
-^\(25\) S25 = S24$
-^\(26\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(¬\(pointer_object\(cast\(ς\(❝main::1::p❞\), empty\*\)\) = pointer_object\(cast\(address_of\(ς\(❝main::1::p❞\)\), empty\*\)\)\) ⇒ S21\(ς\)\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[ς\(❝main::1::p❞\):=123\]\)$
+^\(\d+\) S23 = S22$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::p_value❞:=ς\(ς\(❝main::1::p❞\)\)\]\)$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::p_value❞\) = 123\)$
+^\(\d+\) S25 = S24$
+^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$
 --
diff --git a/regression/cprover/pointers/pointers9.desc b/regression/cprover/pointers/pointers9.desc
@@ -3,7 +3,7 @@ pointers9.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=123\]\)$
-^\(22\) ∀ ς : state \. S22\(ς\) ⇒ \(¬\(ς\(❝main::1::p❞\) = address_of\(ς\(❝main::1::x❞\)\)\) \? S23T\(ς\) : S23\(ς\)\)$
-^\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 123\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=123\]\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(¬\(ς\(❝main::1::p❞\) = address_of\(ς\(❝main::1::x❞\)\)\) \? S23T\(ς\) : S23\(ς\)\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 123\)$
 --
diff --git a/regression/cprover/pointers/struct_pointer1.desc b/regression/cprover/pointers/struct_pointer1.desc
@@ -3,9 +3,9 @@ struct_pointer1.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\(20\) ∀ ς : state \. S20\(ς\) ⇒ \(¬\(pointer_object\(cast\(ς\(❝main::1::my_struct_ptr❞\), empty\*\)\) = pointer_object\(cast\(address_of\(ς\(❝main::1::my_struct_ptr❞\)\), empty\*\)\)\) ⇒ S21\(ς\)\)$
-^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$
-^\(22\) S23 = S22$
-^\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::my_struct_data❞:=ς\(ς\(❝main::1::my_struct_ptr❞\)\.❝data❞\)\]\)$
-^\(24\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::my_struct_data❞\) = 123\)$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(¬\(pointer_object\(cast\(ς\(❝main::1::my_struct_ptr❞\), empty\*\)\) = pointer_object\(cast\(address_of\(ς\(❝main::1::my_struct_ptr❞\)\), empty\*\)\)\) ⇒ S21\(ς\)\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$
+^\(\d+\) S23 = S22$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::my_struct_data❞:=ς\(ς\(❝main::1::my_struct_ptr❞\)\.❝data❞\)\]\)$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::my_struct_data❞\) = 123\)$
 --
diff --git a/regression/cprover/pointers/struct_pointer2.desc b/regression/cprover/pointers/struct_pointer2.desc
diff --git a/regression/cprover/structs/struct1.desc b/regression/cprover/structs/struct1.desc
diff --git a/regression/cprover/structs/struct2.desc b/regression/cprover/structs/struct2.desc
