Skip to content

Commit

Permalink
Remove string refinement iteration limit
Browse files Browse the repository at this point in the history
This sets the string refinement iteration limit to zero, i.e. unlimited.
The mechanism for providing a limit is left in place, for use probably driven
by a command-line argument by the first user to need that facility.
  • Loading branch information
smowton committed Feb 14, 2018
1 parent 2bb98d9 commit 1ac9abe
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion src/cbmc/cbmc_solvers.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -174,7 +174,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
auto prop=util_make_unique<satcheck_no_simplifiert>();
prop->set_message_handler(get_message_handler());
info.prop=prop.get();
info.refinement_bound=MAX_NB_REFINEMENT;
info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
info.ui=ui;
if(options.get_bool_option("string-max-length"))
info.string_max_length=options.get_signed_int_option("string-max-length");
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/refinement/string_refinement.h
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ Author: Alberto Griggio, [email protected]
#include <solvers/refinement/string_constraint_generator.h>
#include <solvers/refinement/string_refinement_invariant.h>

#define MAX_NB_REFINEMENT 100
#define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
#define CHARACTER_FOR_UNKNOWN '?'

struct index_set_pairt
Expand Down

0 comments on commit 1ac9abe

Please sign in to comment.