Do not use sygus-inst for internal bounded quantifiers for string reductions (#8946)

Fixes #8944.

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index fa1a6b57e3a994e09520d4694d412f5eda91ac88..a5f88dc37c1e50e28397cd3421ec6a4e25cd2599 100644 (file)
--- 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 ce49f4aff4708e7c2beeb7d64936284588b6f282..aa500578889de0f62d1d641e73933b9dc041a0f7 100644 (file)
--- 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 (file)
index 0000000..09a0d37
--- /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)