diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 664022f2e..c95a36df5 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -79,11 +79,7 @@ extern "C" { Z3_TRY; LOG_Z3_model_has_interp(c, m, a); CHECK_NON_NULL(m, 0); - if (to_model_ref(m)->has_interpretation(to_func_decl(a))) { - return true; - } else { - return false; - } + return to_model_ref(m)->has_interpretation(to_func_decl(a)); Z3_CATCH_RETURN(false); } diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index decf499a2..d307912be 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -1120,10 +1120,7 @@ namespace datalog { virtual bool operator==(const iterator_core & it) { //we worry about the equality operator only because of checking //the equality with the end() iterator - if(is_finished() && it.is_finished()) { - return true; - } - return false; + return is_finished() && it.is_finished(); } private: //private and undefined copy constructor and assignment operator @@ -1153,10 +1150,7 @@ namespace datalog { virtual bool operator==(const row_iterator_core & it) { //we worry about the equality operator only because of checking //the equality with the end() iterator - if(is_finished() && it.is_finished()) { - return true; - } - return false; + return is_finished() && it.is_finished(); } private: //private and undefined copy constructor and assignment operator