Skip to content

Commit 44041ae

Browse files
Allowing some options for string refinement
We allow setting the options refine-arrays, refine-arithmetic and max-node-refinement options in the string solver. Not setting the refine-arrays option can greatly improve performances.
1 parent 531ef7e commit 44041ae

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)