diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-06 07:28:59 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-06 07:28:59 -0500 |
| commit | da03399e50e33acd4d4a6534205a67d03f44f4c1 (patch) | |
| tree | 31f5fac566100968cb64267b0ce2b7ba9220fe44 /src | |
| parent | 7f0ea0fafaca1bc40dd1f6f5891526956de857b1 (diff) | |
Fix issue with lemma during equality engine iterator in sets (#6289)
Fixes #4370.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index ea7e773b7..bb4080578 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -286,6 +286,10 @@ void TheorySetsPrivate::fullEffortCheck() d_card_enabled = true; // register it with the cardinality solver d_cardSolver->registerTerm(n); + if (d_im.hasSent()) + { + break; + } // if we do not handle the kind, set incomplete Kind nk0 = n[0].getKind(); // some kinds of cardinality we cannot handle |