Fix cache in learned rewrite preprocessing pass (#8725)

Fixes #8722.

diff --git a/src/preprocessing/passes/learned_rewrite.cpp b/src/preprocessing/passes/learned_rewrite.cpp
index eaff69825c7fdb752e712011f295e568c04a259b..194cd7baea1b676996f8d5ec43054690db192cfa 100644 (file)
--- a/src/preprocessing/passes/learned_rewrite.cpp
+++ b/src/preprocessing/passes/learned_rewrite.cpp
@@ -88,14 +88,15 @@ PreprocessingPassResult LearnedRewrite::applyInternal(
         if (!pol)
         {
           atomu = nm->mkNode(LT, atom[0], atom[1]);
+          atomu = rewrite(atomu);
           originLit[atomu] = l;
         }
         else
         {
           atomu = l;
+          atomu = rewrite(atomu);
           originLit[l] = l;
         }
-        atomu = rewrite(atomu);
         Trace("learned-rewrite-ll")
             << "Add atom (rewritten): " << atomu << std::endl;
         binfer.add(atomu);

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 100138346b6af48ecdd39c9eaa398964d3c995c8..adc3ec611859d1901fe86ded0645024905fe38d5 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1409,6 +1409,7 @@ set(regress_0_tests
   regress0/strings/issue8346-idof-max.smt2
   regress0/strings/issue8481.smt2
   regress0/strings/issue8481-2.smt2
+  regress0/strings/issue8722-learned-rew.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2

diff --git a/test/regress/cli/regress0/strings/issue8722-learned-rew.smt2 b/test/regress/cli/regress0/strings/issue8722-learned-rew.smt2
new file mode 100644 (file)
index 0000000..ed1d730
--- /dev/null
+++ b/test/regress/cli/regress0/strings/issue8722-learned-rew.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --learned-rewrite
+; EXPECT: sat
+(set-logic ALL)
+(declare-const a String) 
+(assert (str.is_digit a)) 
+(check-sat)