diff options
Diffstat (limited to 'src/smt/process_assertions.h')
| -rw-r--r-- | src/smt/process_assertions.h | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index 072603e7d..ca834459d 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -118,22 +118,6 @@ class ProcessAssertions */ void dumpAssertions(const char* key, const preprocessing::AssertionPipeline& assertionList); - /** - * Helper function to fix up assertion list to restore invariants needed after - * ite removal. - */ - void collectSkolems(IteSkolemMap& iskMap, - TNode n, - set<TNode>& skolemSet, - NodeToBoolHashMap& cache); - /** - * Helper function to fix up assertion list to restore invariants needed after - * ite removal. - */ - bool checkForBadSkolems(IteSkolemMap& iskMap, - TNode n, - TNode skolem, - NodeToBoolHashMap& cache); }; } // namespace smt |