From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 5 May 2022 18:35:31 +0000 (-0500)
Subject: Fix cache in learned rewrite preprocessing pass (#8725)
X-Git-Tag: cvc5-1.0.1~165
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3f02c9363244ea92754dc72b8b7c6f5523ce0279;p=cvc5.git

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 eaff69825..194cd7bae 100644
--- 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 100138346..adc3ec611 100644
--- 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
index 000000000..ed1d73035
--- /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)