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.

1 files changed, 61 insertions, 0 deletions

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)