Make strings model construction robust to lengths that are not propagated equal (#2444)

This fixes #2429.

This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value.  See explanation in comment.

We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms.  I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this.

Regardless, the strings model construction should be robust to handle this case, which this PR does.

5 files changed, 481 insertions, 33 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 628ffbba7..2e1d6c2c7 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -501,30 +501,38 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
 {
   Trace("strings-model") << "TheoryStrings : Collect model info" << std::endl;
   Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl;
-  
-  //AJR : no use doing this since we cannot preregister terms with finite types that don't belong to strings.
-  //      change this if we generalize to sequences.
-  //set<Node> termSet;
-  // Compute terms appearing in assertions and shared terms
-  //computeRelevantTerms(termSet);
-  //m->assertEqualityEngine( &d_equalityEngine, &termSet );
 
-  if (!m->assertEqualityEngine(&d_equalityEngine))
+  std::set<Node> termSet;
+
+  // Compute terms appearing in assertions and shared terms
+  computeRelevantTerms(termSet);
+  // assert the (relevant) portion of the equality engine to the model
+  if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
   {
     return false;
   }
 
+  std::unordered_set<Node, NodeHashFunction> repSet;
   NodeManager* nm = NodeManager::currentNM();
   // Generate model
-  std::vector< Node > nodes;
-  getEquivalenceClasses( nodes );
+  // get the relevant string equivalence classes
+  for (const Node& s : termSet)
+  {
+    if (s.getType().isString())
+    {
+      Node r = getRepresentative(s);
+      repSet.insert(r);
+    }
+  }
+  std::vector<Node> nodes(repSet.begin(), repSet.end());
   std::map< Node, Node > processed;
   std::vector< std::vector< Node > > col;
   std::vector< Node > lts;
   separateByLength( nodes, col, lts );
   //step 1 : get all values for known lengths
   std::vector< Node > lts_values;
-  std::map< unsigned, bool > values_used;
+  std::map<unsigned, Node> values_used;
+  std::vector<Node> len_splits;
   for( unsigned i=0; i<col.size(); i++ ) {
     Trace("strings-model") << "Checking length for {";
     for( unsigned j=0; j<col[i].size(); j++ ) {
@@ -534,27 +542,35 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
       Trace("strings-model") << col[i][j];
     }
     Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl;
+    Node len_value;
     if( lts[i].isConst() ) {
-      lts_values.push_back( lts[i] );
-      Assert(lts[i].getConst<Rational>() <= Rational(String::maxSize()),
+      len_value = lts[i];
+    }
+    else if (!lts[i].isNull())
+    {
+      // get the model value for lts[i]
+      len_value = d_valuation.getModelValue(lts[i]);
+    }
+    if (len_value.isNull())
+    {
+      lts_values.push_back(Node::null());
+    }
+    else
+    {
+      Assert(len_value.getConst<Rational>() <= Rational(String::maxSize()),
              "Exceeded UINT32_MAX in string model");
-      unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt();
-      values_used[ lvalue ] = true;
-    }else{
-      //get value for lts[i];
-      if( !lts[i].isNull() ){
-        Node v = d_valuation.getModelValue(lts[i]);
-        Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl;
-        lts_values.push_back( v );
-        Assert(v.getConst<Rational>() <= Rational(String::maxSize()),
-               "Exceeded UINT32_MAX in string model");
-        unsigned lvalue =  v.getConst<Rational>().getNumerator().toUnsignedInt();
-        values_used[ lvalue ] = true;
-      }else{
-        //Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl;
-        //Assert( false );
-        lts_values.push_back( Node::null() );
+      unsigned lvalue =
+          len_value.getConst<Rational>().getNumerator().toUnsignedInt();
+      std::map<unsigned, Node>::iterator itvu = values_used.find(lvalue);
+      if (itvu == values_used.end())
+      {
+        values_used[lvalue] = lts[i];
+      }
+      else
+      {
+        len_splits.push_back(lts[i].eqNode(itvu->second));
       }
+      lts_values.push_back(len_value);
     }
   }
   ////step 2 : assign arbitrary values for unknown lengths?
@@ -564,7 +580,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
   //step 3 : assign values to equivalence classes that are pure variables
   for( unsigned i=0; i<col.size(); i++ ){
     std::vector< Node > pure_eq;
-    Trace("strings-model") << "The equivalence classes ";
+    Trace("strings-model") << "The (" << col[i].size()
+                           << ") equivalence classes ";
     for (const Node& eqc : col[i])
     {
       Trace("strings-model") << eqc << " ";
@@ -614,7 +631,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
         }
         Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl;
         lts_values[i] = nm->mkConst(Rational(lvalue));
-        values_used[ lvalue ] = true;
+        values_used[lvalue] = Node::null();
       }
       Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes ";
       for( unsigned j=0; j<pure_eq.size(); j++ ){
@@ -637,7 +654,42 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
           while (m->hasTerm(c))
           {
             ++sel;
-            Assert(!sel.isFinished());
+            if (sel.isFinished())
+            {
+              // We are in a case where model construction is impossible due to
+              // an insufficient number of constants of a given length.
+
+              // Consider an integer equivalence class E whose value is assigned
+              // n in the model. Let { S_1, ..., S_m } be the set of string
+              // equivalence classes such that len( x ) is a member of E for
+              // some member x of each class S1, ...,Sm. Since our calculus is
+              // saturated with respect to cardinality inference (see Liang
+              // et al, Figure 6, CAV 2014), we have that m <= A^n, where A is
+              // the cardinality of our alphabet.
+
+              // Now, consider the case where there exists two integer
+              // equivalence classes E1 and E2 that are assigned n, and moreover
+              // we did not received notification from arithmetic that E1 = E2.
+              // This typically should never happen, but assume in the following
+              // that it does.
+
+              // Now, it may be the case that there are string equivalence
+              // classes { S_1, ..., S_m1 } whose lengths are in E1,
+              // and classes { S'_1, ..., S'_m2 } whose lengths are in E2, where
+              // m1 + m2 > A^n. In this case, we have insufficient strings to
+              // assign to { S_1, ..., S_m1, S'_1, ..., S'_m2 }. If this
+              // happens, we add a split on len( u1 ) = len( u2 ) for some
+              // len( u1 ) in E1, len( u2 ) in E2. We do this for each pair of
+              // integer equivalence classes that are assigned to the same value
+              // in the model.
+              AlwaysAssert(!len_splits.empty());
+              for (const Node& sl : len_splits)
+              {
+                Node spl = nm->mkNode(OR, sl, sl.negate());
+                d_out->lemma(spl);
+              }
+              return false;
+            }
             c = *sel;
           }
           ++sel;
@@ -4139,6 +4191,7 @@ void TheoryStrings::checkCardinality() {
   std::vector< Node > lts;
   separateByLength( d_strings_eqc, cols, lts );
 
+  Trace("strings-card") << "Check cardinality...." << std::endl;
   for( unsigned i = 0; i<cols.size(); ++i ) {
     Node lr = lts[i];
     Trace("strings-card") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl;
@@ -4219,6 +4272,7 @@ void TheoryStrings::checkCardinality() {
       }
     }
   }
+  Trace("strings-card") << "...end check cardinality" << std::endl;
 }
 
 void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) {
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 5bc6b019f..77dae0cf3 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -578,8 +578,18 @@ private:
   /** get concat vector */
   void getConcatVec(Node n, std::vector<Node>& c);
 
-  // get equivalence classes
+  /** get equivalence classes
+   *
+   * This adds the representative of all equivalence classes to eqcs
+   */
   void getEquivalenceClasses(std::vector<Node>& eqcs);
+  /** get relevant equivalence classes
+   *
+   * This adds the representative of all equivalence classes that contain at
+   * least one term in termSet.
+   */
+  void getRelevantEquivalenceClasses(std::vector<Node>& eqcs,
+                                     std::set<Node>& termSet);
 
   // separate into collections with equal length
   void separateByLength(std::vector<Node>& n,
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 45385f9c6..b4f920ca4 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1493,6 +1493,7 @@ REG1_TESTS = \
 	regress1/strings/issue1105.smt2 \
 	regress1/strings/issue1684-regex.smt2 \
 	regress1/strings/issue2060.smt2 \
+	regress1/strings/issue2429-code.smt2 \
 	regress1/strings/kaluza-fl.smt2 \
 	regress1/strings/loop002.smt2 \
 	regress1/strings/loop003.smt2 \
@@ -1722,6 +1723,7 @@ REG3_TESTS = \
 	regress3/hole9.cvc \
 	regress3/incorrect1.smt \
 	regress3/incorrect2.smt \
+	regress3/issue2429.smt2 \
 	regress3/pp-regfile.smt \
 	regress3/qwh.35.405.shuffled-as.sat03-1651.smt
 
diff --git a/test/regress/regress1/strings/issue2429-code.smt2 b/test/regress/regress1/strings/issue2429-code.smt2
new file mode 100644
index 000000000..2d906c1fd
--- /dev/null
+++ b/test/regress/regress1/strings/issue2429-code.smt2
@@ -0,0 +1,61 @@
+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-option :produce-models true)
+(set-info :status sat)
+
+(define-fun byte_2_int ((s String)) Int (ite (= (str.len s) 1) (str.code s) 256))
+
+(define-fun read_buffer16 ((s1 String) (s2 String)) Int
+  (+ (* 256 (byte_2_int s1)) 
+     (byte_2_int s2))
+)
+
+
+(define-fun read_buffer32 ((s1 String) (s2 String) (s3 String) (s4 String)) Int
+  (+ (+ (+ (* 16777216 (byte_2_int s1) )
+           (*    65536 (byte_2_int s2) ) )
+           (*      256 (byte_2_int s3) ) )
+           (byte_2_int s4) )
+)
+
+
+(declare-const magic String)
+(declare-const p1 String)
+(declare-const p2 String)
+(declare-const p3 String)
+(declare-const size1 String)
+(declare-const size2 String)
+(declare-const size3 String)
+(declare-const size4 String)
+(declare-const off1 String)
+(declare-const off2 String)
+(declare-const off3 String)
+(declare-const off4 String)
+(assert (= magic "ABCD"))
+(assert (= 1 (str.len size1)))
+(assert (= 1 (str.len size2)))
+(assert (= 1 (str.len size3)))
+(assert (= 1 (str.len size4)))
+(assert (= 1 (str.len off1)))
+(assert (= 1 (str.len off2)))
+(assert (= 1 (str.len off3)))
+(assert (= 1 (str.len off4)))
+
+
+(declare-const p3_off Int)
+(declare-const before_p3 String)
+(assert (= before_p3 (str.++ p1 p2)))
+(assert (not (str.contains before_p3 magic)))
+(assert (= p3_off (str.len before_p3)))
+
+
+(declare-const p2_size   Int)
+(declare-const p2_off    Int)
+(declare-const p2_min_size  Int)
+(assert (= p2_size  (read_buffer32  size1  size2  size3  size4)))
+(assert (= p2_off   (read_buffer32  off1   off2   off3   off4)))
+(assert (<= (+ p2_size p2_off) p3_off))
+(assert (>= p2_size p2_min_size))
+(assert (= p2_min_size 10))
+
+(check-sat)
diff --git a/test/regress/regress3/issue2429.smt2 b/test/regress/regress3/issue2429.smt2
new file mode 100644
index 000000000..37e932a65
--- /dev/null
+++ b/test/regress/regress3/issue2429.smt2
@@ -0,0 +1,321 @@
+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-option :produce-models true)
+(set-info :status sat)
+
+(define-fun byte_2_int ((s String)) Int
+  (ite (= s "\x00") 0
+  (ite (= s "\x01") 1
+  (ite (= s "\x02") 2
+  (ite (= s "\x03") 3
+  (ite (= s "\x04") 4
+  (ite (= s "\x05") 5
+  (ite (= s "\x06") 6
+  (ite (= s "\x07") 7
+  (ite (= s "\x08") 8
+  (ite (= s "\x09") 9
+  (ite (= s "\x0A") 10
+  (ite (= s "\x0B") 11
+  (ite (= s "\x0C") 12
+  (ite (= s "\x0D") 13
+  (ite (= s "\x0E") 14
+  (ite (= s "\x0F") 15
+  (ite (= s "\x10") 16
+  (ite (= s "\x11") 17
+  (ite (= s "\x12") 18
+  (ite (= s "\x13") 19
+  (ite (= s "\x14") 20
+  (ite (= s "\x15") 21
+  (ite (= s "\x16") 22
+  (ite (= s "\x17") 23
+  (ite (= s "\x18") 24
+  (ite (= s "\x19") 25
+  (ite (= s "\x1A") 26
+  (ite (= s "\x1B") 27
+  (ite (= s "\x1C") 28
+  (ite (= s "\x1D") 29
+  (ite (= s "\x1E") 30
+  (ite (= s "\x1F") 31
+  (ite (= s "\x20") 32
+  (ite (= s "\x21") 33
+  (ite (= s "\x22") 34
+  (ite (= s "\x23") 35
+  (ite (= s "\x24") 36
+  (ite (= s "\x25") 37
+  (ite (= s "\x26") 38
+  (ite (= s "\x27") 39
+  (ite (= s "\x28") 40
+  (ite (= s "\x29") 41
+  (ite (= s "\x2A") 42
+  (ite (= s "\x2B") 43
+  (ite (= s "\x2C") 44
+  (ite (= s "\x2D") 45
+  (ite (= s "\x2E") 46
+  (ite (= s "\x2F") 47
+  (ite (= s "\x30") 48
+  (ite (= s "\x31") 49
+  (ite (= s "\x32") 50
+  (ite (= s "\x33") 51
+  (ite (= s "\x34") 52
+  (ite (= s "\x35") 53
+  (ite (= s "\x36") 54
+  (ite (= s "\x37") 55
+  (ite (= s "\x38") 56
+  (ite (= s "\x39") 57
+  (ite (= s "\x3A") 58
+  (ite (= s "\x3B") 59
+  (ite (= s "\x3C") 60
+  (ite (= s "\x3D") 61
+  (ite (= s "\x3E") 62
+  (ite (= s "\x3F") 63
+  (ite (= s "\x40") 64
+  (ite (= s "\x41") 65
+  (ite (= s "\x42") 66
+  (ite (= s "\x43") 67
+  (ite (= s "\x44") 68
+  (ite (= s "\x45") 69
+  (ite (= s "\x46") 70
+  (ite (= s "\x47") 71
+  (ite (= s "\x48") 72
+  (ite (= s "\x49") 73
+  (ite (= s "\x4A") 74
+  (ite (= s "\x4B") 75
+  (ite (= s "\x4C") 76
+  (ite (= s "\x4D") 77
+  (ite (= s "\x4E") 78
+  (ite (= s "\x4F") 79
+  (ite (= s "\x50") 80
+  (ite (= s "\x51") 81
+  (ite (= s "\x52") 82
+  (ite (= s "\x53") 83
+  (ite (= s "\x54") 84
+  (ite (= s "\x55") 85
+  (ite (= s "\x56") 86
+  (ite (= s "\x57") 87
+  (ite (= s "\x58") 88
+  (ite (= s "\x59") 89
+  (ite (= s "\x5A") 90
+  (ite (= s "\x5B") 91
+  (ite (= s "\x5C") 92
+  (ite (= s "\x5D") 93
+  (ite (= s "\x5E") 94
+  (ite (= s "\x5F") 95
+  (ite (= s "\x60") 96
+  (ite (= s "\x61") 97
+  (ite (= s "\x62") 98
+  (ite (= s "\x63") 99
+  (ite (= s "\x64") 100
+  (ite (= s "\x65") 101
+  (ite (= s "\x66") 102
+  (ite (= s "\x67") 103
+  (ite (= s "\x68") 104
+  (ite (= s "\x69") 105
+  (ite (= s "\x6A") 106
+  (ite (= s "\x6B") 107
+  (ite (= s "\x6C") 108
+  (ite (= s "\x6D") 109
+  (ite (= s "\x6E") 110
+  (ite (= s "\x6F") 111
+  (ite (= s "\x70") 112
+  (ite (= s "\x71") 113
+  (ite (= s "\x72") 114
+  (ite (= s "\x73") 115
+  (ite (= s "\x74") 116
+  (ite (= s "\x75") 117
+  (ite (= s "\x76") 118
+  (ite (= s "\x77") 119
+  (ite (= s "\x78") 120
+  (ite (= s "\x79") 121
+  (ite (= s "\x7A") 122
+  (ite (= s "\x7B") 123
+  (ite (= s "\x7C") 124
+  (ite (= s "\x7D") 125
+  (ite (= s "\x7E") 126
+  (ite (= s "\x7F") 127
+  (ite (= s "\x80") 128
+  (ite (= s "\x81") 129
+  (ite (= s "\x82") 130
+  (ite (= s "\x83") 131
+  (ite (= s "\x84") 132
+  (ite (= s "\x85") 133
+  (ite (= s "\x86") 134
+  (ite (= s "\x87") 135
+  (ite (= s "\x88") 136
+  (ite (= s "\x89") 137
+  (ite (= s "\x8A") 138
+  (ite (= s "\x8B") 139
+  (ite (= s "\x8C") 140
+  (ite (= s "\x8D") 141
+  (ite (= s "\x8E") 142
+  (ite (= s "\x8F") 143
+  (ite (= s "\x90") 144
+  (ite (= s "\x91") 145
+  (ite (= s "\x92") 146
+  (ite (= s "\x93") 147
+  (ite (= s "\x94") 148
+  (ite (= s "\x95") 149
+  (ite (= s "\x96") 150
+  (ite (= s "\x97") 151
+  (ite (= s "\x98") 152
+  (ite (= s "\x99") 153
+  (ite (= s "\x9A") 154
+  (ite (= s "\x9B") 155
+  (ite (= s "\x9C") 156
+  (ite (= s "\x9D") 157
+  (ite (= s "\x9E") 158
+  (ite (= s "\x9F") 159
+  (ite (= s "\xA0") 160
+  (ite (= s "\xA1") 161
+  (ite (= s "\xA2") 162
+  (ite (= s "\xA3") 163
+  (ite (= s "\xA4") 164
+  (ite (= s "\xA5") 165
+  (ite (= s "\xA6") 166
+  (ite (= s "\xA7") 167
+  (ite (= s "\xA8") 168
+  (ite (= s "\xA9") 169
+  (ite (= s "\xAA") 170
+  (ite (= s "\xAB") 171
+  (ite (= s "\xAC") 172
+  (ite (= s "\xAD") 173
+  (ite (= s "\xAE") 174
+  (ite (= s "\xAF") 175
+  (ite (= s "\xB0") 176
+  (ite (= s "\xB1") 177
+  (ite (= s "\xB2") 178
+  (ite (= s "\xB3") 179
+  (ite (= s "\xB4") 180
+  (ite (= s "\xB5") 181
+  (ite (= s "\xB6") 182
+  (ite (= s "\xB7") 183
+  (ite (= s "\xB8") 184
+  (ite (= s "\xB9") 185
+  (ite (= s "\xBA") 186
+  (ite (= s "\xBB") 187
+  (ite (= s "\xBC") 188
+  (ite (= s "\xBD") 189
+  (ite (= s "\xBE") 190
+  (ite (= s "\xBF") 191
+  (ite (= s "\xC0") 192
+  (ite (= s "\xC1") 193
+  (ite (= s "\xC2") 194
+  (ite (= s "\xC3") 195
+  (ite (= s "\xC4") 196
+  (ite (= s "\xC5") 197
+  (ite (= s "\xC6") 198
+  (ite (= s "\xC7") 199
+  (ite (= s "\xC8") 200
+  (ite (= s "\xC9") 201
+  (ite (= s "\xCA") 202
+  (ite (= s "\xCB") 203
+  (ite (= s "\xCC") 204
+  (ite (= s "\xCD") 205
+  (ite (= s "\xCE") 206
+  (ite (= s "\xCF") 207
+  (ite (= s "\xD0") 208
+  (ite (= s "\xD1") 209
+  (ite (= s "\xD2") 210
+  (ite (= s "\xD3") 211
+  (ite (= s "\xD4") 212
+  (ite (= s "\xD5") 213
+  (ite (= s "\xD6") 214
+  (ite (= s "\xD7") 215
+  (ite (= s "\xD8") 216
+  (ite (= s "\xD9") 217
+  (ite (= s "\xDA") 218
+  (ite (= s "\xDB") 219
+  (ite (= s "\xDC") 220
+  (ite (= s "\xDD") 221
+  (ite (= s "\xDE") 222
+  (ite (= s "\xDF") 223
+  (ite (= s "\xE0") 224
+  (ite (= s "\xE1") 225
+  (ite (= s "\xE2") 226
+  (ite (= s "\xE3") 227
+  (ite (= s "\xE4") 228
+  (ite (= s "\xE5") 229
+  (ite (= s "\xE6") 230
+  (ite (= s "\xE7") 231
+  (ite (= s "\xE8") 232
+  (ite (= s "\xE9") 233
+  (ite (= s "\xEA") 234
+  (ite (= s "\xEB") 235
+  (ite (= s "\xEC") 236
+  (ite (= s "\xED") 237
+  (ite (= s "\xEE") 238
+  (ite (= s "\xEF") 239
+  (ite (= s "\xF0") 240
+  (ite (= s "\xF1") 241
+  (ite (= s "\xF2") 242
+  (ite (= s "\xF3") 243
+  (ite (= s "\xF4") 244
+  (ite (= s "\xF5") 245
+  (ite (= s "\xF6") 246
+  (ite (= s "\xF7") 247
+  (ite (= s "\xF8") 248
+  (ite (= s "\xF9") 249
+  (ite (= s "\xFA") 250
+  (ite (= s "\xFB") 251
+  (ite (= s "\xFC") 252
+  (ite (= s "\xFD") 253
+  (ite (= s "\xFE") 254
+  (ite (= s "\xFF") 255
+  256))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+)
+
+
+
+(define-fun read_buffer16 ((s1 String) (s2 String)) Int
+  (+ (* 256 (byte_2_int s1)) 
+     (byte_2_int s2))
+)
+
+
+(define-fun read_buffer32 ((s1 String) (s2 String) (s3 String) (s4 String)) Int
+  (+ (+ (+ (* 16777216 (byte_2_int s1) )
+           (*    65536 (byte_2_int s2) ) )
+           (*      256 (byte_2_int s3) ) )
+           (byte_2_int s4) )
+)
+
+
+(declare-const magic String)
+(declare-const p1 String)
+(declare-const p2 String)
+(declare-const p3 String)
+(declare-const size1 String)
+(declare-const size2 String)
+(declare-const size3 String)
+(declare-const size4 String)
+(declare-const off1 String)
+(declare-const off2 String)
+(declare-const off3 String)
+(declare-const off4 String)
+(assert (= magic "ABCD"))
+(assert (= 1 (str.len size1)))
+(assert (= 1 (str.len size2)))
+(assert (= 1 (str.len size3)))
+(assert (= 1 (str.len size4)))
+(assert (= 1 (str.len off1)))
+(assert (= 1 (str.len off2)))
+(assert (= 1 (str.len off3)))
+(assert (= 1 (str.len off4)))
+
+
+(declare-const p3_off Int)
+(declare-const before_p3 String)
+(assert (= before_p3 (str.++ p1 p2)))
+(assert (not (str.contains before_p3 magic)))
+(assert (= p3_off (str.len before_p3)))
+
+
+(declare-const p2_size   Int)
+(declare-const p2_off    Int)
+(declare-const p2_min_size  Int)
+(assert (= p2_size  (read_buffer32  size1  size2  size3  size4)))
+(assert (= p2_off   (read_buffer32  off1   off2   off3   off4)))
+(assert (<= (+ p2_size p2_off) p3_off))
+(assert (>= p2_size p2_min_size))
+(assert (= p2_min_size 10))
+
+(check-sat)