diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp index b6743063401..2748119a320 100644 --- a/src/symex/path_search.cpp +++ b/src/symex/path_search.cpp @@ -281,15 +281,15 @@ bool path_searcht::drop_state(const statet &state) } // depth limit - if(depth_limit>=0 && state.get_depth()>depth_limit) + if(state.get_depth()>=depth_limit) return true; // context bound - if(context_bound>=0 && state.get_no_thread_interleavings()>context_bound) + if(state.get_no_thread_interleavings()>=context_bound) return true; // branch bound - if(branch_bound>=0 && state.get_no_branches()>branch_bound) + if(state.get_no_branches()>=branch_bound) return true; // unwinding limit -- loops @@ -298,7 +298,7 @@ bool path_searcht::drop_state(const statet &state) bool stop=false; for(const auto &loop_info : state.unwinding_map) - if(loop_info.second>unwind_limit) + if(loop_info.second>=unwind_limit) { stop=true; break; @@ -324,7 +324,7 @@ bool path_searcht::drop_state(const statet &state) bool stop=false; for(const auto &rec_info : state.recursion_map) - if(rec_info.second>unwind_limit) + if(rec_info.second>=unwind_limit) { stop=true; break; diff --git a/src/symex/path_search.h b/src/symex/path_search.h index 4823998ef8a..f02b617ee40 100644 --- a/src/symex/path_search.h +++ b/src/symex/path_search.h @@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + class path_searcht:public safety_checkert { public: @@ -26,11 +28,11 @@ class path_searcht:public safety_checkert safety_checkert(_ns), show_vcc(false), eager_infeasibility(false), - depth_limit(-1), // no limit - context_bound(-1), - branch_bound(-1), - unwind_limit(-1), - time_limit(-1), + depth_limit(std::numeric_limits::max()), + context_bound(std::numeric_limits::max()), + branch_bound(std::numeric_limits::max()), + unwind_limit(std::numeric_limits::max()), + time_limit(std::numeric_limits::max()), search_heuristic(search_heuristict::DFS) { } @@ -132,11 +134,11 @@ class path_searcht:public safety_checkert void initialize_property_map( const goto_functionst &goto_functions); - int depth_limit; - int context_bound; - int branch_bound; - int unwind_limit; - int time_limit; + unsigned depth_limit; + unsigned context_bound; + unsigned branch_bound; + unsigned unwind_limit; + unsigned time_limit; enum class search_heuristict { DFS, BFS, LOCS } search_heuristic;