diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc index 1e35e023c98..cd46dae86ce 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc @@ -9,10 +9,10 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc index 1ff684bf0a6..0c12978ae7c 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc @@ -10,10 +10,10 @@ replacing function pointer by 3 possible targets ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc index 1e35e023c98..cd46dae86ce 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc @@ -9,10 +9,10 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc index 1e35e023c98..cd46dae86ce 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc @@ -9,10 +9,10 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc index 1e35e023c98..cd46dae86ce 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc @@ -9,10 +9,10 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc index c4ac12fc4cd..18950ead388 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc @@ -9,10 +9,10 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring -^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ -^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$ +^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$ function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/constant_propagation_05/test.desc b/regression/goto-analyzer/constant_propagation_05/test.desc index e84fdb08b4f..7db491e7874 100644 --- a/regression/goto-analyzer/constant_propagation_05/test.desc +++ b/regression/goto-analyzer/constant_propagation_05/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 12 function main, assertion j!=3: Failure (if reachable)$ +^\[main.assertion.1\] file main.c line 12 function main, assertion j != 3: Failure \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_10/test.desc b/regression/goto-analyzer/constant_propagation_10/test.desc index 527325b84bb..25fbc280876 100644 --- a/regression/goto-analyzer/constant_propagation_10/test.desc +++ b/regression/goto-analyzer/constant_propagation_10/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 10 function main, assertion a\[0\]==2: Failure$ +^\[main.assertion.1\] file main.c line 10 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: Failure$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc index 4e9c8715429..c3eb2ca93e9 100644 --- a/regression/goto-analyzer/constant_propagation_11/test.desc +++ b/regression/goto-analyzer/constant_propagation_11/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0$ +^Simplified: assert: 1, assume: 0, goto: 0, assigns: 0, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 0, function calls: 0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_13/test.desc b/regression/goto-analyzer/constant_propagation_13/test.desc index 2d2e078a424..44ebe6f09e6 100644 --- a/regression/goto-analyzer/constant_propagation_13/test.desc +++ b/regression/goto-analyzer/constant_propagation_13/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion y==0: Failure (if reachable)$ +^\[main.assertion.1\] file main.c line 9 function main, assertion y == 0: Failure \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc index fc3be910670..cf993822161 100644 --- a/regression/goto-analyzer/constant_propagation_14/test.desc +++ b/regression/goto-analyzer/constant_propagation_14/test.desc @@ -3,7 +3,7 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: Success$ -^\[main.assertion.2\] file main.c line 12 function main, assertion a\[0\]==1 && a\[0\]==2: Failure$ +^\[main.assertion.1\] file main.c line 11 function main, assertion tmp_if_expr: Success$ +^\[main.assertion.2\] file main.c line 12 function main, assertion tmp_if_expr\$1: Failure$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_15/test.desc b/regression/goto-analyzer/constant_propagation_15/test.desc index aba11ba0c06..d3c619d08ef 100644 --- a/regression/goto-analyzer/constant_propagation_15/test.desc +++ b/regression/goto-analyzer/constant_propagation_15/test.desc @@ -3,6 +3,6 @@ main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion a\[0\]==2: Failure$ +^\[main.assertion.1\] file main.c line 9 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: Failure$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_02/test.desc b/regression/goto-analyzer/intervals_02/test.desc index fa4f926287f..b81b93bd2a0 100644 --- a/regression/goto-analyzer/intervals_02/test.desc +++ b/regression/goto-analyzer/intervals_02/test.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 && x < 100: Success$ +^\[main.assertion.1\] file main.c line 5 function main, assertion x > -10 \&\& x < 100: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_03/test.desc b/regression/goto-analyzer/intervals_03/test.desc index 79042c334de..d9e5e290723 100644 --- a/regression/goto-analyzer/intervals_03/test.desc +++ b/regression/goto-analyzer/intervals_03/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 || x < 100: Success$ +^\[main.assertion.1\] file main.c line 6 function main, assertion x > -10 \|\| x < 100: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_04/test.desc b/regression/goto-analyzer/intervals_04/test.desc index 5bb03255f37..e28af3a1892 100644 --- a/regression/goto-analyzer/intervals_04/test.desc +++ b/regression/goto-analyzer/intervals_04/test.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 && i <= 2: Success$ +^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 && i <= 2: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_05/test.desc b/regression/goto-analyzer/intervals_05/test.desc index 5c9af29a2b1..d059546aab8 100644 --- a/regression/goto-analyzer/intervals_05/test.desc +++ b/regression/goto-analyzer/intervals_05/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 || i <= 2: Success$ +^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 \|\| i <= 2: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_06/test.desc b/regression/goto-analyzer/intervals_06/test.desc index 2dc8d29a3b6..d5836b3fde9 100644 --- a/regression/goto-analyzer/intervals_06/test.desc +++ b/regression/goto-analyzer/intervals_06/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 || x > 100: Failure (if reachable)$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 \|\| x > 100: Failure \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_07/test.desc b/regression/goto-analyzer/intervals_07/test.desc index aa3962f39de..d5fbbb70b93 100644 --- a/regression/goto-analyzer/intervals_07/test.desc +++ b/regression/goto-analyzer/intervals_07/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 && x > 100: Failure (if reachable)$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 \&\& x > 100: Failure \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_08/test.desc b/regression/goto-analyzer/intervals_08/test.desc index 7b83ecd0f21..c8fff24bba7 100644 --- a/regression/goto-analyzer/intervals_08/test.desc +++ b/regression/goto-analyzer/intervals_08/test.desc @@ -3,6 +3,6 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 6 function main, assertion x < -10 && x < 100: Failure (if reachable)$ +^\[main.assertion.1\] file main.c line 6 function main, assertion x < -10 \&\& x < 100: Failure \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_09/test.desc b/regression/goto-analyzer/intervals_09/test.desc index 83776b8ae34..31f685aa72f 100644 --- a/regression/goto-analyzer/intervals_09/test.desc +++ b/regression/goto-analyzer/intervals_09/test.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 9 function main, assertion i>=1 && i<=2: Success$ +^\[main.assertion.1\] file main.c line 8 function main, assertion i >= 1 \&\& i <= 2: Success$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_10/test.desc b/regression/goto-analyzer/intervals_10/test.desc index 468ce13a550..a359da82f4f 100644 --- a/regression/goto-analyzer/intervals_10/test.desc +++ b/regression/goto-analyzer/intervals_10/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ ^\[main.assertion.1\] file main.c line 8 function main, assertion j<=100: Success$ ^\[main.assertion.2\] file main.c line 11 function main, assertion j<101: Success$ -^\[main.assertion.3\] file main.c line 14 function main, assertion j>100: Failure (if reachable)$ +^\[main.assertion.3\] file main.c line 14 function main, assertion j>100: Failure \(if reachable\)$ ^\[main.assertion.4\] file main.c line 17 function main, assertion j<99: Unknown$ -^\[main.assertion.5\] file main.c line 20 function main, assertion j==100: Failure (if reachable)$ +^\[main.assertion.5\] file main.c line 20 function main, assertion j==100: Failure \(if reachable\)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals_11/test.desc b/regression/goto-analyzer/intervals_11/test.desc index 799ad36f64f..05d8d74bd0d 100644 --- a/regression/goto-analyzer/intervals_11/test.desc +++ b/regression/goto-analyzer/intervals_11/test.desc @@ -3,7 +3,7 @@ main.c --intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file main.c line 30 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: Unknown$ -^\[main.assertion.2\] file main.c line 35 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: Unknown$ +^\[main.assertion.1\] file main.c line 30 function main, assertion y\[i\]>=-1.0f \&\& y\[i\]<=1.0f: Unknown$ +^\[main.assertion.2\] file main.c line 35 function main, assertion y\[i\]>=-1.0f \&\& y\[i\]<=1.0f: Unknown$ -- ^warning: ignoring diff --git a/regression/strings/test_index_of/test.desc b/regression/strings/test_index_of/test.desc index dcb245dbf5e..9da2a9e9eb2 100644 --- a/regression/strings/test_index_of/test.desc +++ b/regression/strings/test_index_of/test.desc @@ -5,5 +5,5 @@ test.c ^SIGNAL=0$ ^\[main.assertion.1\] assertion firstSlash == 3: SUCCESS$ ^\[main.assertion.2\] assertion lastSlash == 7: SUCCESS$ -^\[main.assertion.3\] assertion firstSlash != 3 || lastSlash != 7: FAILURE$ +^\[main.assertion.3\] assertion firstSlash != 3 \|\| lastSlash != 7: FAILURE$ -- diff --git a/regression/strings/test_int/test.desc b/regression/strings/test_int/test.desc index 0638394661c..f89a9bf1907 100644 --- a/regression/strings/test_int/test.desc +++ b/regression/strings/test_int/test.desc @@ -6,5 +6,5 @@ test.c ^\[main.assertion.1\] assertion __CPROVER_char_at\(s,0\) == .1.: SUCCESS$ ^\[main.assertion.2\] assertion __CPROVER_char_at\(s,1\) == .2.: SUCCESS$ ^\[main.assertion.3\] assertion j == 234: SUCCESS$ -^\[main.assertion.4\] assertion j < 233 || __CPROVER_char_at\(s,2\) == .4.: FAILURE$ +^\[main.assertion.4\] assertion j < 233 \|\| __CPROVER_char_at\(s,2\) == .4.: FAILURE$ --