Process pending inferences at the beginning of datatypes post check (#5213)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 7 Oct 2020 03:22:16 +0000 (22:22 -0500)
committerGitHub <noreply@github.com>
Wed, 7 Oct 2020 03:22:16 +0000 (22:22 -0500)
commit0c540b4b96a100ba1d280c700c6c360efeb24fc2
tree7785784ed5ddb2b07a8e1fc8556695f365c86d2b
parent5aa526ab1df69783d17750bfce8819a6e358e157
Process pending inferences at the beginning of datatypes post check (#5213)

This fixes a potential crash in datatypes where a pending inference is not processed on a call to Theory::check. This ensures the pending set of inferences in datatypes is empty after each check. This also ensures the pending vectors are cleared before each check in datatypes.
src/theory/datatypes/inference_manager.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/inference_manager_buffered.cpp
src/theory/inference_manager_buffered.h