diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-05 19:14:01 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-05 19:14:01 -0600 |
| commit | 9e6ca7166cc2c3444429ee691f7b0c32281eddf1 (patch) | |
| tree | 8b2ff25866cc1c73b10f1872b55af91445398b03 /src/theory/sets | |
| parent | 7c86d698dad7180096ec2c81012a3ee18d2b94f9 (diff) | |
Do not combine theories if theory engine needs check (#5861)
In rare cases, theory combination would be run when theory engine still needs check. This was limited to cases where the output channel is used but no lemmas were sent (TheoryEngine::needCheck() vs. d_lemmasAdded).
This led to problems in the theory of sets, which does not run a full effort check if theory engine needs check (since it knows it will be called to check again). However, running theory combination in these cases is not safe since theory of sets computes information pertaining to the care graph during its full effort check. Running theory combination otherwise would lead to theory of sets using stale data, leading to crashes due to terms not appearing in the equality engine.
This fixes #4124 (which appears not to trigger on master anyways currently).
This bug has also appeared on my sat relevancy development branch, hence fixing on master.
Diffstat (limited to 'src/theory/sets')
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 5558b95d4..0d1206dec 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -981,7 +981,6 @@ void TheorySetsPrivate::computeCareGraph() // populate indices for (TNode f1 : it.second) { - Assert(d_equalityEngine->hasTerm(f1)); Trace("sets-cg-debug") << "...build for " << f1 << std::endl; Assert(d_equalityEngine->hasTerm(f1)); // break into index based on operator, and type of first argument (since |