From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 23 Nov 2020 01:41:23 +0000 (-0600)
Subject: Fix quantifiers scope issue in strings preprocessor (#5491)
X-Git-Tag: cvc5-1.0.0~2562
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2b4d6997eec82dce3832a449eea00f94af420f8a;p=cvc5.git

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 81ec79327..87ab533f4 100644
--- 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 af238db18..1bf6c63f0 100644
--- 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
index 000000000..9e9900b21
--- /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)