From 44041aeff5ca8d2e69b4167222ed6dac86f0e009 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 10 Apr 2017 11:00:02 +0100 Subject: [PATCH] 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. --- src/cbmc/cbmc_solvers.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index dace046cc17..b647ba17f52 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -242,6 +242,15 @@ cbmc_solverst::solvert* cbmc_solverst::get_string_refinement() if(options.get_bool_option("string-printable")) string_refinement->enforce_printable_characters(); + if(options.get_option("max-node-refinement")!="") + string_refinement->max_node_refinement= + options.get_unsigned_int_option("max-node-refinement"); + + string_refinement->do_array_refinement= + options.get_bool_option("refine-arrays"); + string_refinement->do_arithmetic_refinement= + options.get_bool_option("refine-arithmetic"); + return new solvert(string_refinement, prop); }