From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 21 May 2020 03:27:04 +0000 (-0500)
Subject: Throw logic exception for equality between regular expressions (#4505)
X-Git-Tag: cvc5-1.0.0~3306
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3dc56426a37bf85f82ed6dc8cf15e4eb81498110;p=cvc5.git

Throw logic exception for equality between regular expressions (#4505)

Fixes #4503.
---

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 3d898b40b..ec034b0c9 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -88,6 +88,12 @@ void TermRegistry::preRegisterTerm(TNode n)
   }
   if (k == EQUAL)
   {
+    if (n[0].getType().isRegExp())
+    {
+      std::stringstream ss;
+      ss << "Equality between regular expressions is not supported";
+      throw LogicException(ss.str());
+    }
     d_ee.addTriggerEquality(n);
     return;
   }