Merge branch 'master' into python3.5regpython3.5reg

16 files changed, 454 insertions, 425 deletions

diff --git a/src/api/java/jni/option_Info.cpp b/src/api/java/jni/option_Info.cpp
deleted file mode 100644
index 4c6025357..000000000
--- a/src/api/java/jni/option_Info.cpp
+++ /dev/null
@@ -1,345 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Mudathir Mohamed
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * The cvc5 Java API.
- */
-
-#include "api/cpp/cvc5.h"
-#include "api_utilities.h"
-#include "io_github_cvc5_api_OptionInfo.h"
-
-using namespace cvc5::api;
-
-/*
- * Class:     io_github_cvc5_api_OptionInfo
- * Method:    deletePointer
- * Signature: (J)V
- */
-JNIEXPORT void JNICALL
-Java_io_github_cvc5_api_OptionInfo_deletePointer(JNIEnv*, jclass, jlong pointer)
-{
-  delete reinterpret_cast<OptionInfo*>(pointer);
-}
-
-/*
- * Class:     io_github_cvc5_api_OptionInfo
- * Method:    toString
- * Signature: (J)Ljava/lang/String;
- */
-JNIEXPORT jstring JNICALL
-Java_io_github_cvc5_api_OptionInfo_toString(JNIEnv* env, jobject, jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
-  std::stringstream ss;
-  ss << *current;
-  return env->NewStringUTF(ss.str().c_str());
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
-}
-
-/*
- * Class:     io_github_cvc5_api_OptionInfo
- * Method:    getName
- * Signature: (J)Ljava/lang/String;
- */
-JNIEXPORT jstring JNICALL
-Java_io_github_cvc5_api_OptionInfo_getName(JNIEnv* env, jobject, jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
-  return env->NewStringUTF(current->name.c_str());
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
-}
-
-/*
- * Class:     io_github_cvc5_api_OptionInfo
- * Method:    getAliases
- * Signature: (J)[Ljava/lang/String;
- */
-JNIEXPORT jobjectArray JNICALL Java_io_github_cvc5_api_OptionInfo_getAliases(
-    JNIEnv* env, jobject, jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
-  jobjectArray ret = getStringArrayFromStringVector(env, current->aliases);
-  return ret;
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
-}
-
-/*
- * Class:     io_github_cvc5_api_OptionInfo
- * Method:    getSetByUser
- * Signature: (J)Z
- */
-JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_OptionInfo_getSetByUser(
-    JNIEnv* env, jobject, jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
-  return static_cast<jboolean>(current->setByUser);
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
-}
-
-/**
- * Convert OptionInfo::NumberInfo cpp object to OptionInfo.NumberInfo java
- * object
- * @tparam T cpp integer types int64_t, uint64_t, etc
- * @param env jni environment
- * @param optionInfo a java object for this OptionInfo
- * @param numberInfoClass the java class for OptionInfo.NumberInfo
- * @param methodId a constructor for OptionInfo.NumberInfo
- * @param info the cpp OptionInfo::NumberInfo object
- * @return a java object of class OptionInfo.NumberInfo<BigInteger>
- */
-template <typename T>
-jobject getNumberInfoFromInteger(JNIEnv* env,
-                                 const _jobject* optionInfo,
-                                 jclass numberInfoClass,
-                                 jmethodID methodId,
-                                 const OptionInfo::NumberInfo<T>& info)
-{
-  jobject defaultValue = getBigIntegerObject<T>(env, info.defaultValue);
-  jobject currentValue = getBigIntegerObject<T>(env, info.currentValue);
-  jobject minimum = nullptr;
-  if (info.minimum)
-  {
-    minimum = getBigIntegerObject<T>(env, *info.minimum);
-  }
-  jobject maximum = nullptr;
-  if (info.maximum)
-  {
-    maximum = getBigIntegerObject<T>(env, *info.maximum);
-  }
-  jobject ret = env->NewObject(numberInfoClass,
-                               methodId,
-                               optionInfo,
-                               defaultValue,
-                               currentValue,
-                               minimum,
-                               maximum);
-
-  return ret;
-}
-
-template <typename T>
-jobject getNumberInfoFromInteger(JNIEnv* env,
-                                 const _jobject* optionInfo,
-                                 jclass numberInfoClass,
-                                 jmethodID methodId,
-                                 const OptionInfo::NumberInfo<int64_t>& info);
-
-template <typename T>
-jobject getNumberInfoFromInteger(JNIEnv* env,
-                                 const _jobject* optionInfo,
-                                 jclass numberInfoClass,
-                                 jmethodID methodId,
-                                 const OptionInfo::NumberInfo<uint64_t>& info);
-
-/*
- * Class:     io_github_cvc5_api_OptionInfo
- * Method:    getBaseInfo
- * Signature: (J)Lio/github/cvc5/api/BaseInfo;
- */
-JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_OptionInfo_getBaseInfo(
-    JNIEnv* env, jobject optionInfo, jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
-  std::variant<OptionInfo::VoidInfo,
-               OptionInfo::ValueInfo<bool>,
-               OptionInfo::ValueInfo<std::string>,
-               OptionInfo::NumberInfo<int64_t>,
-               OptionInfo::NumberInfo<uint64_t>,
-               OptionInfo::NumberInfo<double>,
-               OptionInfo::ModeInfo>
-      v = current->valueInfo;
-
-  if (std::holds_alternative<OptionInfo::VoidInfo>(v))
-  {
-    jclass voidInfoClass =
-        env->FindClass("io/github/cvc5/api/OptionInfo$VoidInfo");
-    jmethodID methodId = env->GetMethodID(
-        voidInfoClass, "<init>", "(Lio/github/cvc5/api/OptionInfo;)V");
-    jobject ret = env->NewObject(voidInfoClass, methodId, optionInfo);
-    return ret;
-  }
-
-  if (std::holds_alternative<OptionInfo::ValueInfo<bool>>(v)
-      || std::holds_alternative<OptionInfo::ValueInfo<std::string>>(v))
-  {
-    jclass valueInfoClass =
-        env->FindClass("io/github/cvc5/api/OptionInfo$ValueInfo");
-    jmethodID methodId =
-        env->GetMethodID(valueInfoClass,
-                         "<init>",
-                         "(Lio/github/cvc5/api/OptionInfo;Ljava/lang/"
-                         "Object;Ljava/lang/Object;)V");
-
-    if (std::holds_alternative<OptionInfo::ValueInfo<bool>>(v))
-    {
-      auto info = std::get<OptionInfo::ValueInfo<bool>>(v);
-      jobject currentValue = getBooleanObject(env, info.currentValue);
-      jobject defaultValue = getBooleanObject(env, info.defaultValue);
-      jobject ret = env->NewObject(
-          valueInfoClass, methodId, optionInfo, defaultValue, currentValue);
-      return ret;
-    }
-
-    if (std::holds_alternative<OptionInfo::ValueInfo<std::string>>(v))
-    {
-      auto info = std::get<OptionInfo::ValueInfo<std::string>>(v);
-      jstring defaultValue = env->NewStringUTF(info.defaultValue.c_str());
-      jstring currentValue = env->NewStringUTF(info.currentValue.c_str());
-      jobject ret = env->NewObject(
-          valueInfoClass, methodId, optionInfo, defaultValue, currentValue);
-      return ret;
-    }
-  }
-
-  if (std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(v)
-      || std::holds_alternative<OptionInfo::NumberInfo<uint64_t>>(v)
-      || std::holds_alternative<OptionInfo::NumberInfo<double>>(v))
-  {
-    jclass numberInfoClass =
-        env->FindClass("io/github/cvc5/api/OptionInfo$NumberInfo");
-    jmethodID methodId = env->GetMethodID(
-        numberInfoClass,
-        "<init>",
-        "(Lio/github/cvc5/api/OptionInfo;Ljava/lang/Object;Ljava/lang/"
-        "Object;Ljava/lang/Object;Ljava/lang/Object;)V");
-
-    if (std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(v))
-    {
-      auto info = std::get<OptionInfo::NumberInfo<int64_t>>(v);
-      return getNumberInfoFromInteger(
-          env, optionInfo, numberInfoClass, methodId, info);
-    }
-
-    if (std::holds_alternative<OptionInfo::NumberInfo<uint64_t>>(v))
-    {
-      auto info = std::get<OptionInfo::NumberInfo<uint64_t>>(v);
-      return getNumberInfoFromInteger(
-          env, optionInfo, numberInfoClass, methodId, info);
-    }
-
-    if (std::holds_alternative<OptionInfo::NumberInfo<double>>(v))
-    {
-      auto info = std::get<OptionInfo::NumberInfo<double>>(v);
-      jobject defaultValue = getDoubleObject(env, info.defaultValue);
-      jobject currentValue = getDoubleObject(env, info.currentValue);
-      jobject minimum = nullptr;
-      if (info.minimum)
-      {
-        minimum = getDoubleObject(env, *info.minimum);
-      }
-      jobject maximum = nullptr;
-      if (info.maximum)
-      {
-        maximum = getDoubleObject(env, *info.maximum);
-      }
-      jobject ret = env->NewObject(numberInfoClass,
-                                   methodId,
-                                   optionInfo,
-                                   defaultValue,
-                                   currentValue,
-                                   minimum,
-                                   maximum);
-      return ret;
-    }
-  }
-
-  if (std::holds_alternative<OptionInfo::ModeInfo>(v))
-  {
-    jclass modeInfoClass =
-        env->FindClass("io/github/cvc5/api/OptionInfo$ModeInfo");
-    jmethodID methodId = env->GetMethodID(
-        modeInfoClass,
-        "<init>",
-        "(Lio/github/cvc5/api/OptionInfo;Ljava/lang/String;Ljava/lang/"
-        "String;[Ljava/lang/String;)V");
-
-    auto info = std::get<OptionInfo::ModeInfo>(v);
-    jstring defaultValue = env->NewStringUTF(info.defaultValue.c_str());
-    jstring currentValue = env->NewStringUTF(info.currentValue.c_str());
-    jobject stringArray = getStringArrayFromStringVector(env, info.modes);
-    jobject ret = env->NewObject(modeInfoClass,
-                                 methodId,
-                                 optionInfo,
-                                 defaultValue,
-                                 currentValue,
-                                 stringArray);
-    return ret;
-  }
-
-  return nullptr;
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
-}
-
-/*
- * Class:     io_github_cvc5_api_OptionInfo
- * Method:    booleanValue
- * Signature: (J)Z
- */
-JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_OptionInfo_booleanValue(
-    JNIEnv* env, jobject, jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
-  return static_cast<jboolean>(current->boolValue());
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
-}
-
-/*
- * Class:     io_github_cvc5_api_OptionInfo
- * Method:    stringValue
- * Signature: (J)Ljava/lang/String;
- */
-JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_OptionInfo_stringValue(
-    JNIEnv* env, jobject, jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
-  std::string ret = current->stringValue();
-  return env->NewStringUTF(ret.c_str());
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
-}
-
-/*
- * Class:     io_github_cvc5_api_OptionInfo
- * Method:    intValue
- * Signature: (J)Ljava/math/BigInteger;
- */
-JNIEXPORT jobject JNICALL
-Java_io_github_cvc5_api_OptionInfo_intValue(JNIEnv* env, jobject, jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
-  std::int64_t value = current->intValue();
-  jobject ret = getBigIntegerObject<std::int64_t>(env, value);
-  return ret;
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
-}
-
-/*
- * Class:     io_github_cvc5_api_OptionInfo
- * Method:    doubleValue
- * Signature: (J)D
- */
-JNIEXPORT jdouble JNICALL Java_io_github_cvc5_api_OptionInfo_doubleValue(
-    JNIEnv* env, jobject, jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
-  double ret = current->doubleValue();
-  return static_cast<jdouble>(ret);
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jdouble>(0.0));
-}
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 28557e472..af753dd26 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -429,6 +429,8 @@ const char* toString(InferenceId i)
     case InferenceId::STRINGS_CTN_POS: return "STRINGS_CTN_POS";
     case InferenceId::STRINGS_REDUCTION: return "STRINGS_REDUCTION";
     case InferenceId::STRINGS_PREFIX_CONFLICT: return "STRINGS_PREFIX_CONFLICT";
