diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-08-16 06:58:43 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-08-16 13:58:43 +0000 |
commit | 0711ec521f01888b059d152d1c1f20382d5ce432 (patch) | |
tree | 1e797fc9c1db49571b6c7aa676b3785d5087eb73 /src/theory/theory_id.cpp | |
parent | ba2acc2d22b7718b102bfa7c2a699be5a4d87296 (diff) |
[Strings] Make fact detection more robust (#7007)
Currently, our check for whether an inference is a fact or a lemma
involves checking whether the kind of the conclusion is a conjunction or
a disjunction. However, this does not take into account inferences of
other kinds such as ites, which is a problem because they require a
decision from the SAT solver. This commit changes the condition to check
the theory of the conclusion. If the conclusion belongs to the theory of
strings, it considers it as a fact.
Diffstat (limited to 'src/theory/theory_id.cpp')
0 files changed, 0 insertions, 0 deletions