esbmc icon indicating copy to clipboard operation
esbmc copied to clipboard

[k-induction] disable partial loops for the k-induction proof rule.

Open lucasccordeiro opened this issue 8 months ago • 7 comments

Summary This commit updates several test description files and a source file in ESBMC. The changes are mainly related to the regression tests for k-induction and its parallel variant. Additionally, the ESBMC parse options source file is updated to disable partial loops for the k-induction proof rule.

Details of Changes Regression Tests for k-Induction Parallel:

regression/k-induction-parallel/count_down_02/test.desc regression/k-induction-parallel/for_infinite_loop_2/test.desc regression/k-induction-parallel/sum06/test.desc regression/k-induction-parallel/terminator_04/test.desc regression/k-induction-parallel/terminator_05/test.desc regression/k-induction-parallel/terminator_06/test.desc regression/k-induction-parallel/trex02/test.desc regression/k-induction-parallel/trex03/test.desc regression/k-induction-parallel/trex04/test.desc regression/k-induction-parallel/while_infinite_loop_1/test.desc

Regression Tests for k-Induction:

regression/k-induction/count_down_02/test.desc regression/k-induction/for_infinite_loop_2/test.desc regression/k-induction/sum06/test.desc regression/k-induction/terminator_04/test.desc regression/k-induction/terminator_05/test.desc regression/k-induction/terminator_06/test.desc regression/k-induction/trex02/test.desc regression/k-induction/trex03/test.desc regression/k-induction/trex04/test.desc regression/k-induction/while_infinite_loop_1/test.desc These updates pertain to the regular k-induction tests and include:

There is a new bug for regression/k-induction/kundu_bug/test.desc and regression/esbmc-cpp/cpp_queue_front_bug/test.desc.

Source File Update:

src/esbmc/esbmc_parseoptions.cpp

lucasccordeiro avatar Jun 12 '24 09:06 lucasccordeiro