Throw logic exception for set.map (#8403)

Support parsing/rewriting, but not solving currently.

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 7a07ae99607626d7dee05ad3405be9114c9a54a4..099843e3c03b4c97910bc537f8b0df17bdccf9bb 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1149,6 +1149,12 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
       }
     }
     break;
+    case kind::SET_MAP:
+    {
+        throw LogicException(
+            "set.map not currently supported by the sets theory solver");
+    }
+      break;
     default: d_equalityEngine->addTerm(node); break;
   }
 }