mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Simplify some boolean returns.
This commit is contained in:
parent
e15a39f463
commit
5fa861fa95
|
@ -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);
|
||||
}
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue