Merge pull request #1820 from smowton/smowton/fix/remove-string-solve…

…r-iteration-limit Remove string solver iteration limit
diffblue · Feb 14, 2018 · ef08ae2 · ef08ae2
2 parents 0f20482 + 1ac9abe
commit ef08ae2
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
@@ -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");

diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
@@ -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