Skip to content

Commit 4bebee9

Browse files
Merge pull request #790 from romainbrenguier/string-solver-refine-array-option
Allowing some options for string refinement
2 parents cb065bf + 44041ae commit 4bebee9

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

src/cbmc/cbmc_solvers.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -242,6 +242,15 @@ cbmc_solverst::solvert* cbmc_solverst::get_string_refinement()
242242
if(options.get_bool_option("string-printable"))
243243
string_refinement->enforce_printable_characters();
244244

245+
if(options.get_option("max-node-refinement")!="")
246+
string_refinement->max_node_refinement=
247+
options.get_unsigned_int_option("max-node-refinement");
248+
249+
string_refinement->do_array_refinement=
250+
options.get_bool_option("refine-arrays");
251+
string_refinement->do_arithmetic_refinement=
252+
options.get_bool_option("refine-arithmetic");
253+
245254
return new solvert(string_refinement, prop);
246255
}
247256

0 commit comments

Comments
 (0)