Add option --lte-partial-inst. Remove inst-closure.

1 files changed, 0 insertions, 10 deletions

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index de0f98af6..89549a71b 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -129,22 +129,12 @@ void TheoryQuantifiers::check(Effort e) {
     case kind::FORALL:
       assertUniversal( assertion );
       break;
-    case kind::INST_CLOSURE:
-      getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
-      break;
-    case kind::EQUAL:
-      //do nothing
-      break;
     case kind::NOT:
       {
         switch( assertion[0].getKind()) {
         case kind::FORALL:
           assertExistential( assertion );
           break;
-        case kind::EQUAL:
-          //do nothing
-          break;
-        case kind::INST_CLOSURE: //cannot negate inst closure
         default:
           Unhandled(assertion[0].getKind());
           break;