+    case InferenceId::STRINGS_ARITH_BOUND_CONFLICT:
+      return "STRINGS_ARITH_BOUND_CONFLICT";
     case InferenceId::STRINGS_REGISTER_TERM_ATOMIC:
       return "STRINGS_REGISTER_TERM_ATOMIC";
     case InferenceId::STRINGS_REGISTER_TERM: return "STRINGS_REGISTER_TERM";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 50c063651..70f70e717 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -772,9 +772,11 @@ enum class InferenceId
   // f(x1, .., xn) and P is the reduction predicate for f
   // (see theory_strings_preprocess).
   STRINGS_REDUCTION,
-  //-------------------- prefix conflict
-  // prefix conflict (coarse-grained)
+  //-------------------- merge conflicts
+  // prefix conflict
   STRINGS_PREFIX_CONFLICT,
+  // arithmetic bound conflict
+  STRINGS_ARITH_BOUND_CONFLICT,
   //-------------------- other
   // a lemma added during term registration for an atomic term
   STRINGS_REGISTER_TERM_ATOMIC,
diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp
index 8950ea6fa..9e3d8ad38 100644
--- a/src/theory/strings/arith_entail.cpp
+++ b/src/theory/strings/arith_entail.cpp
@@ -30,7 +30,10 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-ArithEntail::ArithEntail(Rewriter* r) : d_rr(r) {}
+ArithEntail::ArithEntail(Rewriter* r) : d_rr(r)
+{
+  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+}
 
 Node ArithEntail::rewrite(Node a) { return d_rr->rewrite(a); }
 
