[proofs] [alethe] Remove from node converter unsupported quantifier k…

…inds
HanielB · Dec 5, 2024 · 086f694 · 086f694
1 parent 9abbc68
commit 086f694
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/src/proof/alethe/alethe_node_converter.cpp b/src/proof/alethe/alethe_node_converter.cpp
@@ -389,16 +389,13 @@ Node AletheNodeConverter::postConvert(Node n)
     case Kind::REGEXP_RV:
     /* from quantifiers */
     case Kind::EXISTS:
-    case Kind::INST_CONSTANT:
-    case Kind::ORACLE:
     case Kind::BOUND_VAR_LIST:
     case Kind::INST_PATTERN:
     case Kind::INST_NO_PATTERN:
     case Kind::INST_ATTRIBUTE:
     case Kind::INST_POOL:
     case Kind::INST_ADD_TO_POOL:
     case Kind::SKOLEM_ADD_TO_POOL:
-    case Kind::ORACLE_FORMULA_GEN:
     case Kind::INST_PATTERN_LIST:
     {
       return n;