6 files changed, 97 insertions, 2 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 3c35c2961..1e21abc47 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -702,6 +702,16 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
   // set all defaults in the quantifiers theory, which includes sygus
   setDefaultsQuantifiers(logic, opts);
 
+  // shared selectors are generally not good to combine with standard
+  // quantifier techniques e.g. E-matching
+  if (opts.datatypes.dtSharedSelectorsWasSetByUser)
+  {
+    if (logic.isQuantified() && !usesSygus(opts))
+    {
+      opts.datatypes.dtSharedSelectors = false;
+    }
+  }
+
   // until bugs 371,431 are fixed
   if (!opts.prop.minisatUseElimWasSetByUser)
   {
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index e41bef015..33d143a36 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -199,8 +199,8 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
           for (size_t i = 0, vsize = c[0].getNumChildren(); i < vsize; i++)
           {
             vars.push_back(c[0][i]);
-            Node sc = nm->mkNode(
-                APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(t, i), h);
+            Node sc =
+                nm->mkNode(APPLY_SELECTOR, dt[cindex][i].getSelector(), h);
             subs.push_back(sc);
           }
         }
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 7ba3c9758..eb8102856 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -24,6 +24,16 @@ namespace cvc5 {
 namespace theory {
 namespace datatypes {
 
+/**
+ * The rewriter for datatypes. An invariant of the rewriter is that
+ * postRewrite/preRewrite should not depend on the options, in particular,
+ * they should not depend on whether shared selectors are enabled. Thus,
+ * they should not use DTypeConstructor::getSelectorInternal. Instead,
+ * the conversion from external to internal selectors is done in
+ * expandDefinition. This invariant ensures that the rewritten form of a node
+ * does not mix multiple option settings, which would lead to e.g. shared
+ * selectors being used in an SmtEngine instance where they are disabled.
+ */
 class DatatypesRewriter : public TheoryRewriter
 {
  public:
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 80f4af984..9c43e8b51 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -228,6 +228,9 @@ bool CegSingleInv::solve()
   // solve the single invocation conjecture using a fresh copy of SMT engine
   std::unique_ptr<SmtEngine> siSmt;
   initializeSubsolver(siSmt, d_env);
+  // do not use shared selectors in subsolver, since this leads to solutions
+  // with non-user symbols
+  siSmt->setOption("dt-share-sel", "false");
   siSmt->assertFormula(siq);
   Result r = siSmt->checkSat();
   Trace("sygus-si") << "Result: " << r << std::endl;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8909bfc06..852734772 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2331,6 +2331,7 @@ set(regress_1_tests
   regress1/sygus/interpol_from_pono_2.smt2
   regress1/sygus/issue2914.sy
   regress1/sygus/issue2935.sy
+  regress1/sygus/issue3109-share-sel.sy
   regress1/sygus/issue3199.smt2
   regress1/sygus/issue3200.smt2
   regress1/sygus/issue3201.smt2
diff --git a/test/regress/regress1/sygus/issue3109-share-sel.sy b/test/regress/regress1/sygus/issue3109-share-sel.sy
new file mode 100644
index 000000000..4b08a937d
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3109-share-sel.sy
@@ -0,0 +1,71 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+
+(declare-datatypes ((IntRange 0)) 
+   (((IntRange (lower Int) (upper Int)))))
+
+(declare-datatypes ((Loc 0)) 
+   (((Loc (x Int) (y Int)))))
+
+(declare-datatypes ((LocRange 0)) 
+   (((LocRange (xD IntRange) (yD IntRange)))))
+
+(declare-datatypes ((Ship 0)) 
+   (((Ship (shipCapacity Int) (shipLoc Loc)))))
+
+(declare-datatypes ((ShipRange 0)) 
+   (((ShipRange (shipCapacityD IntRange) (shipLocD LocRange)))))
+
+(define-fun betweenInt ((x Int) (r IntRange)) Bool
+    (and (< (lower r) x) (< x (upper r)))
+)
+
+(define-fun betweenLoc ((l Loc) (lr LocRange)) Bool
+    (and (betweenInt (x l) (xD lr)) (betweenInt (y l) (yD lr)))
+)
+
+(define-fun subsetInt ((r1 IntRange) (r2 IntRange)) Bool
+    (and (>= (lower r1) (lower r2)) (<= (upper r1) (upper r2)))
+)
+
+(define-fun betweenShip ((s Ship) (sr ShipRange)) Bool
+    (and (betweenInt (shipCapacity s) (shipCapacityD sr)) (betweenLoc (shipLoc s) (shipLocD sr)))
+)
+
+(define-fun atLeast ((s Ship)) Bool
+    (> (shipCapacity s) 50)
+)
+
+(define-fun subsetLoc ((s1 LocRange) (s2 LocRange)) Bool
+    (and (subsetInt (xD s1) (xD s2)) (subsetInt (yD s1) (yD s2)))
+)
+
+(define-fun subsetShip ((s1 ShipRange) (s2 ShipRange)) Bool
+    (and (subsetInt (shipCapacityD s1) (shipCapacityD s2)) (subsetLoc (shipLocD s1) (shipLocD s2)))
+)
+
+(define-fun max ((x Int) (y Int)) Int
+ (ite (>= x y) x y)
+)
+
+(define-fun min ((x Int) (y Int)) Int
+ (ite (<= x y) x y)
+)
+
+
+(synth-fun f ((secret Ship) (prior ShipRange) (response Bool)) ShipRange
+)
+
+(declare-var secret Ship)
+(declare-var prior ShipRange)
+(declare-var response Bool)
+
+(constraint (=> (betweenShip secret prior)
+ (=> (betweenShip secret (f secret prior response)) 
+         (= response 
+            (and (atLeast secret) 
+                 (subsetShip (f secret prior response) prior))))
+))
+
+(check-synth)