Fix eager string preprocessing in incremental mode (#7895)

Fixes #5780.

Issue was caused by reintroducing skolems during preprocessing that were already solved for.

diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 89e40a0aa5b6ff87f3796b978fcc95393e01eccc..2924b2dc33967e1a5de0e2580ba8f884dee487a0 100644 (file)
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -147,8 +147,12 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   {
     // Simplify the literal we learned wrt previous substitutions
     Node learnedLiteral = learned_literals[i].getNode();
+    Trace("non-clausal-simplify")
+        << "Process learnedLiteral : " << learnedLiteral;
     Assert(rewrite(learnedLiteral) == learnedLiteral);
-    Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral);
+    Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral)
+        << learnedLiteral << " after subs is "
+        << top_level_substs.apply(learnedLiteral);
     // process the learned literal with substitutions and const propagations
     learnedLiteral = processLearnedLit(
         learnedLiteral, newSubstitutions.get(), constantPropagations.get());

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 329f426091f72ba110b76208684de0f8ab9fad27..90fd5847d5257e7322c96fe59158c35aa82e417e 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -229,6 +229,9 @@ bool ProcessAssertions::apply(Assertions& as)
   if (!options().strings.stringLazyPreproc)
   {
     applyPass("strings-eager-pp", as);
+    // needed since strings eager preprocessing may reintroduce skolems that
+    // were already solved for in incremental mode
+    applyPass("apply-substs", as);
   }
   if (options().smt.sortInference || options().uf.ufssFairnessMonotone)
   {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4d9d88c6bc2a880cb3052cbe455bef5ace415c93..4f79758c4f144c525acadffc3b691d7331c87bb5 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2329,6 +2329,7 @@ set(regress_1_tests
   regress1/strings/issue5610-2-infer-proxy.smt2
   regress1/strings/issue5611-deq-norm-emp.smt2
   regress1/strings/issue5692-infer-proxy.smt2
+  regress1/strings/issue5780-repeat-skolem.smt2
   regress1/strings/issue5940-skc-len-conc.smt2
   regress1/strings/issue5940-2-skc-len-conc.smt2
   regress1/strings/issue6057-replace-re.smt2

diff --git a/test/regress/regress1/strings/issue5780-repeat-skolem.smt2 b/test/regress/regress1/strings/issue5780-repeat-skolem.smt2
new file mode 100644 (file)
index 0000000..08308d4
--- /dev/null
+++ b/test/regress/regress1/strings/issue5780-repeat-skolem.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+(set-logic ALL)
+(set-option :strings-lazy-pp false)
+(set-info :status sat)
+(declare-fun s () String)
+(declare-fun t () String)
+(declare-fun r () String)
+(declare-fun u () String)
+(assert (= u (str.replace_re (str.++ t s) re.none r)))
+(push)
+(assert (= t (str.replace_re (str.++ t s) re.none r)))
+(push)
+(check-sat)