From ef9b1b979528ce5ae1fb005c87a31220cef73b8f Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 8 Jul 2022 15:07:52 -0500
Subject: [PATCH] Do not use sygus-inst for internal bounded quantifiers for
 string reductions (#8946)

Fixes #8944.
---
 src/theory/quantifiers/sygus_inst.cpp            |  9 +++++++++
 test/regress/cli/CMakeLists.txt                  |  1 +
 .../regress1/strings/issue8944-sygus-inst.smt2   | 16 ++++++++++++++++
 3 files changed, 26 insertions(+)
 create mode 100644 test/regress/cli/regress1/strings/issue8944-sygus-inst.smt2

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index fa1a6b57e..a5f88dc37 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -358,6 +358,11 @@ void SygusInst::registerQuantifier(Node q)
 {
   Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
 
+  if (!shouldProcess(q))
+  {
+    return;
+  }
+
   Trace("sygus-inst") << "Register " << q << std::endl;
 
   std::map<TypeNode, std::unordered_set<Node>> extra_cons;
@@ -463,6 +468,10 @@ void SygusInst::registerQuantifier(Node q)
  */
 void SygusInst::preRegisterQuantifier(Node q)
 {
+  if (!shouldProcess(q))
+  {
+    return;
+  }
   Trace("sygus-inst") << "preRegister " << q << std::endl;
   addCeLemma(q);
 }
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index ce49f4aff..aa5005788 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2651,6 +2651,7 @@ set(regress_1_tests
   regress1/strings/issue8916-str-unit-pairs.smt2
   regress1/strings/issue8918-str-nth-crange-red.smt2
   regress1/strings/issue8932-cmi-unit.smt2
+  regress1/strings/issue8944-sygus-inst.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
diff --git a/test/regress/cli/regress1/strings/issue8944-sygus-inst.smt2 b/test/regress/cli/regress1/strings/issue8944-sygus-inst.smt2
new file mode 100644
index 000000000..09a0d3752
--- /dev/null
+++ b/test/regress/cli/regress1/strings/issue8944-sygus-inst.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --sygus-inst
+; EXPECT: sat
+(set-logic QF_SLIA)
+(declare-fun s () String)
+(declare-fun y () Int)
+(assert (<= y 1))
+(assert (distinct 1 (str.len (str.substr s 2 2))))
+(assert (= 1 (str.len (str.substr s 1 1))))
+(assert (= 1 (str.len (str.substr s 0 1))))
+(assert (> (- (str.len s) 4) 0))
+(assert (= "0" (str.at (str.substr s 3 (- (str.len s) 3)) 0)))
+(assert (distinct 1 (str.len (str.substr s 3 (- (str.len s) 3)))))
+(assert (str.in_re s (re.+ (re.range "0" "9"))))
+(assert (not (str.is_digit (str.rev (str.replace_all (str.from_code y) "9" s)))))
+(assert (= "0" (str.substr s 2 1)))
+(check-sat)
-- 
2.30.2