diff options
Diffstat (limited to 'src/theory/strings/infer_info.cpp')
| -rw-r--r-- | src/theory/strings/infer_info.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index 432aa39d0..aabefe74e 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -17,6 +17,7 @@ #include "theory/strings/inference_manager.h" #include "theory/strings/theory_strings_utils.h" +#include "theory/theory.h" namespace cvc5 { namespace theory { @@ -60,8 +61,8 @@ bool InferInfo::isFact() const // we could process inferences with conjunctive conclusions as facts, where // the explanation is copied. However, for simplicity, we always send these // as lemmas. This case happens very infrequently. - return !atom.isConst() && atom.getKind() != kind::OR - && atom.getKind() != kind::AND && d_noExplain.empty(); + return !atom.isConst() && Theory::theoryOf(atom) == THEORY_STRINGS + && d_noExplain.empty(); } Node InferInfo::getPremises() const |