@@ -197,7 +200,7 @@ bool ArithEntail::checkApprox(Node ar)
   }
   // get the current "fixed" sum for the abstraction of ar
   Node aar = aarSum.empty()
-                 ? nm->mkConst(Rational(0))
+                 ? d_zero
                  : (aarSum.size() == 1 ? aarSum[0] : nm->mkNode(PLUS, aarSum));
   aar = d_rr->rewrite(aar);
   Trace("strings-ent-approx-debug")
@@ -709,10 +712,61 @@ bool ArithEntail::checkWithAssumptions(std::vector<Node> assumptions,
   return res;
 }
 
+struct ArithEntailConstantBoundLowerId
+{
+};
+typedef expr::Attribute<ArithEntailConstantBoundLowerId, Node>
+    ArithEntailConstantBoundLower;
+
+struct ArithEntailConstantBoundUpperId
+{
+};
+typedef expr::Attribute<ArithEntailConstantBoundUpperId, Node>
+    ArithEntailConstantBoundUpper;
+
+void ArithEntail::setConstantBoundCache(Node n, Node ret, bool isLower)
+{
+  if (isLower)
+  {
+    ArithEntailConstantBoundLower acbl;
+    n.setAttribute(acbl, ret);
+  }
+  else
+  {
+    ArithEntailConstantBoundUpper acbu;
+    n.setAttribute(acbu, ret);
+  }
+}
+
+Node ArithEntail::getConstantBoundCache(Node n, bool isLower)
+{
+  if (isLower)
+  {
+    ArithEntailConstantBoundLower acbl;
+    if (n.hasAttribute(acbl))
+    {
+      return n.getAttribute(acbl);
+    }
+  }
+  else
+  {
+    ArithEntailConstantBoundUpper acbu;
+    if (n.hasAttribute(acbu))
+    {
+      return n.getAttribute(acbu);
+    }
+  }
+  return Node::null();
+}
+
 Node ArithEntail::getConstantBound(Node a, bool isLower)
 {
   Assert(d_rr->rewrite(a) == a);
-  Node ret;
+  Node ret = getConstantBoundCache(a, isLower);
+  if (!ret.isNull())
+  {
+    return ret;
+  }
   if (a.isConst())
   {
     ret = a;
@@ -721,7 +775,7 @@ Node ArithEntail::getConstantBound(Node a, bool isLower)
   {
     if (isLower)
     {
-      ret = NodeManager::currentNM()->mkConst(Rational(0));
+      ret = d_zero;
     }
   }
   else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT)
@@ -767,7 +821,7 @@ Node ArithEntail::getConstantBound(Node a, bool isLower)
     {
       if (children.empty())
       {
-        ret = NodeManager::currentNM()->mkConst(Rational(0));
+        ret = d_zero;
       }
       else if (children.size() == 1)
       {
@@ -789,6 +843,55 @@ Node ArithEntail::getConstantBound(Node a, bool isLower)
          || check(a, false));
   Assert(!isLower || ret.isNull() || ret.getConst<Rational>().sgn() <= 0
          || check(a, true));
+  // cache
+  setConstantBoundCache(a, ret, isLower);
+  return ret;
+}
+
+Node ArithEntail::getConstantBoundLength(Node s, bool isLower)
+{
+  Assert(s.getType().isStringLike());
+  Node ret = getConstantBoundCache(s, isLower);
+  if (!ret.isNull())
+  {
+    return ret;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  if (s.isConst())
+  {
+    ret = nm->mkConst(Rational(Word::getLength(s)));
+  }
+  else if (s.getKind() == STRING_CONCAT)
+  {
+    Rational sum(0);
+    bool success = true;
+    for (const Node& sc : s)
+    {
+      Node b = getConstantBoundLength(sc, isLower);
+      if (b.isNull())
+      {
+        if (isLower)
+        {
+          // assume zero and continue
+          continue;
+        }
+        success = false;
+        break;
+      }
+      Assert(b.getKind() == CONST_RATIONAL);
+      sum = sum + b.getConst<Rational>();
+    }
+    if (success)
+    {
+      ret = nm->mkConst(sum);
+    }
+  }
+  else if (isLower)
+  {
+    ret = d_zero;
+  }
+  // cache
+  setConstantBoundCache(s, ret, isLower);
   return ret;
 }
 
@@ -853,7 +956,7 @@ bool ArithEntail::inferZerosInSumGeq(Node x,
     }
     else
     {
-      sum = ys.size() == 1 ? ys[0] : nm->mkConst(Rational(0));
+      sum = ys.size() == 1 ? ys[0] : d_zero;
     }
 
     if (check(sum, x))
diff --git a/src/theory/strings/arith_entail.h b/src/theory/strings/arith_entail.h
index 2158b23b0..295afb8c9 100644
--- a/src/theory/strings/arith_entail.h
+++ b/src/theory/strings/arith_entail.h
@@ -136,6 +136,10 @@ class ArithEntail
   Node getConstantBound(Node a, bool isLower = true);
 
   /**
+   * get constant bound on the length of s.
+   */
+  Node getConstantBoundLength(Node s, bool isLower = true);
+  /**
    * Given an inequality y1 + ... + yn >= x, removes operands yi s.t. the
    * original inequality still holds. Returns true if the original inequality
    * holds and false otherwise. The list of ys is modified to contain a subset
@@ -179,8 +183,14 @@ class ArithEntail
   void getArithApproximations(Node a,
                               std::vector<Node>& approx,
                               bool isOverApprox = false);
+  /** Set bound cache */
+  void setConstantBoundCache(Node n, Node ret, bool isLower);
+  /** Get bound cache */
+  Node getConstantBoundCache(Node n, bool isLower);
   /** The underlying rewriter */
   Rewriter* d_rr;
+  /** Constant zero */
+  Node d_zero;
 };
 
 }  // namespace strings
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index d4d3761d8..b5e15a129 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -2550,6 +2550,7 @@ void CoreSolver::checkNormalFormsDeq()
   
   const context::CDList<Node>& deqs = d_state.getDisequalityList();
 
