From 83e7191449e397a53eb3a31a82d4c2bcd66fce86 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Wed, 15 Nov 2017 17:41:21 +0100 Subject: [PATCH] don't count bool sort equality as interpreted --- Kernel/Theory.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Kernel/Theory.cpp b/Kernel/Theory.cpp index d8e586e862..832661f0b8 100644 --- a/Kernel/Theory.cpp +++ b/Kernel/Theory.cpp @@ -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());