From 3f02c9363244ea92754dc72b8b7c6f5523ce0279 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 5 May 2022 13:35:31 -0500 Subject: [PATCH] Fix cache in learned rewrite preprocessing pass (#8725) Fixes #8722. --- src/preprocessing/passes/learned_rewrite.cpp | 3 ++- test/regress/cli/CMakeLists.txt | 1 + .../regress/cli/regress0/strings/issue8722-learned-rew.smt2 | 6 ++++++ 3 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 test/regress/cli/regress0/strings/issue8722-learned-rew.smt2 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) -- 2.30.2