diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-25 18:26:41 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-09-25 16:26:41 -0700 |
| commit | 923abd7000a2ab6e3c0776c59d159bdc3a4d9a52 (patch) | |
| tree | 8f5a1e11428ce181abc5b722997847c4faecc29f /test/regress/regress1/strings | |
| parent | 91565cda11ad42082a11055514e12ddeee459460 (diff) | |
Fix off by one error in strings flat form explanation (#3273)
Fixes #3272.
This was caused by not explaining the last equal component in a flat form inference. For example, if `x=y`, we may infer `z=""` from `u++x++z=u++y` since the 1st and 2nd components of these strings are equal. However, we would not add the explanation of `x=y` due to an off-by-one error.
Notice that this code is very rarely used (the code for F_EndpointEmp is not covered by our regressions). This is since length elaboration should catch conflicting cases like above, where `len(u++x++z)!=len(u++y)` if `x=y` and `z!=""` and thus `u++x++z != u++y`. #3272 happened to catch a rare case where it is applied. This is likely due to theory combination not propagating an equality prior to running a full effort call to strings check, which is unexpected but not impossible.
Diffstat (limited to 'test/regress/regress1/strings')
| -rw-r--r-- | test/regress/regress1/strings/issue3272.smt2 | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/issue3272.smt2 b/test/regress/regress1/strings/issue3272.smt2 new file mode 100644 index 000000000..47759ef1e --- /dev/null +++ b/test/regress/regress1/strings/issue3272.smt2 @@ -0,0 +1,23 @@ +(set-logic ALL_SUPPORTED) +(set-option :strings-exp true) +(set-info :status sat) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun c () String) +(assert + (and + (and + (and + (not (= (ite (= (str.at (str.substr c 1 (- (str.len (str.substr c 0 (- (str.len c) 1))) 1)) (- (str.len (str.substr (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1))) 1)) "\t") 1 0) 0)) + + (= (ite (= (str.at (str.substr (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1)) 0) "\n") 1 0) 0) + ) + + (= (ite (= (str.at (str.substr (str.substr c 1 (- (str.len c) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1)) 0) " ") 1 0) 0) + (not (= (ite (= (str.at (str.substr (str.replace a b "") 1 (- (str.len c) 1)) (- (str.len (str.substr c 1 (- (str.len c) 1))) 1)) "\v") 1 0) 0)) + ) + (= (ite (= (str.at (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0) " ") 1 0) 0) + ) +) +; may trigger F_EndpointEmp inference +(check-sat) |