From aba70eb79f255582aa5c254518b3731f284ad0c4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 25 Mar 2022 21:51:29 -0500 Subject: [PATCH] Throw logic exception for set.map (#8403) Support parsing/rewriting, but not solving currently. --- src/theory/sets/theory_sets_private.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 7a07ae996..099843e3c 100644 --- 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; } } -- 2.30.2