Fix quantifiers scope issue in strings preprocessor (#5491)

Leads to free variables in assertions when using `str.<=` whose reduction uses EXISTS not FORALL.

Fixes #5483.

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 81ec79327a3aa2e1751396439c7e94ba18610131..87ab533f41b77e4e118f002ae995761c60103196 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -965,7 +965,9 @@ Node StringsPreprocess::simplifyRec(Node t,
     Node retNode = t;
     if( t.getNumChildren()==0 ){
       retNode = simplify(t, asserts);
-    }else if( t.getKind()!=kind::FORALL ){
+    }
+    else if (!t.isClosure())
+    {
       bool changed = false;
       std::vector< Node > cc;
       if( t.getMetaKind() == kind::metakind::PARAMETERIZED ){

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index af238db1839bfa9749d008e8c6f00fb79c67e849..1bf6c63f06f27b54256f7510dedc0d5f45766074 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1862,6 +1862,7 @@ set(regress_1_tests
   regress1/strings/issue5330.smt2
   regress1/strings/issue5330_2.smt2
   regress1/strings/issue5374-proxy-i.smt2
+  regress1/strings/issue5483-pp-leq.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress1/strings/issue5483-pp-leq.smt2 b/test/regress/regress1/strings/issue5483-pp-leq.smt2
new file mode 100644 (file)
index 0000000..9e9900b
--- /dev/null
+++ b/test/regress/regress1/strings/issue5483-pp-leq.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+(set-logic QF_SLIA)
+(declare-fun _substvar_21_ () String)
+(declare-fun _substvar_29_ () String)
+(set-option :strings-lazy-pp false)
+(assert (xor true true true true (str.<= _substvar_21_ _substvar_29_) true true))
+(push 1)
+(check-sat)