Skip to content

Commit

Permalink
don't count bool sort equality as interpreted
Browse files Browse the repository at this point in the history
  • Loading branch information
Martin Suda committed Nov 15, 2017
1 parent 9433a03 commit 83e7191
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Kernel/Theory.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1460,7 +1460,7 @@ bool Theory::isInterpretedPredicate(Literal* lit)

if(lit->isEquality()){
unsigned srt = SortHelper::getEqualityArgumentSort(lit);
return (srt > Sorts::SRT_DEFAULT && srt < Sorts::FIRST_USER_SORT);
return (srt == Sorts::SRT_INTEGER || srt == Sorts::SRT_RATIONAL || srt == Sorts::SRT_REAL);
}

return isInterpretedPredicate(lit->functor());
Expand Down

0 comments on commit 83e7191

Please sign in to comment.