+  NodeManager* nm = NodeManager::currentNM();
   //for each pair of disequal strings, must determine whether their lengths are equal or disequal
   for (const Node& eq : deqs)
   {
@@ -2564,9 +2565,8 @@ void CoreSolver::checkNormalFormsDeq()
         EqcInfo* ei = d_state.getOrMakeEqcInfo(n[i], false);
         lt[i] = ei ? ei->d_lengthTerm : Node::null();
         if( lt[i].isNull() ){
-          lt[i] = eq[i];
+          lt[i] = nm->mkNode(STRING_LENGTH, eq[i]);
         }
-        lt[i] = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt[i] );
       }
       if (!d_state.areEqual(lt[0], lt[1]) && !d_state.areDisequal(lt[0], lt[1]))
       {
@@ -2642,14 +2642,13 @@ void CoreSolver::checkLengthsEqc() {
         << "Process length constraints for " << d_strings_eqc[i] << std::endl;
     // check if there is a length term for this equivalence class
     EqcInfo* ei = d_state.getOrMakeEqcInfo(d_strings_eqc[i], false);
-    Node lt = ei ? ei->d_lengthTerm : Node::null();
-    if (lt.isNull())
+    Node llt = ei ? ei->d_lengthTerm : Node::null();
+    if (llt.isNull())
     {
       Trace("strings-process-debug")
           << "No length term for eqc " << d_strings_eqc[i] << std::endl;
       continue;
     }
-    Node llt = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, lt);
     // now, check if length normalization has occurred
     if (ei->d_normalizedLength.get().isNull())
     {
@@ -2669,7 +2668,7 @@ void CoreSolver::checkLengthsEqc() {
       // if not, add the lemma
       std::vector<Node> ant;
       ant.insert(ant.end(), nfi.d_exp.begin(), nfi.d_exp.end());
-      ant.push_back(lt.eqNode(nfi.d_base));
+      ant.push_back(llt[0].eqNode(nfi.d_base));
       Node lc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, nf);
       Node lcr = rewrite(lc);
       Trace("strings-process-debug")
diff --git a/src/theory/strings/eager_solver.cpp b/src/theory/strings/eager_solver.cpp
index 829146f52..21fdd6fa2 100644
--- a/src/theory/strings/eager_solver.cpp
+++ b/src/theory/strings/eager_solver.cpp
@@ -16,6 +16,7 @@
 #include "theory/strings/eager_solver.h"
 
 #include "theory/strings/theory_strings_utils.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;
 
@@ -23,7 +24,13 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-EagerSolver::EagerSolver(SolverState& state) : d_state(state) {}
+EagerSolver::EagerSolver(Env& env,
+                         SolverState& state,
+                         TermRegistry& treg,
+                         ArithEntail& aent)
+    : EnvObj(env), d_state(state), d_treg(treg), d_aent(aent)
+{
+}
 
 EagerSolver::~EagerSolver() {}
 
@@ -37,7 +44,30 @@ void EagerSolver::eqNotifyNewClass(TNode t)
     EqcInfo* ei = d_state.getOrMakeEqcInfo(r);
     if (k == STRING_LENGTH)
     {
-      ei->d_lengthTerm = t[0];
+      ei->d_lengthTerm = t;
+      // also assume it as upper/lower bound as applicable for the equivalence
+      // class info of t.
+      EqcInfo* eil = nullptr;
+      for (size_t i = 0; i < 2; i++)
+      {
+        Node b = getBoundForLength(t, i == 0);
+        if (b.isNull())
+        {
+          continue;
+        }
+        if (eil == nullptr)
+        {
+          eil = d_state.getOrMakeEqcInfo(t);
+        }
+        if (i == 0)
+        {
+          eil->d_firstBound = t;
+        }
+        else if (i == 1)
+        {
+          eil->d_secondBound = t;
+        }
+      }
     }
     else
     {
@@ -46,11 +76,12 @@ void EagerSolver::eqNotifyNewClass(TNode t)
   }
   else if (t.isConst())
   {
-    if (t.getType().isStringLike())
+    TypeNode tn = t.getType();
+    if (tn.isStringLike() || tn.isInteger())
     {
       EqcInfo* ei = d_state.getOrMakeEqcInfo(t);
-      ei->d_prefixC = t;
-      ei->d_suffixC = t;
+      ei->d_firstBound = t;
+      ei->d_secondBound = t;
     }
   }
   else if (k == STRING_CONCAT)
@@ -66,8 +97,18 @@ void EagerSolver::eqNotifyMerge(TNode t1, TNode t2)
   {
     return;
   }
-  Assert(t1.getType().isStringLike());
+  // always create it if e2 was non-null
   EqcInfo* e1 = d_state.getOrMakeEqcInfo(t1);
+  // check for conflict
+  Node conf = checkForMergeConflict(t1, t2, e1, e2);
+  if (!conf.isNull())
+  {
+    InferenceId id = t1.getType().isStringLike()
+                         ? InferenceId::STRINGS_PREFIX_CONFLICT
+                         : InferenceId::STRINGS_ARITH_BOUND_CONFLICT;
+    d_state.setPendingMergeConflict(conf, id);
+    return;
+  }
   // add information from e2 to e1
   if (!e2->d_lengthTerm.get().isNull())
   {
@@ -77,16 +118,6 @@ void EagerSolver::eqNotifyMerge(TNode t1, TNode t2)
   {
     e1->d_codeTerm.set(e2->d_codeTerm);
   }
-  if (!e2->d_prefixC.get().isNull())
-  {
-    d_state.setPendingPrefixConflictWhen(
-        e1->addEndpointConst(e2->d_prefixC, Node::null(), false));
-  }
-  if (!e2->d_suffixC.get().isNull())
-  {
-    d_state.setPendingPrefixConflictWhen(
-        e1->addEndpointConst(e2->d_suffixC, Node::null(), true));
-  }
   if (e2->d_cardinalityLemK.get() > e1->d_cardinalityLemK.get())
   {
     e1->d_cardinalityLemK.set(e2->d_cardinalityLemK);
@@ -126,9 +157,50 @@ void EagerSolver::addEndpointsToEqcInfo(Node t, Node concat, Node eqc)
       Trace("strings-eager-pconf-debug")
           << "New term: " << concat << " for " << t << " with prefix " << c
           << " (" << (r == 1) << ")" << std::endl;
-      d_state.setPendingPrefixConflictWhen(ei->addEndpointConst(t, c, r == 1));
+      Node conf = ei->addEndpointConst(t, c, r == 1);
+      if (!conf.isNull())
+      {
+        d_state.setPendingMergeConflict(conf,
+                                        InferenceId::STRINGS_PREFIX_CONFLICT);
+        return;
+      }
+    }
+  }
+}
+
+Node EagerSolver::checkForMergeConflict(Node a,
+                                        Node b,
+                                        EqcInfo* ea,
+                                        EqcInfo* eb)
+{
+  Assert(eb != nullptr && ea != nullptr);
+  Assert(a.getType() == b.getType());
+  Assert(a.getType().isStringLike() || a.getType().isInteger());
+  // check prefix, suffix
+  for (size_t i = 0; i < 2; i++)
+  {
+    Node n = i == 0 ? eb->d_firstBound.get() : eb->d_secondBound.get();
+    if (!n.isNull())
+    {
+      Node conf;
+      if (a.getType().isStringLike())
+      {
+        conf = ea->addEndpointConst(n, Node::null(), i == 1);
+      }
+      else
+      {
+        Trace("strings-eager-aconf-debug")
+            << "addArithmeticBound " << n << " into " << a << " from " << b
+            << std::endl;
+        conf = addArithmeticBound(ea, n, i == 0);
+      }
+      if (!conf.isNull())
+      {
+        return conf;
+      }
     }
   }
+  return Node::null();
 }
 
 void EagerSolver::notifyFact(TNode atom,
@@ -147,6 +219,75 @@ void EagerSolver::notifyFact(TNode atom,
   }
 }
 
+Node EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower)
+{
+  Assert(e != nullptr);
+  Assert(!t.isNull());
+  Node tb = t.isConst() ? t : getBoundForLength(t, isLower);
+  Assert(!tb.isNull() && tb.getKind() == CONST_RATIONAL)
+      << "Unexpected bound " << tb << " from " << t;
+  Rational br = tb.getConst<Rational>();
+  Node prev = isLower ? e->d_firstBound : e->d_secondBound;
+  // check if subsumed
+  if (!prev.isNull())
+  {
+    // convert to bound
+    Node prevb = prev.isConst() ? prev : getBoundForLength(prev, isLower);
+    Assert(!prevb.isNull() && prevb.getKind() == CONST_RATIONAL);
+    Rational prevbr = prevb.getConst<Rational>();
+    if (prevbr == br || (br < prevbr) == isLower)
+    {
+      // subsumed
+      return Node::null();
+    }
+  }
+  Node prevo = isLower ? e->d_secondBound : e->d_firstBound;
+  Trace("strings-eager-aconf-debug")
+      << "Check conflict for bounds " << t << " " << prevo << std::endl;
+  if (!prevo.isNull())
+  {
+    // are we in conflict?
+    Node prevob = prevo.isConst() ? prevo : getBoundForLength(prevo, !isLower);
+    Assert(!prevob.isNull() && prevob.getKind() == CONST_RATIONAL);
+    Rational prevobr = prevob.getConst<Rational>();
+    if (prevobr != br && (prevobr < br) == isLower)
+    {
+      // conflict
+      Node ret = EqcInfo::mkMergeConflict(t, prevo);
+      Trace("strings-eager-aconf")
+          << "String: eager arithmetic bound conflict: " << ret << std::endl;
+      return ret;
+    }
+  }
+  if (isLower)
+  {
+    e->d_firstBound = t;
+  }
+  else
+  {
+    e->d_secondBound = t;
+  }
+  return Node::null();
+}
+
+Node EagerSolver::getBoundForLength(Node len, bool isLower)
+{
+  Assert(len.getKind() == STRING_LENGTH);
+  // it is prohibitively expensive to convert to original form and rewrite,
+  // since this may invoke the rewriter on lengths of complex terms. Instead,
+  // we convert to original term the argument, then call the utility method
+  // for computing the length of the argument, implicitly under an application
+  // of length (ArithEntail::getConstantBoundLength).
+  // convert to original form
+  Node olent = SkolemManager::getOriginalForm(len[0]);
+  // get the bound
+  Node c = d_aent.getConstantBoundLength(olent, isLower);
+  Trace("strings-eager-aconf-debug")
+      << "Constant " << (isLower ? "lower" : "upper") << " bound for " << len
+      << " is " << c << ", from original form " << olent << std::endl;
+  return c;
+}
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/strings/eager_solver.h b/src/theory/strings/eager_solver.h
index cf4062bfe..03fb0ff63 100644
--- a/src/theory/strings/eager_solver.h
+++ b/src/theory/strings/eager_solver.h
@@ -21,8 +21,11 @@
 #include <map>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
