summaryrefslogtreecommitdiff
path: root/src/theory/theory_id.cpp
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2021-08-16 06:58:43 -0700
committerGitHub <noreply@github.com>2021-08-16 13:58:43 +0000
commit0711ec521f01888b059d152d1c1f20382d5ce432 (patch)
tree1e797fc9c1db49571b6c7aa676b3785d5087eb73 /src/theory/theory_id.cpp
parentba2acc2d22b7718b102bfa7c2a699be5a4d87296 (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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback