Fix SMT2 output determinism by using ordered maps

jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc

@@ -4,7 +4,7 @@ Test
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-\s*// 0 no location\n\s*CALL java::Other\.<clinit_wrapper>\(\)\s*// 1 no location\s*DECL .*::total
+\s*// 26 no location\n\s*CALL java::Other\.<clinit_wrapper>\(\)\s*// 27 no location\s*DECL .*::total
 --
 --
 This checks that the clinit-wrapper function is called once, even though there are two calls in the source

jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc

@@ -4,7 +4,7 @@ Test
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-\s*// 0 no location\n\s*CALL java::Other\.<clinit_wrapper>\(\)\s*// 1 no location\s*CALL java::Third\.<clinit_wrapper>\(\)\s*// 2 no location\s*DECL .*::total
+\s*// 28 no location\n\s*CALL java::Other\.<clinit_wrapper>\(\)\s*// 29 no location\s*CALL java::Third\.<clinit_wrapper>\(\)\s*// 30 no location\s*DECL .*::total
 --
 --
 This checks that the clinit-wrapper function is called once, even though there are two calls in the source

regression/cbmc/deterministic-smt-output/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+int main()
+{
+  int x;
+  int y;
+  int z = x + y;
+  assert(z == x + y);
+  return 0;
+}

regression/cbmc/deterministic-smt-output/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--smt2 --outfile -
+activate-multi-line-match
+\(declare-fun \|main::1::x!0@1#1\| \(\) \(_ BitVec 32\)\)(?s:.)*\(declare-fun \|main::1::y!0@1#1\| \(\) \(_ BitVec 32\)\)
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that x is always declared before y, i.e., in lexicographic order.

regression/cprover/function_calls/call_no_body1.desc

@@ -4,6 +4,6 @@ call_no_body1.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\*\*\*\* WARNING: no body for function function_without_body$
-^\(\d+\) ∀ ς : state, nondet::S18\.2-0 : signedbv\[32\] \. S18\.1\(ς\) ⇒ S18\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S18\.2-0\]\)$
-^\(\d+\) ∀ ς : state \. S18\.2\(ς\) ⇒ S18\.3\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$
+^\(\d+\) ∀ ς : state, nondet::S2\.14-0 : signedbv\[32\] \. S2\.13\(ς\) ⇒ S2\.14\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S2\.14-0\]\)$
+^\(\d+\) ∀ ς : state \. S2\.14\(ς\) ⇒ S2\.15\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$
 --

regression/cprover/function_calls/call_no_body2.desc

@@ -3,5 +3,5 @@ call_no_body2.c
 --text
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state, nondet::S18\.2-0 : signedbv\[32\] \. S18\.1\(ς\) ⇒ S18\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S18\.2-0\]\)$
+^\(\d+\) ∀ ς : state, nondet::S2\.14-0 : signedbv\[32\] \. S2\.13\(ς\) ⇒ S2\.14\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S2\.14-0\]\)$
 --

regression/goto-analyzer/branching-ge/test-always-constants.desc

@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[23, 25\]
-^main::1::p .* TOP @ \[3, 9, 18\]
+^main::1::i .* TOP @ \[37, 39\]
+^main::1::p .* TOP @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-ge/test-always-intervals.desc

@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[5, 5\] @ \[23\]
-^main::1::p .* \[0, A\] @ \[3, 9, 18\]
+^main::1::i .* \[5, 5\] @ \[37\]
+^main::1::p .* \[0, A\] @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-ge/test-always-value-set.desc

@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
+^main::1::i .* value-set-begin: 5 :value-set-end @ \[37\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc

@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[23, 25\]
-^main::1::p .* TOP @ \[3, 9, 18\]
+^main::1::i .* TOP @ \[37, 39\]
+^main::1::p .* TOP @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc

@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\]
-^main::1::p .* \[0, A\] @ \[3, 9, 18\]
+^main::1::i .* \[FFFFFFFB, 5\] @ \[37, 39\]
+^main::1::p .* \[0, A\] @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-ge/test-indeterminate-value-set.desc

@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
+^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[37, 39\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-ge/test-never-constants.desc

@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[23, 25\]
-^main::1::p .* TOP @ \[3, 9, 18\]
+^main::1::i .* TOP @ \[37, 39\]
+^main::1::p .* TOP @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-ge/test-never-intervals.desc

@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\]
-^main::1::p .* \[0, A\] @ \[3, 9, 18\]
+^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[39\]
+^main::1::p .* \[0, A\] @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-ge/test-never-value-set.desc

