diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-02-04 11:59:56 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-04 08:59:56 -0600 |
commit | 18e8b81b8eb4c4e313b03f4616271a0ea8e65e9b (patch) | |
tree | b48324201876336ec351f3128d0850160df71ff9 /src/theory/quantifiers/equality_query.cpp | |
parent | ac998a45ae64c589aeb79c5fd72234468e40451c (diff) |
[proof-new] Catch trivial cycles in SAT proof generation (#5853)
Evaluating the proof infrastructure in SMT-LIB has uncovered a rare
case (i.e., not previously in our regressions!!) in which we generate
a trivial cycle during SAT proof generation, which can lead to
problematic cycles when expanding MACRO_RESOLUTION steps. For example,
we can go from
l1 v l2 ~l1 v l3 ~l2 v l3
(ok) ------------------------------
l3
in which l3 = l1 v l2, to
l1 v l2 ~l1 v l3 ~l2 v l3
(bad) ------------------------------
l3 v l3
---------
l3
This commit now catches the trivial cycle before it's generated.
Diffstat (limited to 'src/theory/quantifiers/equality_query.cpp')
0 files changed, 0 insertions, 0 deletions