+#include "theory/strings/arith_entail.h"
 #include "theory/strings/eqc_info.h"
 #include "theory/strings/solver_state.h"
+#include "theory/strings/term_registry.h"
 
 namespace cvc5 {
 namespace theory {
@@ -32,10 +35,13 @@ namespace strings {
  * Eager solver, which is responsible for tracking of eager information and
  * reporting conflicts to the solver state.
  */
-class EagerSolver
+class EagerSolver : protected EnvObj
 {
  public:
-  EagerSolver(SolverState& state);
+  EagerSolver(Env& env,
+              SolverState& state,
+              TermRegistry& treg,
+              ArithEntail& aent);
   ~EagerSolver();
   /** called when a new equivalence class is created */
   void eqNotifyNewClass(TNode t);
@@ -58,8 +64,21 @@ class EagerSolver
    * for some eqc that is currently equal to z.
    */
   void addEndpointsToEqcInfo(Node t, Node concat, Node eqc);
+  /**
+   * Check for conflict when merging equivalence classes with the given info,
+   * return the node corresponding to the conflict if so.
+   */
+  Node checkForMergeConflict(Node a, Node b, EqcInfo* ea, EqcInfo* eb);
+  /** add arithmetic bound */
+  Node addArithmeticBound(EqcInfo* ea, Node t, bool isLower);
+  /** get bound for length term */
+  Node getBoundForLength(Node len, bool isLower);
   /** Reference to the solver state */
   SolverState& d_state;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
+  /** Arithmetic entailment */
+  ArithEntail& d_aent;
 };
 
 }  // namespace strings
diff --git a/src/theory/strings/eqc_info.cpp b/src/theory/strings/eqc_info.cpp
index 43636ecea..5fb5e91c3 100644
--- a/src/theory/strings/eqc_info.cpp
+++ b/src/theory/strings/eqc_info.cpp
@@ -31,15 +31,15 @@ EqcInfo::EqcInfo(context::Context* c)
       d_codeTerm(c),
       d_cardinalityLemK(c),
       d_normalizedLength(c),
-      d_prefixC(c),
-      d_suffixC(c)
+      d_firstBound(c),
+      d_secondBound(c)
 {
 }
 
 Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
 {
   // check conflict
-  Node prev = isSuf ? d_suffixC : d_prefixC;
+  Node prev = isSuf ? d_secondBound : d_firstBound;
   if (!prev.isNull())
   {
     Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t
@@ -100,28 +100,7 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
     {
       Trace("strings-eager-pconf")
           << "Conflict for " << prevC << ", " << c << std::endl;
-      std::vector<Node> ccs;
-      Node r[2];
-      for (unsigned i = 0; i < 2; i++)
-      {
-        Node tp = i == 0 ? t : prev;
-        if (tp.getKind() == STRING_IN_REGEXP)
-        {
-          ccs.push_back(tp);
-          r[i] = tp[0];
-        }
-        else
-        {
-          r[i] = tp;
-        }
-      }
-      if (r[0] != r[1])
-      {
-        ccs.push_back(r[0].eqNode(r[1]));
-      }
-      Assert(!ccs.empty());
-      Node ret =
-          ccs.size() == 1 ? ccs[0] : NodeManager::currentNM()->mkNode(AND, ccs);
+      Node ret = mkMergeConflict(t, prev);
       Trace("strings-eager-pconf")
           << "String: eager prefix conflict: " << ret << std::endl;
       return ret;
@@ -129,15 +108,40 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
   }
   if (isSuf)
   {
-    d_suffixC = t;
+    d_secondBound = t;
   }
   else
   {
-    d_prefixC = t;
+    d_firstBound = t;
   }
   return Node::null();
 }
 
+Node EqcInfo::mkMergeConflict(Node t, Node prev)
+{
+  std::vector<Node> ccs;
+  Node r[2];
+  for (unsigned i = 0; i < 2; i++)
+  {
+    Node tp = i == 0 ? t : prev;
+    if (tp.getKind() == STRING_IN_REGEXP)
+    {
+      ccs.push_back(tp);
+      r[i] = tp[0];
+    }
+    else
+    {
+      r[i] = tp;
+    }
+  }
+  if (r[0] != r[1])
+  {
+    ccs.push_back(r[0].eqNode(r[1]));
+  }
+  Assert(!ccs.empty());
+  return NodeManager::currentNM()->mkAnd(ccs);
+}
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/strings/eqc_info.h b/src/theory/strings/eqc_info.h
index 1fd430c95..bfc753989 100644
--- a/src/theory/strings/eqc_info.h
+++ b/src/theory/strings/eqc_info.h
@@ -62,17 +62,34 @@ class EqcInfo
   context::CDO<unsigned> d_cardinalityLemK;
   context::CDO<Node> d_normalizedLength;
   /**
-   * A node that explains the longest constant prefix known of this
+   * If this is a string equivalence class, this is
+   * a node that explains the longest constant prefix known of this
    * equivalence class. This can either be:
    * (1) A term from this equivalence class, including a constant "ABC" or
    * concatenation term (str.++ "ABC" ...), or
    * (2) A membership of the form (str.in.re x R) where x is in this
    * equivalence class and R is a regular expression of the form
    * (str.to.re "ABC") or (re.++ (str.to.re "ABC") ...).
+   *
+   * If this is an integer equivalence class, this is the lower bound
+   * of the value of this equivalence class.
+   */
+  context::CDO<Node> d_firstBound;
+  /** same as above, for suffix and integer upper bounds. */
+  context::CDO<Node> d_secondBound;
+  /**
+   * Make merge conflict. Let "bound term" refer to a term that is set
+   * as the data member of this class for d_firstBound or d_secondBound.
+   * This method is called when this implies that two terms occur in an
+   * equivalence class that have conflicting properties. For example,
+   * t may be (str.in_re x (re.++ (str.to_re "A") R2)) and prev may be
+   * (str.++ "B" y), where the equivalence class of x has merged into
+   * the equivalence class of (str.++ "B" y). This method would return
+   * the conflict:
+   *   (and (= x (str.++ "B" y)) (str.in_re x (re.++ (str.to_re "A") R2)))
+   * for this input.
    */
-  context::CDO<Node> d_prefixC;
-  /** same as above, for suffix. */
-  context::CDO<Node> d_suffixC;
+  static Node mkMergeConflict(Node t, Node prev);
 };
 
 }  // namespace strings
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 32ed6896c..28ab63d05 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -90,6 +90,10 @@ Node SolverState::getLengthExp(Node t, std::vector<Node>& exp, Node te)
     // typically shouldnt be necessary
     lengthTerm = t;
   }
