diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-14 16:27:29 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-14 16:27:29 -0500 |
| commit | c84db60dabd8104928c7261c9df7bd9ef2917e9f (patch) | |
| tree | 25dfaeb4549fc995fddbc2940d94dfe5084e8860 /src/theory/quantifiers/term_util.h | |
| parent | c3f7c3c9203a355a9c45bf820e3fea0e29b439de (diff) | |
Fix relevant domain computation for nested quantifiers coming from CEGQI (#4235)
Fixes #4228. That benchmark now times out.
Diffstat (limited to 'src/theory/quantifiers/term_util.h')
| -rw-r--r-- | src/theory/quantifiers/term_util.h | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 904f301b9..315b4b1d0 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -160,8 +160,6 @@ public: std::vector<Node>& vars); public: - /** ensure type */ - static Node ensureType( Node n, TypeNode tn ); //general utilities // TODO #1216 : promote these? |