diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-15 11:44:15 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-15 11:44:15 -0500 |
| commit | b3f716fc402e2508a2ae1183fcfebebd2c95d6a3 (patch) | |
| tree | e4b45bf7590bd005b85608498a54e866ef581d68 /src/smt/term_formula_removal.h | |
| parent | 213433866fd07e94d40909484ef1e906722cd0c7 (diff) | |
Fix bug 806. Minor fixes to remove term formula pass.
Diffstat (limited to 'src/smt/term_formula_removal.h')
| -rw-r--r-- | src/smt/term_formula_removal.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 09991c571..9c96bbf15 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -40,6 +40,8 @@ class RemoveTermFormulas { ITECache d_iteCache; static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); } + + static bool hasNestedTermChildren( TNode node ); public: RemoveTermFormulas(context::UserContext* u); |