+  else
+  {
+    lengthTerm = lengthTerm[0];
+  }
   Debug("strings") << "SolverState::getLengthTerm " << t << " is " << lengthTerm
                    << std::endl;
   if (te != lengthTerm)
@@ -135,13 +139,14 @@ bool SolverState::isEqualEmptyWord(Node s, Node& emps)
   return false;
 }
 
-void SolverState::setPendingPrefixConflictWhen(Node conf)
+void SolverState::setPendingMergeConflict(Node conf, InferenceId id)
 {
-  if (conf.isNull() || d_pendingConflictSet.get())
+  if (d_pendingConflictSet.get())
   {
+    // already set conflict
     return;
   }
-  InferInfo iiPrefixConf(InferenceId::STRINGS_PREFIX_CONFLICT);
+  InferInfo iiPrefixConf(id);
   iiPrefixConf.d_conc = d_false;
   utils::flattenOp(AND, conf, iiPrefixConf.d_premises);
   setPendingConflict(iiPrefixConf);
@@ -188,7 +193,6 @@ void SolverState::separateByLength(
   // not have an associated length in the mappings above, if the length of
   // an equivalence class is unknown.
   std::map<unsigned, std::vector<Node> > eqc_to_strings;
-  NodeManager* nm = NodeManager::currentNM();
   for (const Node& eqc : n)
   {
     Assert(d_ee->getRepresentative(eqc) == eqc);
@@ -197,7 +201,6 @@ void SolverState::separateByLength(
     Node lt = ei ? ei->d_lengthTerm : Node::null();
     if (!lt.isNull())
     {
-      lt = nm->mkNode(STRING_LENGTH, lt);
       Node r = d_ee->getRepresentative(lt);
       std::pair<Node, TypeNode> lkey(r, tnEqc);
       if (eqc_to_leqc.find(lkey) == eqc_to_leqc.end())
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index bbeb470f7..061c5cf10 100644
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -64,9 +64,9 @@ class SolverState : public TheoryState
   void addDisequality(TNode t1, TNode t2);
   //-------------------------------------- end disequality information
   //------------------------------------------ conflicts
-  /** set pending prefix conflict
+  /** set pending merge conflict
    *
-   * If conf is non-null, this is called when conf is a conjunction of literals
+   * This is called when conf is a conjunction of literals
    * that hold in the current context that are unsatisfiable. It is set as the
    * "pending conflict" to be processed as a conflict lemma on the output
    * channel of this class. It is not sent out immediately since it may require
@@ -74,7 +74,7 @@ class SolverState : public TheoryState
    * during a merge operation, when the equality engine is not in a state to
    * provide explanations.
    */
-  void setPendingPrefixConflictWhen(Node conf);
+  void setPendingMergeConflict(Node conf, InferenceId id);
   /**
    * Set pending conflict, infer info version. Called when we are in conflict
    * based on the inference ii. This generalizes the above method.
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 25d0e7336..9a793e14f 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -55,14 +55,14 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
       d_notify(*this),
       d_statistics(),
       d_state(env, d_valuation),
-      d_eagerSolver(d_state),
       d_termReg(env, d_state, d_statistics, d_pnm),
-      d_extTheoryCb(),
-      d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics),
-      d_extTheory(env, d_extTheoryCb, d_im),
       d_rewriter(env.getRewriter(),
                  &d_statistics.d_rewrites,
                  d_termReg.getAlphabetCardinality()),
+      d_eagerSolver(env, d_state, d_termReg, d_rewriter.getArithEntail()),
+      d_extTheoryCb(),
+      d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics),
+      d_extTheory(env, d_extTheoryCb, d_im),
       // the checker depends on the cardinality of the alphabet
       d_checker(d_termReg.getAlphabetCardinality()),
       d_bsolver(env, d_state, d_im),
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index f23b2449f..dbb04580f 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -254,18 +254,18 @@ class TheoryStrings : public Theory {
   SequencesStatistics d_statistics;
   /** The solver state object */
   SolverState d_state;
-  /** The eager solver */
-  EagerSolver d_eagerSolver;
   /** The term registry for this theory */
   TermRegistry d_termReg;
+  /** The theory rewriter for this theory. */
+  StringsRewriter d_rewriter;
+  /** The eager solver */
+  EagerSolver d_eagerSolver;
   /** The extended theory callback */
   StringsExtfCallback d_extTheoryCb;
   /** The (custom) output channel of the theory of strings */
   InferenceManager d_im;
   /** Extended theory, responsible for context-dependent simplification. */
   ExtTheory d_extTheory;
-  /** The theory rewriter for this theory. */
-  StringsRewriter d_rewriter;
   /** The proof rule checker */
   StringProofRuleChecker d_checker;
   /**
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5dd456b9f..5b3f3b729 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2280,6 +2280,7 @@ set(regress_1_tests
   regress1/strings/nt6-dd.smt2
   regress1/strings/nterm-re-inter-sigma.smt2
   regress1/strings/open-pf-merge.smt2
+  regress1/strings/pattern1.smt2
   regress1/strings/pierre150331.smt2
   regress1/strings/policy_variable.smt2
   regress1/strings/pre_ctn_no_skolem_share.smt2
diff --git a/test/regress/regress1/strings/pattern1.smt2 b/test/regress/regress1/strings/pattern1.smt2
new file mode 100644
index 000000000..b75fdb9be
--- /dev/null
+++ b/test/regress/regress1/strings/pattern1.smt2
@@ -0,0 +1,73 @@
+(set-option :produce-models true)
+(set-logic QF_SLIA)
+(set-info :status sat)
+(declare-const x String)
+
+(assert
+ (str.in_re
+  x
+  (re.++
+   (str.to_re "pref")
+   (re.* re.allchar)
+   (str.to_re "a")
+   (re.* re.allchar)
+   (str.to_re "b")
+   (re.* re.allchar)
+   (str.to_re "c")
+   (re.* re.allchar)
+   (str.to_re "d")
+   (re.* re.allchar)
+   (str.to_re "e")
+   (re.* re.allchar)
+   (str.to_re "f")
+   (re.* re.allchar)
+   (str.to_re "g")
+   (re.* re.allchar)
+   (str.to_re "h")
+   (re.* re.allchar)
+   (str.to_re "i")
+   (re.* re.allchar)
+   (str.to_re "j")
+   (re.* re.allchar)
+   (str.to_re "k")
+   (re.* re.allchar)
+   (str.to_re "l")
+   (re.* re.allchar)
+   (str.to_re "m")
+   (re.* re.allchar)
+   (str.to_re "n")
+   (re.* re.allchar)
+   (str.to_re "o")
+   (re.* re.allchar)
+   (str.to_re "p")
+   (re.* re.allchar)
+   (str.to_re "q")
+   (re.* re.allchar)
+   (str.to_re "r")
+   (re.* re.allchar)
+   (str.to_re "s")
+   (re.* re.allchar)
+   (str.to_re "t")
+   (re.* re.allchar)
+   (str.to_re "u")
+   (re.* re.allchar)
+   (str.to_re "v")
+   (re.* re.allchar)
+   (str.to_re "w")
+   (re.* re.allchar)
+   (str.to_re "x")
+   (re.* re.allchar)
+   (str.to_re "y")
+   (re.* re.allchar)
+   (str.to_re "z")
+   (re.* re.allchar))))
+
+(assert
+ (or
+  (= x "pref0a-b-c-de")
+  (str.in_re x (re.++ (str.to_re "prefix") (re.* re.allchar)))
+  (str.in_re x (re.++ (re.* re.allchar) (str.to_re "test") (re.* re.allchar)))))
+
+(check-sat)
+
+