More

proofs/eo/cpc/rules/Strings.eo

@@ -592,10 +592,11 @@
 ; return: >
 ;   The multiset over-approximation of s, which is a (flattened) concatenation
 ;   term whose components represent an overapproximation of what s may contain.
-(program $str_multiset_overapprox ((T Type) (s (Seq T)) (ss (Seq T) :list) (t (Seq T)) (r (Seq T)))
+(program $str_multiset_overapprox ((T Type) (s (Seq T)) (ss (Seq T) :list) (t (Seq T)) (r (Seq T)) (n Int) (m Int))
     ((Seq T)) (Seq T)
     (
       (($str_multiset_overapprox (str.++ s ss))        (eo::list_concat str.++ ($str_multiset_overapprox s) ($str_multiset_overapprox ss)))
+      (($str_multiset_overapprox (str.substr s n m))   ($str_to_flat_form s false))
       (($str_multiset_overapprox (str.replace s t r))  (eo::list_concat str.++ ($str_multiset_overapprox s) ($str_multiset_overapprox r)))
       (($str_multiset_overapprox s)                    ($str_to_flat_form s false))
     )

test/regress/cli/CMakeLists.txt

@@ -1818,6 +1818,8 @@ set(regress_0_tests
   regress0/strings/code-perf.smt2
   regress0/strings/code-sat-neg-one.smt2
   regress0/strings/complement-simple.smt2
+  regress0/strings/ctn-decompose-3-sym.smt2
+  regress0/strings/dd_issue6913-str-inf.smt2
   regress0/strings/delta-trust-subs.smt2
   regress0/strings/denghan-instance56567.smt2
   regress0/strings/distinct-witness-id.smt2

test/regress/cli/regress0/strings/ctn-decompose-3-sym.smt2

@@ -1,3 +1,5 @@
+; EXPECT: unsat
+(set-logic ALL)
 (declare-fun x () String)
 (declare-fun y () String)
 (declare-fun z () String)