From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 29 Jul 2021 16:11:05 +0000 (-0500)
Subject: Integrate central equality engine approach into theory engine, add option and regress... 
X-Git-Tag: cvc5-1.0.0~1430
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b685ed411b6814f0810ce8f61d07aa49bd75ea3b;p=cvc5.git

Integrate central equality engine approach into theory engine, add option and regressions (#6943)

This commit makes TheoryEngine take into account whether theories are using the central equality engine.

With this commit, the central equality engine can now be optionally enabled via `--ee-mode=central`.
---

diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml
index f47907683..87869beb3 100644
--- a/src/options/theory_options.toml
+++ b/src/options/theory_options.toml
@@ -51,6 +51,9 @@ name   = "Theory Layer"
 [[option.mode.DISTRIBUTED]]
   name = "distributed"
   help = "Each theory maintains its own equality engine."
+[[option.mode.CENTRAL]]
+  name = "central"
+  help = "All applicable theories use the central equality engine."
 
 [[option]]
   name       = "tcMode"
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index e12d3eb1d..c7a2c8916 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -970,6 +970,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // set up of central equality engine
+  if (opts.theory.eeMode == options::EqEngineMode::CENTRAL)
+  {
+    if (!opts.arith.arithEqSolverWasSetByUser)
+    {
+      // use the arithmetic equality solver by default
+      opts.arith.arithEqSolver = true;
+    }
+  }
   if (opts.arith.arithEqSolver)
   {
     if (!opts.arith.arithCongManWasSetByUser)
diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index da7f0a548..609f8d9d6 100644
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -18,10 +18,10 @@
 #include "expr/node_visitor.h"
 #include "proof/eager_proof_generator.h"
 #include "theory/care_graph.h"
+#include "theory/ee_manager_central.h"
 #include "theory/ee_manager_distributed.h"
 #include "theory/model_manager.h"
 #include "theory/model_manager_distributed.h"
-#include "theory/shared_solver.h"
 #include "theory/shared_solver_distributed.h"
 #include "theory/theory_engine.h"
 
@@ -56,6 +56,18 @@ CombinationEngine::CombinationEngine(TheoryEngine& te,
     d_mmanager.reset(
         new ModelManagerDistributed(d_te, d_env, *d_eemanager.get()));
   }
+  else if (options::eeMode() == options::EqEngineMode::CENTRAL)
+  {
+    // for now, the shared solver is the same in both approaches; use the
+    // distributed one for now
+    d_sharedSolver.reset(new SharedSolverDistributed(d_te, d_pnm));
+    // make the central equality engine manager
+    d_eemanager.reset(
+        new EqEngineManagerCentral(d_te, *d_sharedSolver.get(), d_pnm));
+    // make the distributed model manager
+    d_mmanager.reset(
+        new ModelManagerDistributed(d_te, d_env, *d_eemanager.get()));
+  }
   else
   {
     Unhandled() << "CombinationEngine::finishInit: equality engine mode "
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 891a3ca08..07920ecc6 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -22,6 +22,8 @@
 
 #include "base/check.h"
 #include "expr/node_algorithm.h"
+#include "options/arith_options.h"
+#include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "smt/smt_statistics_registry.h"
@@ -368,7 +370,7 @@ std::unordered_set<TNode> Theory::currentlySharedTerms() const
 bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet)
 {
   // if we are using an equality engine, assert it to the model
-  if (d_equalityEngine != nullptr)
+  if (d_equalityEngine != nullptr && !termSet.empty())
   {
     Trace("model-builder") << "Assert Equality engine for " << d_id
                            << std::endl;
@@ -613,10 +615,24 @@ bool Theory::usesCentralEqualityEngine(TheoryId id)
   {
     return false;
   }
-  // Below are all theories with an equality engine except id ==THEORY_ARITH
+  if (id == THEORY_ARITH)
+  {
+    // conditional on whether we are using the equality solver
+    return options::arithEqSolver();
+  }
+  if (id == THEORY_BV)
+  {
+    // the internal bitblast BV solver doesnt use an equality engine
+    return options::bvSolver() != options::BVSolver::BITBLAST_INTERNAL;
+  }
   return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS
          || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS
-         || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV;
+         || id == THEORY_SEP || id == THEORY_ARRAYS;
+}
+
+bool Theory::expUsingCentralEqualityEngine(TheoryId id)
+{
+  return id != THEORY_ARITH && usesCentralEqualityEngine(id);
 }
 
 }  // namespace theory
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 7149d8e3f..41f35601b 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -877,10 +877,12 @@ class Theory {
    */
   virtual std::pair<bool, Node> entailmentCheck(TNode lit);
 
-  /** uses central equality engine */
+  /** Return true if this theory uses central equality engine */
   bool usesCentralEqualityEngine() const;
   /** uses central equality engine (static) */
   static bool usesCentralEqualityEngine(TheoryId id);
+  /** Explains/propagates via central equality engine only */
+  static bool expUsingCentralEqualityEngine(TheoryId id);
 };/* class Theory */
 
 std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 58014b06b..63fd6d9b7 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -909,13 +909,16 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
     return;
   }
 
-  // If sending to the shared terms database, it's also simple
+  // determine the actual theory that will process/explain the fact, which is
+  // THEORY_BUILTIN if the theory uses the central equality engine
+  TheoryId toTheoryIdProp = (Theory::expUsingCentralEqualityEngine(toTheoryId))
+                                ? THEORY_BUILTIN
+                                : toTheoryId;
+  // If sending to the shared solver, it's also simple
   if (toTheoryId == THEORY_BUILTIN) {
-    Assert(assertion.getKind() == kind::EQUAL
-           || (assertion.getKind() == kind::NOT
-               && assertion[0].getKind() == kind::EQUAL))
-        << "atom should be an EQUALity, not `" << assertion << "'";
-    if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
+    if (markPropagation(
+            assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
+    {
       // assert to the shared solver
       bool polarity = assertion.getKind() != kind::NOT;
       TNode atom = polarity ? assertion : assertion[0];
@@ -928,7 +931,9 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
   // directly to the apropriate theory
   if (fromTheoryId == THEORY_SAT_SOLVER) {
     // We know that this is normalized, so just send it off to the theory
-    if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
+    if (markPropagation(
+            assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
+    {
       // Is it preregistered
       bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
       // We assert it
@@ -942,6 +947,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
   // Propagations to the SAT solver are just enqueued for pickup by
   // the SAT solver later
   if (toTheoryId == THEORY_SAT_SOLVER) {
+    Assert(toTheoryIdProp == toTheoryId);
     if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
       // Enqueue for propagation to the SAT solver
       d_propagatedLiterals.push_back(assertion);
@@ -971,7 +977,11 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
   if (normalizedLiteral.isConst()) {
     if (!normalizedLiteral.getConst<bool>()) {
       // Mark the propagation for explanations
-      if (markPropagation(normalizedLiteral, originalAssertion, toTheoryId, fromTheoryId)) {
+      if (markPropagation(normalizedLiteral,
+                          originalAssertion,
+                          toTheoryIdProp,
+                          fromTheoryId))
+      {
         // special case, trust node has no proof generator
         TrustNode trnn = TrustNode::mkTrustConflict(normalizedLiteral);
         // Get the explanation (conflict will figure out where it came from)
@@ -984,7 +994,9 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
   }
 
   // Try and assert (note that we assert the non-normalized one)
-  if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
+  if (markPropagation(
+          assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
+  {
     // Check if has been pre-registered with the theory
     bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
     // Assert away
@@ -1509,6 +1521,12 @@ TrustNode TheoryEngine::getExplanation(
 {
   Assert(explanationVector.size() == 1);
   Node conclusion = explanationVector[0].d_node;
+  // if the theory explains using the central equality engine, we always start
+  // with THEORY_BUILTIN.
+  if (Theory::expUsingCentralEqualityEngine(explanationVector[0].d_theory))
+  {
+    explanationVector[0].d_theory = THEORY_BUILTIN;
+  }
   std::shared_ptr<LazyCDProof> lcp;
   if (isProofEnabled())
   {
@@ -1668,7 +1686,9 @@ TrustNode TheoryEngine::getExplanation(
         << "TheoryEngine::explain(): got explanation " << explanation
         << " got from " << toExplain.d_theory << endl;
     Assert(explanation != toExplain.d_node)
-        << "wasn't sent to you, so why are you explaining it trivially";
+        << "wasn't sent to you, so why are you explaining it trivially, for "
+           "fact "
+        << explanation;
     // Mark the explanation
     NodeTheoryPair newExplain(
         explanation, toExplain.d_theory, toExplain.d_timestamp);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 151e01088..902037088 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -120,6 +120,7 @@ set(regress_0_tests
   regress0/aufbv/bug493.smtv1.smt2
   regress0/aufbv/bug509.smtv1.smt2
   regress0/aufbv/bug580.delta.smt2
+  regress0/aufbv/cee-small-shared-eq.smt2
   regress0/aufbv/diseqprop.01.smtv1.smt2
   regress0/aufbv/dubreva005ue.delta01.smtv1.smt2
   regress0/aufbv/fifo32bc06k08.delta01.smtv1.smt2
@@ -468,6 +469,7 @@ set(regress_0_tests
   regress0/datatypes/bug597-rbt.smt2
   regress0/datatypes/bug604.smt2
   regress0/datatypes/bug625.smt2
+  regress0/datatypes/canExp-dtPendingMerge.smt2
   regress0/datatypes/cdt-model-cade15.smt2
   regress0/datatypes/cdt-non-canon-stream.smt2
   regress0/datatypes/coda_simp_model.smt2
@@ -1084,6 +1086,7 @@ set(regress_0_tests
   regress0/sets/pre-proc-univ.smt2
   regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
   regress0/sets/setel-eq.smt2
+  regress0/sets/sets-deq-dd.smt2
   regress0/sets/sets-equal.smt2
   regress0/sets/sets-extr.smt2
   regress0/sets/sets-inter.smt2
@@ -1542,10 +1545,12 @@ set(regress_1_tests
   regress1/bv/test-bv-abstraction.smt2
   regress1/bv/unsound1.smt2
   regress1/bvdiv2.smt2
+  regress1/cee-bug0909-dd-scope.smt2
   regress1/constarr3.cvc
   regress1/constarr3.smt2
   regress1/cores/issue5604.smt2
   regress1/datatypes/acyclicity-sr-ground096.smt2
+  regress1/datatypes/cee-prs-small-dd2.smt2
   regress1/datatypes/dt-color-2.6.smt2
   regress1/datatypes/dt-param-card4-unsat.smt2
   regress1/datatypes/error.cvc
@@ -1734,6 +1739,7 @@ set(regress_1_tests
   regress1/push-pop/arith_lra_02.smt2
   regress1/push-pop/bug-fmf-fun-skolem.smt2
   regress1/push-pop/bug216.smt2
+  regress1/push-pop/cee-prs-small.smt2
   regress1/push-pop/fuzz_1.smt2
   regress1/push-pop/fuzz_10.smt2
   regress1/push-pop/fuzz_11.smt2
@@ -1813,6 +1819,8 @@ set(regress_1_tests
   regress1/quantifiers/burns13.smt2
   regress1/quantifiers/burns4.smt2
   regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
+  regress1/quantifiers/cee-npnt-dd.smt2
+  regress1/quantifiers/cee-os-delta.smt2
   regress1/quantifiers/cdt-0208-to.smt2
   regress1/quantifiers/const.cvc
   regress1/quantifiers/constfunc.cvc
@@ -2088,6 +2096,7 @@ set(regress_1_tests
   regress1/strings/bug686dd.smt2
   regress1/strings/bug768.smt2
   regress1/strings/bug799-min.smt2
+  regress1/strings/cee-norn-aes-trivially.smt2 
   regress1/strings/chapman150408.smt2
   regress1/strings/cmu-2db2-extf-reg.smt2
   regress1/strings/cmu-5042-0707-2.smt2
@@ -2482,6 +2491,7 @@ set(regress_2_tests
   regress2/piVC_5581bd.smt2
   regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
   regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
+  regress2/quantifiers/cee-event-wrong-sat.smt2
   regress2/quantifiers/gn-wrong-091018.smt2
   regress2/quantifiers/issue3481-unsat1.smt2
   regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2
@@ -2722,6 +2732,7 @@ set(regression_disabled_tests
   # previously sygus inference did not apply, now (correctly) times out
   regress1/sygus/issue3498.smt2
   regress2/arith/miplib-opt1217--27.smt2
+  regress2/quantifiers/exp-trivially-dd3.smt2
   regress2/nl/dumortier-050317.smt2
   # timeout on some builds after changes to justification heuristic
   regress2/nl/nt-lemmas-bad.smt2
diff --git a/test/regress/regress0/aufbv/cee-small-shared-eq.smt2 b/test/regress/regress0/aufbv/cee-small-shared-eq.smt2
new file mode 100644
index 000000000..fa91fe7de
--- /dev/null
+++ b/test/regress/regress0/aufbv/cee-small-shared-eq.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Array (_ BitVec 1) (_ BitVec 16)))
+(assert (not (= (_ bv0 16) (select a ((_ extract 14 14) (select a (_ bv0 1)))))))
+(check-sat)
diff --git a/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2 b/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2
new file mode 100644
index 000000000..d81c3723d
--- /dev/null
+++ b/test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((T 0)) (((A) (B (proj0B T) (proj1B T)) (C (proj0C T)) (D (proj0D T) ))))
+(declare-fun w () T)
+(declare-fun u () T)
+(assert (= w (B (D u) (B (D u) (C w)))))
+(check-sat)
diff --git a/test/regress/regress0/sets/sets-deq-dd.smt2 b/test/regress/regress0/sets/sets-deq-dd.smt2
new file mode 100644
index 000000000..17ca1fce2
--- /dev/null
+++ b/test/regress/regress0/sets/sets-deq-dd.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun S () (Set (_ BitVec 1)))
+(assert (not (= S (as emptyset (Set (_ BitVec 1))))))
+(check-sat)
diff --git a/test/regress/regress1/cee-bug0909-dd-scope.smt2 b/test/regress/regress1/cee-bug0909-dd-scope.smt2
new file mode 100644
index 000000000..6ce621a98
--- /dev/null
+++ b/test/regress/regress1/cee-bug0909-dd-scope.smt2
@@ -0,0 +1,23 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((x5 0)) (((x3) (x4))))
+(declare-sort x 0)
+(declare-sort x1 0)
+(declare-datatypes ((x22 0)) (((x2))))
+(declare-datatypes ((x2 0)) (((x2 (x2 x5) (x24 x5) (x25 Int) (x26 Int) (x27 Int)))))
+(declare-sort x30 0)
+(declare-sort x3 0)
+(declare-datatypes ((x4 0)) (((x44 (x43 x3)))))
+(declare-fun x46 (x3) x1)
+(declare-datatypes ((x54 0)) (((x49 (x48 x22)) (x5 (x5 x2)) (d (s x1)))))
+(declare-fun x5 (x22) x2)
+(declare-fun x67 () (Array x x54))
+(declare-fun x6 () (Array x x54))
+(declare-fun x7 () (Array x30 x4))
+(declare-fun x63 () x30)
+(declare-fun x () x)
+(assert (distinct x3 (ite (or (distinct x6 (store x67 x (d (x46 (x43 (select x7 x63)))))) (= x67 (store x67 x (x5 (x2 x4 x3 (x25 (x5 (x48 (select x67 x)))) (x26 (x5 (x48 (select x67 x)))) (x27 (x5 (x48 (select x6 x))))))))) x3 x4)))
+(check-sat)
diff --git a/test/regress/regress1/datatypes/cee-prs-small-dd2.smt2 b/test/regress/regress1/datatypes/cee-prs-small-dd2.smt2
new file mode 100644
index 000000000..fe422d9e4
--- /dev/null
+++ b/test/regress/regress1/datatypes/cee-prs-small-dd2.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((r 0)) (((R (x Int)))))
+(declare-datatype t ((M (t1 (Array Int Int)) (t2 (Array Int Int)))))
+(declare-datatypes ((q 0)) (((R (x (Array Int r)) (y t)))))
+(declare-fun z () q)
+(assert (= z (R ((as const (Array Int r)) (R 0)) (M ((as const (Array Int Int)) 1) ((as const (Array Int Int)) 0)))))
+(assert (= (x (select (x z) 0)) (select (t1 (y z)) 1)))
+(check-sat)
diff --git a/test/regress/regress1/push-pop/cee-prs-small.smt2 b/test/regress/regress1/push-pop/cee-prs-small.smt2
new file mode 100644
index 000000000..4c0b06764
--- /dev/null
+++ b/test/regress/regress1/push-pop/cee-prs-small.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: -i --ee-mode=distributed
+; COMMAND-LINE: -i --ee-mode=central
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic ALL)
+(declare-datatypes ((r 0)) (((r_ctor (x Int)))))
+(declare-datatype tup ((mkt (t1 (Array Int Int)) (t2 (Array Int Int)))))
+(declare-datatypes ((q 0)) (((R (x (Array Int r)) (y tup)))))
+(declare-fun z () q)
+(assert (not (= 1 (select (t2 (y z)) 1))))
+(assert (= z (R ((as const (Array Int r)) (r_ctor 0)) (mkt ((as const (Array Int Int)) 1) ((as const (Array Int Int)) 0)))))
+(check-sat)
+(assert (= (x (select (x z) 0)) (select (t1 (y z)) 1)))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/cee-npnt-dd.smt2 b/test/regress/regress1/quantifiers/cee-npnt-dd.smt2
new file mode 100644
index 000000000..15727589d
--- /dev/null
+++ b/test/regress/regress1/quantifiers/cee-npnt-dd.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(set-option :fmf-bound true)
+(declare-datatype N ((o) (f) (s)))
+(declare-datatype P ((P)))
+(declare-fun G (N P Int) Bool)
+(declare-datatype c ((c (_p P))))
+(declare-fun g (N Int Int) c)
+(assert (forall ((x N)) (not (G x P 0))))
+(assert (forall ((t Int)) (or (< t 0) (> t 1) (and (forall ((p P)) (or (exists ((y N)) (and (G y (_p (g y 0 0)) t)))))))))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/cee-os-delta.smt2 b/test/regress/regress1/quantifiers/cee-os-delta.smt2
new file mode 100644
index 000000000..803291aa3
--- /dev/null
+++ b/test/regress/regress1/quantifiers/cee-os-delta.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed
+; COMMAND-LINE: --full-saturate-quant --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun o (Int) Int)
+(declare-fun f (Int Int) Int)
+(assert (forall ((x Int)) (forall ((y Int)) (! (= 1 (* y (div y y))) :pattern ((f x y))))))
+(assert (= 0 (f (o 0) (o 1))))
+(check-sat)
diff --git a/test/regress/regress1/strings/cee-norn-aes-trivially.smt2 b/test/regress/regress1/strings/cee-norn-aes-trivially.smt2
new file mode 100644
index 000000000..2f8d9904d
--- /dev/null
+++ b/test/regress/regress1/strings/cee-norn-aes-trivially.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --arith-eq-solver --ee-mode=distributed
+; COMMAND-LINE: --arith-eq-solver --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun v () String)
+(assert (str.in_re (str.++ "" v) (re.* (str.to_re "z"))))
+(assert (str.in_re v (re.* (re.range "a" "u"))))
+(assert (not (str.in_re v (str.to_re ""))))
+(check-sat)
diff --git a/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2
new file mode 100644
index 000000000..c0b3aac7c
--- /dev/null
+++ b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2
@@ -0,0 +1,43 @@
+; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed
+; COMMAND-LINE: --full-saturate-quant --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((T@$TypeValue 0) (T@A 0)) (((A)) ((T))))
+(declare-datatypes ((T@$Location 0)) (((P) (G (|t# | T@$TypeValue) (|a#G| Int)))))
+(declare-sort |T@[Int]$Value| 0)
+(declare-datatypes ((T@$Value 0) (T@R 0)) (((E) ($Boolean (|b#$Boolean| Bool)) (I (|i#I| Int)) (D (|a#D| Int)) (V (|v#V| T@R))) ((R (|v#R| |T@[Int]$Value|) (|l#R| Int)))))
+(declare-sort b 0)
+(declare-sort l 0)
+(declare-datatypes ((T@M 0)) (((M (|domain#M| b) (|contents#M| l)))))
+(declare-fun $EmptyValueArray () T@R)
+(declare-fun m (T@$Value) |T@[Int]$Value|)
+(declare-fun $IsEqual_stratified (T@$Value T@$Value) Bool)
+(declare-fun sel (|T@[Int]$Value| Int) T@$Value)
+(declare-fun st (|T@[Int]$Value| Int T@$Value) |T@[Int]$Value|)
+(assert (forall ((?x0 |T@[Int]$Value|) (?x1 Int) (?x2 T@$Value)) (= ?x2 (sel (st ?x0 ?x1 ?x2) ?x1))))
+(assert (forall ((?x0 |T@[Int]$Value|) (?x1 Int) (?y1 Int) (?x2 T@$Value)) (= (sel ?x0 ?y1) (sel (st ?x0 ?x1 ?x2) ?y1))))
+(declare-fun $LibraAccount_T_type_value () T@$TypeValue)
+(declare-fun s (l T@$Location) T@$Value)
+(declare-fun $Event_EventHandleGenerator_counter () Int)
+(declare-fun $Event_EventHandleGenerator_type_value () T@$TypeValue)
+(assert (= 0 (|l#R| $EmptyValueArray)))
+(assert (forall ((v1 T@$Value) (v2 T@$Value)) (= ($IsEqual_stratified v1 v2) (or (= v1 v2) (forall ((i Int)) (or (> 0 i) (>= i (|l#R| (|v#V| v1))) ($IsEqual_stratified (sel (|v#R| (|v#V| v1)) i) (sel (|v#R| (|v#V| v2)) i))))))))
+(assert (forall ((m@@0 T@M) (a@@0 T@$Value)) (! (or (not (is-D a@@0)) (and (is-I (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| a@@0))))) $Event_EventHandleGenerator_counter)) (forall ((x@@10 Int)) (or (> x@@10 0) (= E (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $LibraAccount_T_type_value (|a#D| a@@0))))) x@@10)))))) :qid :skolemid)))
+(declare-fun |Select_[$Location]$bool| (b T@$Location) Bool)
+(declare-fun $m@@0 () T@M)
+(declare-fun $abort_flag@2 () Bool)
+(declare-fun $m@3 () T@M)
+(declare-fun mv () T@$TypeValue)
+(declare-fun inline$$MoveToRaw$0$a@0 () Int)
+(declare-fun |Store_[$Location]$bool| (b T@$Location Bool) b)
+(assert (forall ((?x0 b) (?x1 T@$Location) (?y1 T@$Location) (?x2 Bool)) (or (= ?x1 ?y1) (= (|Select_[$Location]$bool| ?x0 ?y1) (|Select_[$Location]$bool| (|Store_[$Location]$bool| ?x0 ?x1 ?x2) ?y1)))))
+(declare-fun inline$$MoveToRaw$0$l@1 () T@$Location)
+(declare-fun |Store_[$Location]$Value| (l T@$Location T@$Value) l)
+(assert (forall ((?x0 l) (?x1 T@$Location) (?x2 T@$Value)) (= ?x2 (s (|Store_[$Location]$Value| ?x0 ?x1 ?x2) ?x1))))
+(assert (forall ((?x0 l) (?x1 T@$Location) (?y1 T@$Location) (?x2 T@$Value)) (= (s ?x0 ?y1) (s (|Store_[$Location]$Value| ?x0 ?x1 ?x2) ?y1))))
+(declare-fun inline$$Event_EventHandleGenerator_pack$0$$struct@1 () T@$Value)
+(declare-fun inline$$Event_publish_generator$0$$tmp@1 () T@$Value)
+(declare-fun i () T@$Value)
+(assert (and (not $abort_flag@2) (= inline$$Event_publish_generator$0$$tmp@1 (I 0)) (|b#$Boolean| ($Boolean (forall ((addr@@9 T@$Value)) (or (is-D addr@@9) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@9))))))))))) (or (not (=> $abort_flag@2 (|b#$Boolean| ($Boolean (forall ((addr@@4 T@$Value)) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@4)))))))))))))))) (and (= inline$$Event_EventHandleGenerator_pack$0$$struct@1 (V (R (st (st (m E) 0 inline$$Event_publish_generator$0$$tmp@1) 1 i) 1))) (not (=> (= inline$$MoveToRaw$0$a@0 (|a#D| i)) (= inline$$MoveToRaw$0$l@1 (G mv inline$$MoveToRaw$0$a@0)) (or (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| i))))) (not (= $m@3 (M (|Store_[$Location]$bool| (|domain#M| $m@@0) inline$$MoveToRaw$0$l@1 true) (|Store_[$Location]$Value| (|contents#M| $m@@0) inline$$MoveToRaw$0$l@1 inline$$Event_EventHandleGenerator_pack$0$$struct@1)))) (and (|b#$Boolean| ($Boolean ($IsEqual_stratified (s (|contents#M| $m@@0) (G mv (|a#D| i))) (V (R (|v#R| (R (|v#R| $EmptyValueArray) 0)) 1))))) (or (not (|b#$Boolean| ($Boolean ($IsEqual_stratified (s (|contents#M| $m@@0) (G mv (|a#D| i))) (V (R (|v#R| (R (st (|v#R| $EmptyValueArray) (|l#R| $EmptyValueArray) (I 0)) 1)) 0)))))) (and (|b#$Boolean| ($Boolean (forall ((addr@@1 T@$Value)) (|b#$Boolean| ($Boolean (or (not (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@1)))))) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean ($IsEqual_stratified (sel (|v#R| (|v#V| (s (|contents#M| $m@3) (G mv (|a#D| addr@@1))))) $Event_EventHandleGenerator_counter) (sel (|v#R| (|v#V| (s (|contents#M| $m@@0) (G mv (|a#D| addr@@1))))) $Event_EventHandleGenerator_counter)))))))))))) (|b#$Boolean| ($Boolean (forall ((addr@@3 T@$Value)) (|b#$Boolean| ($Boolean (or (|b#$Boolean| ($Boolean ($IsEqual_stratified (I 0) (sel (|v#R| (|v#V| (s (|contents#M| $m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| addr@@3))))) $Event_EventHandleGenerator_counter)))) (not (|b#$Boolean| ($Boolean (and (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@3) (G mv (|a#D| addr@@3))))) (|b#$Boolean| ($Boolean (not (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G $LibraAccount_T_type_value (|a#D| addr@@3))))))))))))))))))))))))))))
+(check-sat)
diff --git a/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2 b/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2
new file mode 100644
index 000000000..7f2e3084f
--- /dev/null
+++ b/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2
@@ -0,0 +1,41 @@
+; COMMAND-LINE: --ee-mode=distributed --no-check-unsat-cores
+; COMMAND-LINE: --ee-mode=central --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((dA 0)) (((A))))
+(declare-datatypes ((Loc 0)) (((G (g dA) (ag Int)))))
+(declare-sort v 0)
+(declare-datatypes ((T 0) (U 0)) (((E) (I (ii Int)) (D (d Int)) (V (vv U))) ((R (rr v)))))
+(declare-sort b 0)
+(declare-sort l 0)
+(declare-datatypes ((T@M 0)) (((M (dom b) (cnt l)))))
+(declare-fun e () U)
+(declare-fun m (T) v)
+(declare-fun iseq (T T) Bool)
+(declare-fun sel (v Int) T)
+(declare-fun st (v) v)
+(declare-fun s (l Loc) T)
+(declare-fun sb (Loc) Bool)
+(declare-fun m0 () T@M)
+(declare-fun a () Bool)
+(declare-fun im () Loc)
+(declare-fun o (Loc T) l)
+(declare-fun i () T)
+(assert (forall ((?x0 v) (?x1 Int) (?x2 T)) (= ?x2 (sel (st ?x0) ?x1))))
+(assert (forall ((v1 T) (v2 T)) (= (iseq v1 v2) (forall ((i Int)) (iseq (sel (rr (vv v1)) i) (sel (rr (vv v2)) i))))))
+(assert (forall ((?x1 Loc) (?x2 T)) (= ?x2 (s (o ?x1 ?x2) ?x1))))
+(assert (and 
+(not a) 
+(forall ((?a9 T)) (or (is-D ?a9) (sb (G A (d ?a9))))) 
+(or 
+(not (=> a (forall (($a T)) (sb (G A (d $a)))))) 
+(and 
+  (not (sb (G A (d i))))
+  (= im (G A (d (I 0)))) 
+  (= m0 (M (dom m0) (o im (V (R (st (m E))))))) 
+  (iseq (s (cnt m0) (G A (d i))) (V (R (rr e)))) 
+  (or 
+    (exists ((?a1 T)) (not (iseq (sel (rr (vv (s (cnt m0) (G A (d ?a1))))) 0) (sel (rr (vv (s (cnt m0) (G A (d ?a1))))) 0)))) 
+    (forall ((?a3 T)) (sb (G A (d ?a3)))))))))
+(check-sat)