diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-08 09:15:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-08 14:15:31 +0000 |
| commit | cd8fd2e4909513b4253ce8f9aa272eb87ae6bf83 (patch) | |
| tree | 713ef362a026a676363894277219a54658a9e05e /test | |
| parent | 889daf13112f71b6f5dd98444af99ec7656195be (diff) | |
Add identifiers for sources of incompleteness (#6311)
This PR classifies all internal kinds of incompleteness as identifiers.
It makes it so TheoryEngine records an identifier when its incomplete flag is set.
The next step will be to possibly communicate this value to the user.
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/test_smt.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 9be954059..425e61bc2 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -137,7 +137,7 @@ class DummyOutputChannel : public cvc5::theory::OutputChannel } void requirePhase(TNode, bool) override {} - void setIncomplete() override {} + void setIncomplete(theory::IncompleteId id) override {} void handleUserAttribute(const char* attr, theory::Theory* t) override {} void splitLemma(TNode n, bool removable = false) override { push(LEMMA, n); } |