[loops] check 8 benchmarks: diff coverage results for different TG modes

[izlatkin]

check 8 benchmarks: bin-suffix-5.c eq1.c eq2.c even.c mod3.c mod3.c.v+cfa-reducer.c mod4.c odd.c

Here, the coverage by --inv-mode 0 is better than the coverage by --inv-mode 2 and both modes terminate. This is strange. I expect both modes to return the same coverage.

[izlatkin]

there is no diff for all smt2 files.

diff inv-mode_0/bin-suffix-5/bin-suffix-5.smt2 inv_mode_2_phase_prop_no_term/bin-suffix-5/bin-suffix-5.smt2
export TO_TEST=bin-suffix-5
diff inv-mode_0/${TO_TEST}/${TO_TEST}.smt2 inv_mode_2_phase_prop_no_term/${TO_TEST}/${TO_TEST}.smt2
export TO_TEST=eq1
diff inv-mode_0/${TO_TEST}/${TO_TEST}.smt2 inv_mode_2_phase_prop_no_term/${TO_TEST}/${TO_TEST}.smt2
export TO_TEST=eq2
diff inv-mode_0/${TO_TEST}/${TO_TEST}.smt2 inv_mode_2_phase_prop_no_term/${TO_TEST}/${TO_TEST}.smt2
export TO_TEST=even
diff inv-mode_0/${TO_TEST}/${TO_TEST}.smt2 inv_mode_2_phase_prop_no_term/${TO_TEST}/${TO_TEST}.smt2
export TO_TEST=mod3
diff inv-mode_0/${TO_TEST}/${TO_TEST}.smt2 inv_mode_2_phase_prop_no_term/${TO_TEST}/${TO_TEST}.smt2
export TO_TEST=mod3.c.v+cfa-reducer
diff inv-mode_0/${TO_TEST}/${TO_TEST}.smt2 inv_mode_2_phase_prop_no_term/${TO_TEST}/${TO_TEST}.smt2
export TO_TEST=mod4
diff inv-mode_0/${TO_TEST}/${TO_TEST}.smt2 inv_mode_2_phase_prop_no_term/${TO_TEST}/${TO_TEST}.smt2
export TO_TEST=odd
diff inv-mode_0/${TO_TEST}/${TO_TEST}.smt2 inv_mode_2_phase_prop_no_term/${TO_TEST}/${TO_TEST}.smt2

=> TG tool returns the different numbers of testcases.

[izlatkin]

--inv-mode 0log.txt --inv-mode 2 log.txt

[grigoryfedyukovich]

Can you please identify the exact test case(s) that is generated with --inv-mode 0 and not generated with --inv-mode 2?

[izlatkin]

for --inv-mode 0 there are two extra cases:

testcase_1
int cnt_3664 = 0;
int tot_3664 = 0;

static const int inp_3664[] = {};

testcase_2
int cnt_3664 = 0;
int tot_3664 = 0;

static const int inp_3664[] = {};

and there are two cases, which were generated in both modes

testcase_3
int cnt_3664 = 0;
int tot_3664 = 1;

static const int inp_3664[] = {0};

testcase_4
int cnt_3664 = 0;
int tot_3664 = 1;

static const int inp_3664[] = {1};

[izlatkin]

bin-suffix-5.smt2.txt

[grigoryfedyukovich]

Maybe fixed. To test.