@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
+^main::1::i .* value-set-begin: -5 :value-set-end @ \[39\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-gt/test-always-constants.desc

@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[23, 25\]
-^main::1::p .* TOP @ \[3, 9, 18\]
+^main::1::i .* TOP @ \[37, 39\]
+^main::1::p .* TOP @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-gt/test-always-intervals.desc

@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[5, 5\] @ \[23\]
-^main::1::p .* \[0, A\] @ \[3, 9, 18\]
+^main::1::i .* \[5, 5\] @ \[37\]
+^main::1::p .* \[0, A\] @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-gt/test-always-value-set.desc

@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
+^main::1::i .* value-set-begin: 5 :value-set-end @ \[37\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc

@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[23, 25\]
-^main::1::p .* TOP @ \[3, 9, 18\]
+^main::1::i .* TOP @ \[37, 39\]
+^main::1::p .* TOP @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc

@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\]
-^main::1::p .* \[0, A\] @ \[3, 9, 18\]
+^main::1::i .* \[FFFFFFFB, 5\] @ \[37, 39\]
+^main::1::p .* \[0, A\] @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-gt/test-indeterminate-value-set.desc

@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
+^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[37, 39\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-gt/test-never-constants.desc

@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[23, 25\]
-^main::1::p .* TOP @ \[3, 9, 18\]
+^main::1::i .* TOP @ \[37, 39\]
+^main::1::p .* TOP @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-gt/test-never-intervals.desc

@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\]
-^main::1::p .* \[0, A\] @ \[3, 9, 18\]
+^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[39\]
+^main::1::p .* \[0, A\] @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-gt/test-never-value-set.desc

@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
+^main::1::i .* value-set-begin: -5 :value-set-end @ \[39\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-le/test-always-constants.desc

@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[23, 25\]
-^main::1::p .* TOP @ \[3, 9, 18\]
+^main::1::i .* TOP @ \[37, 39\]
+^main::1::p .* TOP @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-le/test-always-intervals.desc

@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[5, 5\] @ \[23\]
-^main::1::p .* \[0, A\] @ \[3, 9, 18\]
+^main::1::i .* \[5, 5\] @ \[37\]
+^main::1::p .* \[0, A\] @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-le/test-always-value-set.desc

@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
+^main::1::i .* value-set-begin: 5 :value-set-end @ \[37\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-le/test-indeterminate-constants.desc

@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[23, 25\]
-^main::1::p .* TOP @ \[3, 9, 18\]
+^main::1::i .* TOP @ \[37, 39\]
+^main::1::p .* TOP @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc

@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\]
-^main::1::p .* \[0, A\] @ \[3, 9, 18\]
+^main::1::i .* \[FFFFFFFB, 5\] @ \[37, 39\]
+^main::1::p .* \[0, A\] @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-le/test-indeterminate-value-set.desc

@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
+^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[37, 39\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-le/test-never-constants.desc

@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[23, 25\]
-^main::1::p .* TOP @ \[3, 9, 18\]
+^main::1::i .* TOP @ \[37, 39\]
+^main::1::p .* TOP @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-le/test-never-intervals.desc

@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\]
-^main::1::p .* \[0, A\] @ \[3, 9, 18\]
+^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[39\]
+^main::1::p .* \[0, A\] @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-le/test-never-value-set.desc

@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
+^main::1::i .* value-set-begin: -5 :value-set-end @ \[39\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-lt/test-always-constants.desc

@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[23, 25\]
-^main::1::p .* TOP @ \[3, 9, 18\]
+^main::1::i .* TOP @ \[37, 39\]
+^main::1::p .* TOP @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-lt/test-always-intervals.desc

@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[5, 5\] @ \[23\]
-^main::1::p .* \[0, A\] @ \[3, 9, 18\]
+^main::1::i .* \[5, 5\] @ \[37\]
+^main::1::p .* \[0, A\] @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-lt/test-always-value-set.desc

@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
+^main::1::i .* value-set-begin: 5 :value-set-end @ \[37\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-lt/test-indeterminate-constants.desc

@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[23, 25\]
-^main::1::p .* TOP @ \[3, 9, 18\]
+^main::1::i .* TOP @ \[37, 39\]
+^main::1::p .* TOP @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-lt/test-indeterminate-intervals.desc

@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\]
-^main::1::p .* \[0, A\] @ \[3, 9, 18\]
+^main::1::i .* \[FFFFFFFB, 5\] @ \[37, 39\]
+^main::1::p .* \[0, A\] @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-lt/test-indeterminate-value-set.desc

@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
+^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[37, 39\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-lt/test-never-constants.desc

@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[23, 25\]
-^main::1::p .* TOP @ \[3, 9, 18\]
+^main::1::i .* TOP @ \[37, 39\]
+^main::1::p .* TOP @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-lt/test-never-intervals.desc

@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\]
-^main::1::p .* \[0, A\] @ \[3, 9, 18\]
+^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[39\]
+^main::1::p .* \[0, A\] @ \[17, 23, 32\]
 --

regression/goto-analyzer/branching-lt/test-never-value-set.desc

@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
+^main::1::i .* value-set-begin: -5 :value-set-end @ \[39\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\]
 --

regression/goto-analyzer/liveness-array/test-liveness.desc

@@ -3,7 +3,7 @@ main.c
 --no-standard-checks --variable-sensitivity --vsd-arrays every-element --vsd-values intervals --vsd-liveness --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::x .* TOP @ \[1\]
-^main::1::x .* \{\[0\] = \[0, 0\] @ \[2\]
-^main::1::x .* \{\[0\] = \[2, 3\] @ \[7\]
+^main::1::x .* TOP @ \[15\]
+^main::1::x .* \{\[0\] = \[0, 0\] @ \[16\]
+^main::1::x .* \{\[0\] = \[2, 3\] @ \[21\]
 --