Skip to content

Commit 029dece

Browse files
committed
Do not use std-invariants with k-induction
Standard invariants seem to cause more trouble than with array invariants (already fixed). Let us try to disable them completely since they should bring no significant benefits. There are some tests which still require standard invariants with k-induction. Add the option explicitly and we will debug them later.
1 parent e1ba240 commit 029dece

File tree

4 files changed

+3
-4
lines changed

4 files changed

+3
-4
lines changed

regression/kiki/induction5/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--k-induction
3+
--k-induction --std-invariants
44
^EXIT=10$
55
^SIGNAL=0$
66
^.*FAILURE$

regression/kiki/induction7/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--k-induction
3+
--k-induction --std-invariants
44
^EXIT=10$
55
^SIGNAL=0$
66
^.*FAILURE$

regression/kiki/nested12/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--k-induction
3+
--k-induction --std-invariants
44
^EXIT=10$
55
^SIGNAL=0$
66
^.*FAILURE$

src/2ls/2ls_parse_options.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -296,7 +296,6 @@ void twols_parse_optionst::get_command_line_options(optionst &options)
296296
// do k-induction refinement
297297
if(cmdline.isset("k-induction"))
298298
{
299-
options.set_option("std-invariants", true);
300299
options.set_option("k-induction", true);
301300
options.set_option("inline", true);
302301
if(!cmdline.isset("unwind"))

0 commit comments

Comments
 (0)