Skip to content

Commit fc3d885

Browse files
authored
Merge pull request #6222 from TGWDB/symex_max_depth_default_max
Symex max depth default max
2 parents d3dc560 + c344048 commit fc3d885

File tree

3 files changed

+3
-1
lines changed

3 files changed

+3
-1
lines changed

jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -113,6 +113,7 @@ void jbmc_parse_optionst::set_default_options(optionst &options)
113113

114114
// Other default
115115
options.set_option("arrays-uf", "auto");
116+
options.set_option("depth", UINT32_MAX);
116117
}
117118

118119
void jbmc_parse_optionst::get_command_line_options(optionst &options)

src/cbmc/cbmc_parse_options.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,7 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
117117

118118
// Other default
119119
options.set_option("arrays-uf", "auto");
120+
options.set_option("depth", UINT32_MAX);
120121
}
121122

122123
void cbmc_parse_optionst::get_command_line_options(optionst &options)

src/goto-symex/symex_main.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -612,7 +612,7 @@ void goto_symext::execute_next_instruction(
612612
merge_gotos(state);
613613

614614
// depth exceeded?
615-
if(symex_config.max_depth != 0 && state.depth > symex_config.max_depth)
615+
if(state.depth > symex_config.max_depth)
616616
{
617617
// Rule out this path:
618618
symex_assume_l2(state, false_exprt());

0 commit comments

Comments
 (0)