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 3922525f26a24d1db0bb741a4abeb8d8477b87a7..5f659e7e643739bb2d3bfe3a8a43ea6f07fe5bd3 100644 (file)
--- 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 f9fc93e58e075d52367f3ee6422212b5b9d1f0a3..3bc0ff9a931f0e13bc573b970e248c4ec594af34 100644 (file)
--- 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 (file)
index 0000000..035ef3f
--- /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)