From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 14 Jan 2022 20:00:37 +0000 (-0600)
Subject: Fix learned rewrite pass for non-real equalties (#7936)
X-Git-Tag: cvc5-1.0.0~543
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c0951521904d62fab2d0a2d57d05dde8a1d23969;p=cvc5.git

Fix learned rewrite pass for non-real equalties (#7936)

Fixes #7918.
---

diff --git a/src/preprocessing/passes/learned_rewrite.cpp b/src/preprocessing/passes/learned_rewrite.cpp
index 3922525f2..5f659e7e6 100644
--- a/src/preprocessing/passes/learned_rewrite.cpp
+++ b/src/preprocessing/passes/learned_rewrite.cpp
@@ -81,7 +81,7 @@ PreprocessingPassResult LearnedRewrite::applyInternal(
       TNode atom = pol ? l : l[0];
       Kind ak = atom.getKind();
       Assert(ak != LT && ak != GT && ak != LEQ);
-      if ((ak == EQUAL && pol) || ak == GEQ)
+      if ((ak == EQUAL && pol && atom[0].getType().isRealOrInt()) || ak == GEQ)
       {
         // provide as < if negated >=
         Node atomu;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f9fc93e58..3bc0ff9a9 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2373,6 +2373,7 @@ set(regress_1_tests
   regress1/strings/issue6913.smt2
   regress1/strings/issue6973-dup-lemma-conc.smt2
   regress1/strings/issue7677-test-const-rv.smt2 
+  regress1/strings/issue7918-learned-rewrite.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
diff --git a/test/regress/regress1/strings/issue7918-learned-rewrite.smt2 b/test/regress/regress1/strings/issue7918-learned-rewrite.smt2
new file mode 100644
index 000000000..035ef3ff0
--- /dev/null
+++ b/test/regress/regress1/strings/issue7918-learned-rewrite.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --learned-rewrite
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun v () String)
+(assert (= "" (str.substr v 0 1)))
+(check-sat)